MOCHA is a joint project between the
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 differences between cMocha and jMocha are:
cMocha follows a software architecture similar to
It is written entirely in C and its graphical user interface is provided by
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
through the C interfaces.
jMocha is written in Java and uses native code BDD libraries from
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 scripts.
an enhanced refinement checker using both symbolic and
an enhanced enumerative checker with many new optimizations like hierarchic