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.
CITATION STYLE
Bryant, R. E., Chauhan, P., Clarke, E. M., & Goel, A. (2000). A theory of consistency for modular synchronous systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1954, pp. 486–504). Springer Verlag. https://doi.org/10.1007/3-540-40922-x_30
Mendeley helps you to discover research relevant for your work.