MOCHA: Modularity in model checking

We describe a new interactive verication environment called Mocha for the modular verication of heterogeneous systems. Mocha diers from many existing model checkers in three signicant ways: { For modeling, we replace unstructured state-transition graphs with the heterogeneous modeling framework of reactive modules [AH96]. The denition of reactive modules is inspired by formalisms such as Unity [CM88], I/O automata [Lyn96], and Esterel [BG88], and allows complex forms of interaction between components within a single transition. Reactive modules provide a semantic glue that allows the formal embedding and interaction of components with dierent characteristics. Some modules may be synchronous, others asynchronous, some may represent hardware, others software, some may be speed-independent, others time-critical. { For requirement specication, we replace the system-level specication languages of linear and branching temporal logics [Pnu77,CE81] with the module-level specication language of Alternating Temporal Logic (ATL) [AHK97]. In ATL, both cooperative and adversarial relationships between modules can be expressed. For example, it is possible to specify that a module can attain a goal regardless of how the environment of the module behaves. { For the verication of complex systems, Mocha supports a range of compositional and hierarchical verication methodologies. For this purpose, reactive modules provide assume-guarantee rules [HQR98] and abstraction operators [AHR98]; Mocha provides algorithms for automatic renement checking, and will provide a proof editor that manages the decomposition of verication tasks into subtasks. In this paper, we describe the toolkit Mocha in which the proposed approach is being implemented. The input language of Mocha is a machine readable variant of reactive modules. The following functionalities are currently being supported: { Simulation, including games between the user and the simulator { Enumerative and symbolic invariant checking and error-trace generation