MOCHA: Exploiting Modularity in Model Checking

Abstract : MOCHA is a growing interactive software environment for specification, simulation and verification of concurrent systems. The main objective MOCHA is to exploit the modularity in the design structure during model checking. It 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). This paper describes jMOCHA (for an introduction to cMOCHA, see [2]). Like its predecessor, jMOCHA offers the following capabilities: * System specification in the language of ReaCTIVE MODULES. Reactive modules allow the formal specification of heterogeneous systems with synchronous and asynchronous components. Reactive Modules support modular and hierarchical structuring and reasoning * System executive by randomized or manual trace generation. In the manual mode, the user may choose at each step one of the possible next state of the system. * Requirement verification by invariant checking. MOCHA supports both symbolic and enumerative search. The symbolic model checker is based on BDD engines developed by the UC Berkeley VIS project. * Implementation verification by checking trace containment between implementation and specification modules. The check can be performed automatically if the specification module has no private variables, and otherwise, the user has to supply a witness module defining the refinement mapping. For decomposing proofs, MOCHA supports an assume-guarantee principle.