Do You Trust Your Model Checker?
In this paper we describe the formal specification and verification of the effcient algorithm for real-time model checking implemented in the model checker RAVEN. It was specified and proved using the KIV system. We demonstrate how to decompose the correctness proof into several independent subtasks and indicate the corresponding verification efforts. The formal verification revealed some errors, reduced the code size, and improved the efficiency of the implementation.
KeywordsModel Check Time Prediction Proof Obligation Correctness Proof Time Jump
Unable to display preview. Download preview PDF.
- 1.R.I. Bahar, E.A. Frohm, C.M. Gaona, G.D. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Algebraic Decision Diagrams and Their Applications. In IEEE/ACM International Conference on Computer Aided Design (ICCAD), pages 188–191, Santa Clara, California, November 1993. ACM/IEEE, IEEE Computer Society Press.Google Scholar
- 2.J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic Model Checking: 1020 States and Beyond. In IEEE Symposium on Logic in Computer Science (LICS), pages 1–33, Washington, D.C., June 1990. IEEE Computer Society Press.Google Scholar
- 3.E. Clarke, K.L. McMillian, X. Zhao, M. Fujita, and J.C.-Y. Yang. Spectral Transforms for large Boolean Functions with Application to Technologie Mapping. In ACM/IEEE Design Automation Conference (DAC), pages 54–60, Dallas, TX, June 1993.Google Scholar
- 5.D. Long. Long-package sun release 4.1 overview of c-library functions, 1993.Google Scholar
- 6.W. Reif. Correctness of Generic Modules. In Nerode and Taitslin, editors, Symposium on Logical Foundations of Computer Science, LNCS 620, Berlin, 1992. Logic at Tver, Tver, Russia, Springer.Google Scholar
- 7.W. Reif, G. Schellhorn, and K. Stenzel. Interactive Correctness Proofs for Software Modules Using KIV. In COMPASS’95 Tenth Annual Conference on Computer Assurance, Gaithersburg (MD), USA, 1995. IEEE preGoogle Scholar
- 8.W. Reif, G. Schellhorn, K. Stenzel, and M. Balser. Structured specifications and interactive proofs with KIV. In W. Bibel and P. Schmitt, editors, Automated Deduction-A Basis for Applications. Kluwer Academic Publishers, Dordrecht, 1998.Google Scholar
- 9.J. Ruf. RAVEN: Real-time analyzing and veri_cation environment. Technical Report WSI 2000-3, University of Tübingen, Wilhelm-Schickard-Institute, January 2000.Google Scholar
- 10.Jürgen Ruf and Thomas Kropf. Symbolic Model Checking for a Discrete Clocked Temporal Logic with Intervals. In E. Cerny and D.K. Probst, editors, Conference on Correct Hardware Design and Veri_cationMethods (CHARME), pages 146–166, Montreal, Canada, October 1997. IFIP WG 10.5, Chapman and Hall.Google Scholar
- 11.Jürgen Ruf and Thomas Kropf. Using MTBDDs for Composition and Model Checking of Real-Time Systems. In FMCAD 1998. Springer, November 1998.Google Scholar
- 12.Jürgen Ruf and Thomas Kropf. Modeling and Checking Networks of CommunicatingReal-Time Systems. In Correct Hardware Design and VeriFication Methods (CHARME 99), pages 265–279. IFIP WG 10.5, Springer, September 1999.Google Scholar
- 13.T. Vollmer. Korrekte Modellprüfung von Realzeitsystemen. Diplomarbeit, Fakultät für Informatik, Universität Ulm, Germany, 2000. (in German).Google Scholar