AbstractThis article discusses a new approach to model checking of real-time systems. One of the novel aspects of our approach is the fact that an unconventional approach is chosen to deal with representing symbolic state spaces. Its key feature is that it does not use a canonical representation for representing symbolic nodes, but an alternative representation based on splitting trees. We describe this approach in terms of the verification problem of parametric reacheability of systems described in an extension of timed automata. Additionally, we describe how we extended this approach to deal with more complex verification problems, namely the parametric verification of an extension of the real-time temporal logic TCTL. This resulted in a model checking tool called PMC. The practical application of our approach is addressed through the analysis and verification of the root contention protocol of the IEEE1394 (FireWire) standard using this tool.
Categories and Subject Descriptors: D.2.4 [Software Engineering]: Program Verification; C.3 [Special-Purpose and Application-Based Systems]; D.4.7 [Operating Systems]: Organization and Design
Additional Key Words and Phrases: real-time systems, specification, verification, parametric model checking
Selected references
- R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138(1):3-34, 6 February 1995.
- Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 25 April 1994. Fundamental Study.
- Edmund M. Clarke Jr., E. Allen Emerson, and A. Prasad Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244-263, April 1986.
- Thomas A. Henzinger. The theory of hybrid automata. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pages 278-292, New Brunswick, New Jersey, 27-30 July 1996. IEEE Computer Society Press.
- Thomas A. Henzinger, Orna Kupferman, and Moshe Y. Vardi. A space-efficient on-the-fly algorithm for real-time model checking. In Ugo Montanari and Vladimiro Sassone, editors, CONCUR '96: Concurrency Theory, 7th International Conference, volume 1119 of Lecture Notes in Computer Science, pages 514-529, Pisa, Italy, 26-29 August 1996. Springer-Verlag.
- Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193-244, June 1994.