A Theory of Consistency for Modular Synchronous Systems
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.
KeywordsModel Check Observable State Linear Temporal Logic Atomic Proposition Kripke Structure
Unable to display preview. Download preview PDF.
- 1.R. Alur and T.A. Henzinger. “Reactive modules.” In Proceedings of the 11th IEEE Symposium on Logic in Computer Science, pp. 207–218. 1996.Google Scholar
- 2.G. Berry, G. Gonthier. “The synchronous programming language Esterel: Design, semantics, implementation.” Technical Report 842, INRIA. 1988.Google Scholar
- 4.P. Chauhan, E. Clarke, Y. Lu, D. Wang. “Verifying IP-Core based System-On-Chip designs.” In Proceedings of the IEEE ASIC/SOC Conference, pp. 27–31. 1999.Google Scholar
- 6.E. Clarke, O. Grumberg, D. Peled. Model Checking. MIT Press. 1999.Google Scholar
- 7.E. Clarke, Y. Lu, H. Veith, D. Wang, S. German. “Executable Protocol Specification in ESL.” Formal Methods in Computer-Aided Design (FMCAD’00). 2000.Google Scholar
- 8.D.L. Dill. Trace theory for automatic hierarchical verification of speed-independent circuits. ACM Distinguished Dissertations. MIT Press, 1989.Google Scholar
- 9.A. Goel, W. R. Lee. “Formal Verification of an IBM CoreConnect Processor Local Bus Arbiter Core.” 37th ACM/IEEE Design Automation Conference. 2000.Google Scholar
- 10.D. E. Long. “Model Checking, Abstraction and Compositional Reasoning.” PhD Thesis, Carnegie Mellon University, 1993.Google Scholar
- 11.Milner, Tofte, Harper, MacQueen. The Definition of Standard ML. MIT Press, 1997.Google Scholar
- 12.K. Shimizu, D. L. Dill, A. J. Hu. “Monitor-Based Formal Specification.” Formal Methods in Computer Aided Design (FMCAD’00). 2000.Google Scholar
- 13.K. F. Larsen, J. Lichtenberg. MuDDy. Version 1.7. http://www.itu.dk/research/muddy.
- 14.J. L. Nielsen. BuDDy–A Binary Decision Diagram Package. Version 1.7. http://www.itu.dk/research/buddy.
- 15.S. Romanenko, P Sestoft. Moscow ML. Version 1.44. http://www.dina.dk/~sestoft/mosml.html.