Abstract
A state/event model is a concurrent version of Mealy machines used for describing embedded reactive systems. This paper introduces a technique that uses compositionality and dependency analysis to significantly improve the efficiency of symbolic model checking of state/event models. This technique makes possible automated verification of large industrial designs with the use of only modest resources (less than one hour on a standard PC for a model with 1421 concurrent machines). The results of the paper are being implemented in the next version of the commercial tool visualSTATEℳ.
Supported by CIT, The Danish National Center of IT Research
BRICS (Basic Research in Computer Science) is a basic research center funded by the Danish government at Aarhus and Aalborg
Chapter PDF
References
H. R. Andersen, J. Staunstrup, and N. Maretti. Partial model checking with ROBDDs. In E. Brinksma, editor, Proceedings of TACAS'97, volume 1217 of LNCS, pages 35–49. Springer-Verlag, April 1997.
H.R. Andersen. Partial model checking (extended abstract). In Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, pages 398–407, La Jolla, San Diego, 26–29 July 1995. IEEE Computer Society Press.
R.J. Anderson, P. Beame, S. M. Burns, W. Chan, F. Modugno, D. Notkin, and J.D. Reese. Model checking large software specifications. In D. Garlan, editor, SIGSOFT '96. Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 156–66, San Francisco, 1996. ACM.
F. Balarin and A.L. Sangiovanni-Vincentelli. An iterative approach to language containment. In C. Courcoubetis, editor, CAV'93. 5th International Conference on Computer Aided Verification, volume 697 of LNCS, pages 29–40, Berlin, 1993. Springer-Verlag.
R.E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 8(C-35):677–691, 1986.
J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic model checking with partitioned transition relations. In A. Halaas and P. B. Denyer, editors, Proc. 1991 Int. Conf. on VLSI, August 1991.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pages 428–439. IEEE Computer Society Press, 1990.
J.R. Burch, E.M. Clarke, D.E. Long, K.L. McMillan, and D.L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(4):401–424, 1994.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finitestate concurrent systems using temporal logic specifications. A CM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.
E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 1994.
E.M. Clarke, D.E. Long, and K.L. McMillan. Compositional model checking. In Proceedings, Fourth Annual Symposium on Logic in Computer Science, pages 353–362, Asilomar Conference Center, Pacific Grove, California, June 5–8 1989. IEEE Computer Society Press.
O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines based on symbolic execution. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems. Proceedings, volume 407 of LNCS, pages 365–373. Springer-Verlag, 1989.
O. Coudert, J. C. Madre, and C. Berthet. Verifying temporal properties of sequential machines without building their state diagrams. In E.M. Clarke and R.P. Kurshan, editors, CAV'90. Workshop on Computer-Aided Verification., pages 75–84, Rutgers, New Jersey, 1990. American Mathematical Society.
D. Geist and I. Beer. Efficient model checking by automated ordering of transition relation partitions. In D.L. Dill, editor, CAV'94-6th International Conference on Computer Aided Verification, volume 818 of LNCS, pages 299–310, Stanford, 1994. Springer-Verlag.
David Harel. STATECHARTS: A visual formalism for complex systems. Science of Computer Programming, 8(3):231–274, June 1987.
K. J. Kristoffersen, F. Laroussinie, K. G. Larsen, P. Patterson, and W. Yi. A compositional proof of a read-time mutual exclusion protocol. In M. Bidoit and M. Dauchet, editors, Proceedings of TAPSOFT '97: Theory and Practice of Software Development, volume 1214 of LNCS, pages 565–579. Springer-Verlag, 1997.
W. Lee, A. Pardo, J.-Y. Jang, G. Hachtel, and F. Somenzi. Tearing based automatic abstraction for CTL model checking. In 1996 IEEE/ACM International Conference on Computer-Aided Design, pages 76–81, San Jose, CA, 1996. IEEE Comput. Soc. Press.
Beologic® A/S. visualSTATEℳ 3.0 User's Guide, 1996.
K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Norwell Massachusetts, 1993.
T. Sreemani and J.M. Atlee. Feasibility of model checking software requirements: a case study. In COMPASS '96. Proceedings of the Eleventh Annual Conference on Computer Assurance, pages 77–88, New York, USA, 1996. IEEE.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lind-Nielsen, J., Andersen, H.R., Behrmann, G., Hulgaard, H., Kristoifersen, K., Larsen, K.G. (1998). Verification of large state/event systems using compositionality and dependency analysis. In: Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1998. Lecture Notes in Computer Science, vol 1384. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054173
Download citation
DOI: https://doi.org/10.1007/BFb0054173
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64356-2
Online ISBN: 978-3-540-69753-4
eBook Packages: Springer Book Archive