jMocha: A Model-checking Tool that Exploits Design Structure

Rajeev Alur, Luca de Alfaro, Radu Grosu, Thomas A. Henzinger, Minsu Kang, Christoph M. Kirsch, Rupak Majumdar, Freddy Y.C. Mang, and Bow-Yaw Wang

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, verification tasks such as refinement 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 verification algorithms.

Proceedings of the 23rd Annual International Conference on Software Engineering (ICSE), IEEE Computer Society Press, 2001, pp. 835-836.

Download inofficial, sometimes updated PostScript / PDF document. © 2001 IEEE.