Advertisement

Using Symbolic Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard

  • Cindy Eisner
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)

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.

References

  1. [BBEL96]
    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.Google Scholar
  2. [BCCZ98]A. Biere, A. Cimatti, E. Clarke, Y. Zhu, “Symbolic Model Checking without BDDs”, in TACAS’99, to appear.Google Scholar
  3. [BCRZ99]
    A. Biere, E. Clarke, R. Raimi, Y. Zhu, “Verifying Safety Properties of a PowerPC Microprocessor Using Symbolic Model Checking without BDDs“,submitted, CAV’ 99.Google Scholar
  4. [CE81]
    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.Google Scholar
  5. [CE81b]
    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.Google Scholar
  6. [CG+95]
    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.Google Scholar
  7. [Fok95]
    W.J. Fokkink, “ Safety criteria for Hoorn-Kersenboogerd Railway Station“, Logic Group Preprint Series 135, Utrecht University 1995.Google Scholar
  8. [Fok99]
    W.J. Fokkink, personal communication to C. Eisner.Google Scholar
  9. [GKV94]
    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.Google Scholar
  10. [Gro98]
    J.F. Groote, personal communication to C. Eisner.Google Scholar
  11. [Gro99]
    J.F. Groote, personal communication to C. Eisner.Google Scholar
  12. [McM93]
    K.L. McMillan, “Symbolic Model Checking“, Kluwer Academic Publishers, 1993.Google Scholar
  13. [SS98]
    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.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Cindy Eisner
    • 1
  1. 1.IBM Haifa Research LaboratoryMatam Advanced Technology CenterHaifaIsrael

Personalised recommendations