Project Overview
The LMC (Logic Programming-Based
Model Checking) project
deploys the latest advances in concurrency research and in logic
programming systems to build a software environment for system specification
and verification. The project is focussed on model
checking---
determining whether a system specification possesses a property
expressed as a temporal logic formula--- but the techniques we propose are
applicable to any verification methodology requiring fixed-point computation
(e.g., bisimulation and refinement checking).
The LMC environment builds on two existing software systems that have
helped advance the state of the art in their respective fields---the
Concurrency Factory specification and verification environment, and the
XSB
tabled logic programming system.
Both of these systems have been developed at
the Stony Brook Department of Computer Science, and this project brings
together for the two groups of researchers responsible for these
systems.
The anticipated benefits from a logic programming-based 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 meta-interpreters can be used to execute arbitrary deductive
systems.
Hence, the logic programming-based 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.
-
By using constraints to finitely reprsent 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, such as real-time 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.
The directions of current research in the LMC project are:
Work is also underway in enhancing the XSB tabled logic programming
system with the LMC project as the primary application:
- Tabled Constraint Logic Programming
(supports verification of real-time systems)
- Demand-based Tabling
(supports implementation of partial-order
reduction techiques)
Contact: lmc@cs.sunysb.edu
Last modified: Thu Jul 2 16:52:39 EDT 1998