Mocha: Exploiting Modularity in Model Checking

MOCHA is a joint project between the University of California at Berkeley, the University of Pennsylvania, and the State University of New York at Stony Brook; and is funded in part by the Defense Advanced Research Projects Agency (DARPA (NASA) grant NAG2-1214), the National Science Foundation (NSF CAREER award CCR95-01708 and CCR97-34115, and award CCR99-70925), the Microelectronics Advanced Research Corporation (MARCO grant 98-DT-660), and the Semiconductor Research Corporation (SRC contract 99-TJ-683.003 and 99-TJ-688).

MOCHA is a growing interactive software environment for system specification and verification. The main objective of MOCHA is to exploit, rather than destroy, design structure in automatic verification. MOCHA is intended as a vehicle for development of new verification algorithms and approaches. MOCHA is available in two versions, cMocha (Version 1.0.1) and jMocha (Version 2.0).

Both versions offer the following capabilities:

System specification in the language of Reactive Modules. Reactive Modules allow the formal specification of heterogeneous systems with synchronous, asynchronous, and real-time components. Reactive Modules support modular and hierarchical structuring and reasoning principles.
System execution by randomized, user-guided, or mixed-mode trace generation. In mixed-mode trace generation, the user plays a game against MOCHA in which the user guides the execution of some modules, while MOCHA controls the execution of other modules.
Requirement specification in Alternating Temporal Logic . The logic ATL allows the formal specification of requirements that refer to collaborative as well as adversarial relationships between modules. The popular logic CTL is a sublanguage of ATL. (Only invariant and refinement checking in jMocha 2.0)
Requirement verification by ATL model checking. The symbolic model checker in both implementations is based on BDD engines developed by the UC Berkeley VIS project. For invariant checking, MOCHA supports both symbolic and enumerative search.
Implementation verification by checking trace containment between implementation and specification modules. MOCHA supports containment checking if the specification module has no hidden state, and simulation checking otherwise. For decomposing proofs, MOCHA supports an assume-guarantee principle.

The Mocha Team

The Mocha Demo

The Mocha Papers and References

The Mocha Files

jMocha documentation
Download jMocha version 2.0.1 is now available for linux platforms
Download jMocha version 2.0
jMocha is written in Java and uses native code BDD libraries from VIS. Version 2.0 of jMocha explicitly supports only invariant checking and refinement checking, but no temporal logic model checking. However, it provides the following improvements over cMocha:
- an updated graphical user interface written in Java: it looks familiar to Windows/Java users, has a project window and a desktop that simplifies its use, has syntax directed editor windows, allows concurrent threads, can be easily extended and debugged.
- a new simulator with a graphical user interface: it displays traces in a message sequence chart (MSC) fashion and shows dynamically how the update of one variable depends on other variables.
- a proof manager for managing verification proofs such as assume-guarantee proofs.
- a new scripting language called Slang for rapid and structured algorithm development. Slang provides primitive functions for symbolic manipulation of transitions systems and states. Unlike with cMocha, new symbolic algorithms can be developed by writing Slang scripts.
- an enhanced refinement checker using both symbolic and enumerative methods.
- an enhanced enumerative checker with many new optimizations like hierarchic reduction.
cMocha documentation
Download cMocha version 1.0.1
cMocha follows a software architecture similar to VIS. It is written entirely in C and its graphical user interface is provided by Tcl/Tk and Tix. cMocha provides two levels of development: designers and application developers can customize their application or design their own graphical user interface by writing Tcl scripts; algorithm developers and researchers can develop new algorithms by writing C codes, or assemble any verification packages such as those provided by VIS through the C interfaces.