Evolution of a course on model checking for practical applications

Yasuyuki Tahara, Nobukazu Yoshioka, Kenji Taguchi, Toshiaki Aoki, Shinichi Honiden

Research output: Contribution to journalArticle

2 Citations (Scopus)

Abstract

Although model checking is expected as a practical formal verification approach for its automatic nature, it still suffers from difficulties in writing the formal descriptions to be verified and applying model checking tools to them effectively. The difficulties are found mainly in grasping the exact system behaviors, representing them in formal languages, and using model checking tools that fit the best to the verification problems. Even capable software developers need extensive education to overcome the difficulties. In this paper, we report our education course of practical applications of model checking in our education project called Top SE. Our approach consists of the following two features. First, we adopt UML as the design specification language and create the descriptions for each specific model checking tool from the UML diagrams, to enable easy practical application of model checking. Second, we build taxonomies of system behaviors, in particular behaviors of concurrent systems that are main targets of model checking. We can organize the knowledge and the techniques of practical model checking according to the taxonomies. The taxonomies are based on several aspects of system behaviors such as synchronization of transitions, synchronization of communications, and modeling of system environments. In addition, we make clear which model checking tools fit which types of systems. We treat the three different model checking tools: SPIN, SMV, and LTSA. Each tool has its specific features that make the tool easier or more difficult to be applied to specific problems than others. In our education course, we explain the taxonomies, the knowledge, and the techniques using very simple examples. We also assign the students exercises to apply the knowledge and the techniques to more complicated problems such as the dining philosopher problem, data copying between a DVD recorder and a hard disk recorder, and the alternating bit protocol.

Original languageEnglish
Pages (from-to)38-44
Number of pages7
JournalSIGCSE Bulletin Inroads
Volume41
Issue number2
DOIs
Publication statusPublished - 2009 Jun 25
Externally publishedYes

Fingerprint

Model checking
Taxonomies
Education
Synchronization
Copying
Formal languages
Videodisks
Specification languages
Hard disk storage
Students
Network protocols
Communication

Keywords

  • Education
  • Formal methods
  • Model checking

ASJC Scopus subject areas

  • Computer Science(all)

Cite this

Evolution of a course on model checking for practical applications. / Tahara, Yasuyuki; Yoshioka, Nobukazu; Taguchi, Kenji; Aoki, Toshiaki; Honiden, Shinichi.

In: SIGCSE Bulletin Inroads, Vol. 41, No. 2, 25.06.2009, p. 38-44.

Research output: Contribution to journalArticle

Tahara, Yasuyuki ; Yoshioka, Nobukazu ; Taguchi, Kenji ; Aoki, Toshiaki ; Honiden, Shinichi. / Evolution of a course on model checking for practical applications. In: SIGCSE Bulletin Inroads. 2009 ; Vol. 41, No. 2. pp. 38-44.
@article{8b1c210f1bb54c34b7543de415ebb638,
title = "Evolution of a course on model checking for practical applications",
abstract = "Although model checking is expected as a practical formal verification approach for its automatic nature, it still suffers from difficulties in writing the formal descriptions to be verified and applying model checking tools to them effectively. The difficulties are found mainly in grasping the exact system behaviors, representing them in formal languages, and using model checking tools that fit the best to the verification problems. Even capable software developers need extensive education to overcome the difficulties. In this paper, we report our education course of practical applications of model checking in our education project called Top SE. Our approach consists of the following two features. First, we adopt UML as the design specification language and create the descriptions for each specific model checking tool from the UML diagrams, to enable easy practical application of model checking. Second, we build taxonomies of system behaviors, in particular behaviors of concurrent systems that are main targets of model checking. We can organize the knowledge and the techniques of practical model checking according to the taxonomies. The taxonomies are based on several aspects of system behaviors such as synchronization of transitions, synchronization of communications, and modeling of system environments. In addition, we make clear which model checking tools fit which types of systems. We treat the three different model checking tools: SPIN, SMV, and LTSA. Each tool has its specific features that make the tool easier or more difficult to be applied to specific problems than others. In our education course, we explain the taxonomies, the knowledge, and the techniques using very simple examples. We also assign the students exercises to apply the knowledge and the techniques to more complicated problems such as the dining philosopher problem, data copying between a DVD recorder and a hard disk recorder, and the alternating bit protocol.",
keywords = "Education, Formal methods, Model checking",
author = "Yasuyuki Tahara and Nobukazu Yoshioka and Kenji Taguchi and Toshiaki Aoki and Shinichi Honiden",
year = "2009",
month = "6",
day = "25",
doi = "10.1145/1595453.1595460",
language = "English",
volume = "41",
pages = "38--44",
journal = "SIGCSE Bulletin Inroads",
issn = "1096-3936",
publisher = "Association for Computing Machinery (ACM)",
number = "2",

}

TY - JOUR

T1 - Evolution of a course on model checking for practical applications

AU - Tahara, Yasuyuki

AU - Yoshioka, Nobukazu

AU - Taguchi, Kenji

AU - Aoki, Toshiaki

AU - Honiden, Shinichi

PY - 2009/6/25

Y1 - 2009/6/25

N2 - Although model checking is expected as a practical formal verification approach for its automatic nature, it still suffers from difficulties in writing the formal descriptions to be verified and applying model checking tools to them effectively. The difficulties are found mainly in grasping the exact system behaviors, representing them in formal languages, and using model checking tools that fit the best to the verification problems. Even capable software developers need extensive education to overcome the difficulties. In this paper, we report our education course of practical applications of model checking in our education project called Top SE. Our approach consists of the following two features. First, we adopt UML as the design specification language and create the descriptions for each specific model checking tool from the UML diagrams, to enable easy practical application of model checking. Second, we build taxonomies of system behaviors, in particular behaviors of concurrent systems that are main targets of model checking. We can organize the knowledge and the techniques of practical model checking according to the taxonomies. The taxonomies are based on several aspects of system behaviors such as synchronization of transitions, synchronization of communications, and modeling of system environments. In addition, we make clear which model checking tools fit which types of systems. We treat the three different model checking tools: SPIN, SMV, and LTSA. Each tool has its specific features that make the tool easier or more difficult to be applied to specific problems than others. In our education course, we explain the taxonomies, the knowledge, and the techniques using very simple examples. We also assign the students exercises to apply the knowledge and the techniques to more complicated problems such as the dining philosopher problem, data copying between a DVD recorder and a hard disk recorder, and the alternating bit protocol.

AB - Although model checking is expected as a practical formal verification approach for its automatic nature, it still suffers from difficulties in writing the formal descriptions to be verified and applying model checking tools to them effectively. The difficulties are found mainly in grasping the exact system behaviors, representing them in formal languages, and using model checking tools that fit the best to the verification problems. Even capable software developers need extensive education to overcome the difficulties. In this paper, we report our education course of practical applications of model checking in our education project called Top SE. Our approach consists of the following two features. First, we adopt UML as the design specification language and create the descriptions for each specific model checking tool from the UML diagrams, to enable easy practical application of model checking. Second, we build taxonomies of system behaviors, in particular behaviors of concurrent systems that are main targets of model checking. We can organize the knowledge and the techniques of practical model checking according to the taxonomies. The taxonomies are based on several aspects of system behaviors such as synchronization of transitions, synchronization of communications, and modeling of system environments. In addition, we make clear which model checking tools fit which types of systems. We treat the three different model checking tools: SPIN, SMV, and LTSA. Each tool has its specific features that make the tool easier or more difficult to be applied to specific problems than others. In our education course, we explain the taxonomies, the knowledge, and the techniques using very simple examples. We also assign the students exercises to apply the knowledge and the techniques to more complicated problems such as the dining philosopher problem, data copying between a DVD recorder and a hard disk recorder, and the alternating bit protocol.

KW - Education

KW - Formal methods

KW - Model checking

UR - http://www.scopus.com/inward/record.url?scp=78651583459&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=78651583459&partnerID=8YFLogxK

U2 - 10.1145/1595453.1595460

DO - 10.1145/1595453.1595460

M3 - Article

VL - 41

SP - 38

EP - 44

JO - SIGCSE Bulletin Inroads

JF - SIGCSE Bulletin Inroads

SN - 1096-3936

IS - 2

ER -