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,
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
For invariant checking, MOCHA supports both
symbolic and enumerative search.
Implementation verification by checking trace containment between
implementation and specification modules.
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
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
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
an enhanced refinement checker using both symbolic and
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.