Mocha is a model checker based on the theme of exploiting 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, it uses Alternating Temporal Logic (ATL), a game-based temporal logic that is designed to specify collaborative as well as adversarial interactions between different components. Third, the search algorithms incorporate optimizations based on the hierarchical reduction of sequences of internal transitions. This report describes a new release of Mocha that is implemented in Java and supports many new features including an extensive GUI and a scripting languages for rapid prototyping of symbolic verification algorithms.
Proceedings of the 23rd International Conference on Software Engineering (ICSE'01), 2001.