JMOCHA: a model checking tool that exploits design structure
Rajeev Alur, Luca de Alfaro, Radu Grosu, Thomas A. Henzinger, M. KANG, Christoph M. Kirsch, Rupak Majumdar, Freddy Y. C. Mang, B. Y. Wang · 2001
Abstract. 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 aswell 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 prototypingofveri cation algorithms.