Abstract
Stålmarck’s proof procedure is a method of tautology checking that has been used to verify railway interlocking software.Recently,it has been proposed [13] that the method has potential to increase the capacity of formal verification tools for hardware.In this paper,we examine this potential in light of an experiment in the opposite direction: the application of symbolic model checking to railway interlocking software previously verified with Stålmarck’s method.We show that these railway systems share important characteristics which distinguish them from most hardware designs,and that these differences raise some doubts about the applicability of Stålmarck’s method to hardware verification.
Acknowledgements
Thanks are due to Jan Friso Groote for supplying the railway models used in this paper,and to Holland RailConsult for agreeing to such.Thank you to Wan Fokkink for supplying the invariants which enabled the verification of station Heerhugowaard. The help of both Jan Friso Groote and Wan Fokkink in investigating the discrepancy of section 6.1 was greatly appreciated. Thank you to Sharon Keidar for implementation of optimizations to RuleBase which solved the size problems for these models. Thank you to Shoham Ben-David for careful review and important comments.
Chapter PDF
Similar content being viewed by others
References
I. Beer, S. Ben-David, C. Eisner, A. Landver, “RuleBase:An Industry-Oriented Formal Verification Tool”,in Proc.33rd Design Automation Conference 1996,pp. 655–660.
[BCCZ98]A. Biere, A. Cimatti, E. Clarke, Y. Zhu, “Symbolic Model Checking without BDDs”, in TACAS’99, to appear.
A. Biere, E. Clarke, R. Raimi, Y. Zhu, “Verifying Safety Properties of a PowerPC Microprocessor Using Symbolic Model Checking without BDDs“,submitted, CAV’ 99.
E.M. Clarke and E.A. Emerson“Design and synthesis of synchronization skeletons using Branching Time Temporal Logic“,in Proc.Workshop on Logics of Programs, Lecture Notes in Computer Science, Vol. 131(Springer,Berlin, 1981)pp. 52–71.
E.M. Clarke and E.A. Emerson,“Characterizing Properties of Parallel Programs as Fixed-point“,in Seventh International Colloquium on Automata,Languages,and Programming, Volume 85 of LNCS, 1981.
E. Clarke, O. Grumberg, K. McMillan, X. Zhao, “Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking“, Design Automation Conference 1995, pp. 427–432.
W.J. Fokkink, “ Safety criteria for Hoorn-Kersenboogerd Railway Station“, Logic Group Preprint Series 135, Utrecht University 1995.
W.J. Fokkink, personal communication to C. Eisner.
J.F. Groote, J.W.C. Koorn and S.F.M. van Vlijmen: “The Safety Guaranteeing System at Station Hoorn-Kersenboogerd“ Technical Report 121, Logic Group Preprint Series, Utrecht Univ., 1994.
J.F. Groote, personal communication to C. Eisner.
J.F. Groote, personal communication to C. Eisner.
K.L. McMillan, “Symbolic Model Checking“, Kluwer Academic Publishers, 1993.
M. Sheeran and G. Stålmarck, “A Tutorial on Stålmarck’s Proof Procedure for Propositional Logic“,in Second International Conference on Formal Methods in Computer-Aided Design,CAD’ 98,Volume 1522 of LNCS, 1998, pp. 82–99.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Eisner, C. (1999). Using Symbolic Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard. In: Pierre, L., Kropf, T. (eds) Correct Hardware Design and Verification Methods. CHARME 1999. Lecture Notes in Computer Science, vol 1703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48153-2_9
Download citation
DOI: https://doi.org/10.1007/3-540-48153-2_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66559-5
Online ISBN: 978-3-540-48153-9
eBook Packages: Springer Book Archive