Advertisement

Formal Verification of Signalling Programs with SafeCap

  • Alexei IliasovEmail author
  • Dominic Taylor
  • Linas Laibinis
  • Alexander Romanovsky
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11093)

Abstract

SafeCap is a modern toolkit for modelling, simulation and formal verification of railway networks. This paper discusses the use of SafeCap for formal analysis and fully-automated scalable safety verification of solid state interlocking (SSI) programs – a technology at the heart of many railway signalling solutions. The focus of the work is on making it easy for signalling engineers to use the developed technology and thus to help with its smooth industrial deployment. In this paper we explain the formal foundations of the proposed method, its tool support, and their application to real life railway verification problems.

References

  1. 1.
    Abrial, J.-R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)CrossRefGoogle Scholar
  2. 2.
    Badeau, F., Amelot, A.: Using B as a high level programming language in an industrial project: Roissy VAL. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 334–354. Springer, Heidelberg (2005).  https://doi.org/10.1007/11415787_20CrossRefGoogle Scholar
  3. 3.
    Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: Météor: a successful application of B in a large project. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369–387. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48119-2_22CrossRefGoogle Scholar
  4. 4.
    Bobot, F., Filliâtre, J.-C., Marché, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Proccedings of Boogie 2011, pp. 53–64 (2011)Google Scholar
  5. 5.
    Busard, S., Cappart, Q., Limbrée, C., Pecheur, C., Schaus, P.: Verification of railway interlocking systems. In: Proceedings of ESSS 2015, pp. 19–31 (2015)Google Scholar
  6. 6.
    Cappart, Q., Limbrée, C., Schaus, P., Quilbeuf, J., Traonouez, L.-M. Legay, A.: Verification of interlocking systems using statistical model checking. In: Proceedings of HASE - High Assurance Systems Engineering, pp. 61–68 (2017)Google Scholar
  7. 7.
    Cimatti, A., et al.: Formal verification and validation of ERTMS industrial railway train spacing system. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 378–393. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-31424-7_29CrossRefGoogle Scholar
  8. 8.
    Department for Transport: RAIB review of the railway industry’s investigation of an irregular signal sequence at Milton Keynes (2008). https://www.gov.uk/raib-reports/review-of-the-railway-industry-s-formal-investigation-of-an-irregular-signal-sequence-at-milton-keynes
  9. 9.
    Gonschorek, T., Bedau, L., Ortmeier, F.: Automatic model-based verification of railway interlocking systems using model checking. In: Proceedings of ESREL (2018)Google Scholar
  10. 10.
    Huber, M., King, S.: Towards an integrated model checker for railway signalling data. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 204–223. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45614-7_12CrossRefGoogle Scholar
  11. 11.
    Iliasov, A., Lopatkin, I., Romanovsky, A.: The safecap platform for modelling railway safety and capacity. In: Bitsch, F., Guiochet, J., Kaâniche, M. (eds.) SAFECOMP 2013. LNCS, vol. 8153, pp. 130–137. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-40793-2_12CrossRefGoogle Scholar
  12. 12.
    Iliasov, A., Lopatkin, I., Romanovsky, A.: Practical formal methods in railways - the safecap approach. In: George, L., Vardanega, T. (eds.) Ada-Europe 2014. LNCS, vol. 8454, pp. 177–192. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-08311-7_14CrossRefGoogle Scholar
  13. 13.
    Iliasov, A., Romanovsky, A.: SafeCap domain language for reasoning about safety and capacity. In: Proceedings of PRDC - Pacific-Rim Dependable Computing, pp. 1–10. IEEE (2012)Google Scholar
  14. 14.
    Iliasov, A., Romanovsky, A.B.: Formal analysis of railway signalling data. In: Proceedings of HASE - High Assurance Systems Engineering, pp. 70–77 (2016)Google Scholar
  15. 15.
    Iliasov, A., Stankaitis, P., Adjepon-Yamoah, D.: Static verification of railway schema and interlocking design data. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 123–133. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-33951-1_9CrossRefGoogle Scholar
  16. 16.
    James, P.: Verification of solid state interlocking programs. In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 253–268. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-05032-4_19CrossRefGoogle Scholar
  17. 17.
    Leuschel, M., Butler, M.: ProB: A model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003).  https://doi.org/10.1007/978-3-540-45236-2_46CrossRefGoogle Scholar
  18. 18.
    Limbrée, C., Cappart, Q., Pecheur, C., Tonetta, S.: Verification of railway interlocking - compositional approach with OCRA. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 134–149. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-33951-1_10CrossRefGoogle Scholar
  19. 19.
    Macedo, H.D., Fantechi, A., Haxthausen, A.E.: Compositional verification of multi-station interlocking systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 279–293. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47169-3_20CrossRefGoogle Scholar
  20. 20.
    Morley, M.J.: Safety Assurance in Interlocking Design. PhD thesis, University of Edinburgh (1996)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Alexei Iliasov
    • 1
    Email author
  • Dominic Taylor
    • 2
  • Linas Laibinis
    • 3
  • Alexander Romanovsky
    • 1
  1. 1.Newcastle UniversityNewcastle upon TyneUK
  2. 2.Systra Scott ListerLondonUK
  3. 3.Institute of Computer ScienceVilnius UniversityVilniusLithuania

Personalised recommendations