JMOCHA: A Model Checking Tool that Exploits Design Structure

Mocha is a model checker based on the theme of exploiting design modularity: instead of manipulating unstructured state-transition graphs, it supports the hierarchical modeling framework of Reactive Modules. The hierarchy is exploited by the tool in three ways. First, veri cation tasks such as re nement checking can be decomposed into subgoals using assume-guarantee rules. Second, instead of traditional temporal logics such as CTL, Mocha supports Alternating Temporal Logic (ATL), a game-based temporal logic for specifying collaborative as well as adversarial interactions between the components of a design. Third, the search algorithms incorporate optimizations based on the hierarchical reduction of sequences of internal transitions. This report describes a new release, called jMocha, which is implemented in Java and supports many new features, including an extensive GUI and a scripting languages for the rapid prototyping of veri cation algorithms. An abbreviated version of this paper a...

• Type: Conference
• Year: 2001
• Where: ICSE
• Authors: Rajeev Alur, Luca de Alfaro, Radu Grosu, Thomas A. Henzinger, M. Kang, Christoph M. Kirsch, Rupak Majumdar, Freddy Y. C. Mang, Bow-Yaw Wang
• Keywords: ICSE 2001, Software Engineering, Temporal Logic, Veri Cation, Veri Cation Tasks