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

Keywords

  • Education
  • Formal methods
  • Model checking

ASJC Scopus subject areas

  • Computer Science(all)

Fingerprint Dive into the research topics of 'Evolution of a course on model checking for practical applications'. Together they form a unique fingerprint.

  • Cite this