sorry, we can't preview this file
file.pdf (274.76 kB)
A Theory of Consistency for Modular Synchronous Systems
journal contribution
posted on 2008-01-01, 00:00 authored by Randal E. Bryant, Pankaj Chauhan, Edmund M Clarke, Amit GoelWe 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.