A Theory of Consistency for Modular Synchronous Systems

Randal E. Bryant, Pankaj Chauhan, Edmund M. Clarke, Amit Goel

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


We propose a model for modular synchronous systems with combinational dependencies and define consistency using this model. We then show how to derive this model from a modular specification where individual modules are specified as Kripke Structures and give an algorithm to check the system for consistency. We have implemented this algorithm symbolically using BDDs in a tool, SpecCheck. We have used this tool to check an example bus protocol derived from an industrial specification. The counterexamples obtained for this protocol highlight the need for consistency checking.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:38
Maintainer sjohnson@cs.indiana.edu.
Start Conference Manager
Conference Systems