MOCHA: Modularity in model checking - Alur, R.; Henzinger, T.; Mang, F.; Qadeer, Shaz; Rajamani, Sriram; Tasiran, S. (Proceedings of the 10th International Conference on Computer-aided Veri cation (CAV), 1998)
We describe a new interactive veri cation environment called Mocha for the modular veri cation of heterogeneous systems. Mocha di ers 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 di erent 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