Project Overview
MMC (Mobility
Model Checker)
is a model checker for mobile systems specified
in the style of the picalculus. MMC addresses the salient issues that
arise in the picalculus including scope extrusion and intrusion, and
dynamic generation of new names to avoid name capture. MMC also supports
verification of security protocols specified using spicalculus.
MMC has been evolved from a model checker to a comprehensive toolset that
consists of a user specification language, a
compiler, a model checker, and a justifier.
The MMC environment builds on
the XSB
tabled logic programming system developed at the Department of Computer Science
at Stony Brook University.
The anticipated benefits from a logic programmingbased approach to model
checking include
the following:

A specification of a model checker is given at the level of semantic
equations, and is therefore not limited to any specific system specification
language or logic.

XSB is essentially a deductive system for proving theorems
in Horn logic. Moreover,
optimized
XSB metainterpreters can be used to execute arbitrary deductive
systems.
Hence, the logic programmingbased approach offers a unique opportunity
to fully and flexibly integrate aspects of verification based
on deduction, such as induction, to
traditional algorithmic
approaches to model checking.

The state spaces of systems modeled in the picalculus is unbounded since
process may generate new channels dynamically, choosing names from an infinite
name space.
By using constraints to finitely represent infinite sets and
tabled resolution to efficiently compute fixed points over these sets,
tabled (contraint) LP is an effective approach for verifying infinite state
systems.

The high level at which model checking is specified correspondingly elevates
the level at which erroneous system specifications can be diagnosed and
debugged.

The ability of a tabled LP system to execute directly and efficiently program analyses
from specifications
facilitates the incorporation of process and formula
abstractions. Such abstractions are based on Abstract Interpretation
techniques, which have been used successfully to ameliorate the
state space explosion problem in model checking.

The programmability of a tabled LP system allows for direct encoding of traditional
model checking optimizations such as partial order reduction.