Mocha: Modularity in Model Checking

Rajeev Alur, Thomas A. Henzinger, Freddy Y.C. Mang, Shaz Qadeer, Sriram K. Rajamani, and Serdar Tasiran

We describe a new interactive verification environment, called Mocha, for the modular and hierarchical verification of heterogeneous systems. Mocha differs from many existing model checkers in three important ways. First, instead of manipulating unstructured state-transition graphs, Mocha supports the heterogeneous modeling framework of Reactive Modules. Second, instead of employing system requirements written in traditional temporal logics, Mocha checks module requirements written in Alternating Temporal Logic (ATL), which is designed for specifying collaborative as well as adversarial interactions between the components of a system. Third, to support hierarchical design and verification, Mocha combines model checking with automatic and semiautomatic refinement checking based on assume-guarantee reasoning. Additional features of Mocha include various modes of simulation, as well as real-time verification.

Proceedings of the Tenth International Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science 1427, Springer, 1998, pp. 521-525.

Download inofficial, sometimes updated PostScript / PDF document. © 1998 Springer.