nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Formal Verification of Signalling Programs with SafeCap

verfasst von : Alexei Iliasov, Dominic Taylor, Linas Laibinis, Alexander Romanovsky

Erschienen in: Computer Safety, Reliability, and Security

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel A Model-Based Safety Analysis of Dependencies Across Abstraction Layers

Nächstes Kapitel Deriving and Formalising Safety and Security Requirements for Control Systems

For more details, see https://www.mobility.siemens.com/mobility/global/en/interurban-mobility/rail-solutions/rail-automation/electronic-interlockings/pages/electronic-interlockings.aspx.

For more details, see http://www.alstom.com/products-services/product-catalogue/rail-systems/signalling/products/smartlock-interlocking-products/.

With the unfortunate exception of arithmetics that is handled as a black-box rewrite.

For more details, see http://alt-ergo.lri.fr/ and https://cs.nyu.edu/acsys/cvc3/.

Abrial, J.-R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)CrossRef

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_20CrossRef

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_22CrossRef

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)

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)

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)

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_29CrossRef

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

Gonschorek, T., Bedau, L., Ortmeier, F.: Automatic model-based verification of railway interlocking systems using model checking. In: Proceedings of ESREL (2018)

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_12CrossRef

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_12CrossRef

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_14CrossRef

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)

14.

Iliasov, A., Romanovsky, A.B.: Formal analysis of railway signalling data. In: Proceedings of HASE - High Assurance Systems Engineering, pp. 70–77 (2016)

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_9CrossRef

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_19CrossRef

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_46CrossRef

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_10CrossRef

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_20CrossRef

20.

Morley, M.J.: Safety Assurance in Interlocking Design. PhD thesis, University of Edinburgh (1996)

Titel: Formal Verification of Signalling Programs with SafeCap
verfasst von: Alexei Iliasov
Dominic Taylor
Linas Laibinis
Alexander Romanovsky
Verlag: Springer International Publishing
Buch: Computer Safety, Reliability, and Security
Print ISBN: 978-3-319-99129-0

Electronic ISBN: 978-3-319-99130-6

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-99130-6_7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"