nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Comparing Formal Verification Approaches of Interlocking Systems

verfasst von : Anne Elisabeth Haxthausen, Hoang Nga Nguyen, Markus Roggenbach

Erschienen in: Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification

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

The verification of railway interlocking systems is a challenging task, and therefore several research groups have suggested to improve this task by using formal methods, but they use different modelling and verification approaches. To advance this research, there is a need to compare these approaches. As a first step towards this, in this paper we suggest a way to compare different formal approaches for verifying designs of route-based interlocking systems and we demonstrate it on modelling and verification approaches developed within the research groups at DTU/Bremen and at Surrey/Swansea. The focus is on designs that are specified by so-called control tables. The paper can serve as a starting point for further comparative studies.

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 Safety Verification of Heterogeneous Railway Networks

Nächstes Kapitel Predictive Reasoning and Machine Learning for the Enhancement of Reliability in Railway Systems

http://www.imm.dtu.dk/~aeha/RobustRailS/index/.

http://www.cs.swan.ac.uk/~csmarkus/ProcessesAndData/ditto.

Banci, M., Fantechi, A., Gnesi, S.: Some experiences on formal specification of railway interlocking systems using statecharts. In: TRain Workshop at SEFM (Software Engineering and Formal Methods) (2005)

Cao, Y., Xu, T., Tang, T., Wang, H., Zhao, L.: Automatic generation and verification of interlocking tables based on domain specific language for computer based interlocking systems. In: CSAE, pp. 511–515. IEEE (2011)

C. European Committee for Electrotechnical Standardization: EN 50128:2011 – railway applications – communications, signalling and processing systems – software for railway control andprotection systems (2011)

Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: Schnieder, E., Tarnai, G. (eds.) FORMS/FORMAT. Springer, Heidelberg (2010)

Foldager, A.: A graphical domain-specific language for railway interlocking systems. Master’s thesis, Technical University of Denmark, DTU Compute (2015)

Haxthausen, A.E.: Towards a framework for modelling and verification of relay interlocking systems. In: Calinescu, R., Jackson, E. (eds.) Monterey Workshop 2010. LNCS, vol. 6662, pp. 176–192. Springer, Heidelberg (2011)

Haxthausen, A.E.: Automated generation of formal safety conditions from railway interlocking tables. Int. J. Softw. Tools Technol. Transf. (STTT) 16(6), 713–726 (2014). Special Issue on Formal Methods for Railway Control SystemsCrossRef

Haxthausen, A.E., Le Bliguet, M., Kjær, A.A.: Modelling and verification of relay interlocking systems. In: Choppy, C., Sokolsky, O. (eds.) Monterey Workshop 2008. LNCS, vol. 6028, pp. 141–153. Springer, Heidelberg (2010)

Haxthausen, A.E., Peleska, J., Kinder, S.: A formal approach for the construction and verification of railway control systems. Formal Aspects Comput. 23(2), 191–219 (2011). Special issue in Honour of Dines Bjørner and Zhou Chaochen on Occasion of their 70th BirthdaysCrossRefMATH

10.

Haxthausen, A.E., Peleska, J., Pinger, R.: Applied bounded model checking for interlocking system designs. In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 205–220. Springer, Heidelberg (2014)CrossRef

11.

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, Heidelberg (2014)

12.

James, P., Lawrence, A., Roggenbach, M., Seisenberger, M.: Towards safety analysis of ERTMS/ETCS level 2 in real-time maude. In: Artho, C., Ölveczky, P.C. (eds.) Formal Techniques for Safety-Critical Systems. Springer, New York (2016)

13.

James, P., Moller, F., Nga, N.H., Roggenbach, M., Schneider, S.A., Treharne, H.: Techniques for modelling and verifying railway interlockings. STTT 16(6), 685–711 (2014)CrossRef

14.

James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Decomposing scheme plans to manage verification complexity. FORMS/FORMAT (2014)

15.

James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S.A., Treharne, H.: On modelling and verifying railway interlockings: tracking train lengths. Sci. Comput. Program 96, 315–336 (2014)CrossRef

16.

James, P., Roggenbach, M.: Encapsulating formal methods within domain specific languages: a solution for verifying railway scheme plans. Math. Comput. Sci. 8(1), 11–38 (2014)MathSciNetCrossRefMATH

17.

James, P., Trumble, M., Treharne, H., Roggenbach, M., Schneider, S.: Ontrack: an open tooling environment for railway verification. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 435–440. Springer, Heidelberg (2013)CrossRef

18.

Kerr, D., Rowbothan, T.: Introduction to Railway Signalling. Institution of Railway Signal Engineers, London (2001)

19.

Leuschel, M., Bendisposto, J., Dobrikov, I., Krings, S., Plagge, D.: From Animation to Data Validation: The ProB Constraint Solver 10 Years On, pp. 427–446. Wiley, Hoboken (2014)

20.

Mirabadi, A., Yazdi, M.B.: Automatic generation and verification of railway interlocking control tables using fsm and nusmv. Transp. Prob. 4(1), 103–110 (2009)

21.

Peleska, J.: Industrial-strength model-based testing - state of the art and current challenges. In: Petrenko, A.K., Schlingloff, H. (eds.) Proceedings 8th Workshop on Model-Based Testing, Rome, Italy, Electronic Proceedings in Theoretical Computer Science, vol. 111, pp. 3–28. Open Publishing Association (2013)

22.

Schneider, S., Treharne, H.: CSP theorems for communicating B machines. Formal Aspects Comput. 17(4), 390–422 (2005)CrossRefMATH

23.

Tombs, D., Robinson, N., Nikandros, G.: Signalling control table generation and verification. In: Proceedings of Cost Efficient Railways through Engineering (CORE ), pp. 415–425. Railway Technical Society of Australasia (2002)

24.

Verified Systems International GmbH: RT-Tester Model-Based Test Case and Test Data Generator - RTT-MBT - User Manual (2013)

25.

Vu, L.H.: Formal development and verification of railway control systems - in the context of ERTMS/ETCS Level 2. Ph.D. thesis (2015)

26.

Vu, L.H., Haxthausen, A.E., Peleska, J.: A domain-specific language for railway interlocking systems. In: Schnieder, E., Tarnai, G. (eds.) FORMS/FORMAT 2014–10th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems, pp. 200–209. Got best-paper-award, Institute for Traffic Safety and Automation Engineering, Technische Universität Braunschweig (2014)

27.

Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modeling and verification of interlocking systems featuring sequential release. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2014. CCIS, vol. 476, pp. 223–238. Springer, Heidelberg (2015)

28.

Winter, K.: Optimising ordering strategies for symbolic model checking of railway interlockings. In: Steffen, B., Margaria, T. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 246–260. Springer, Heidelberg (2012)CrossRef

29.

Winter, K., Johnston, W., Robinson, P., Strooper, P., van den Berg, L.: Tool support for checking railway interlocking designs. In: Proceedings of the 10th Australian Workshop on Safety Critical Systems and Software, SCS 2005, vol. 55, pp. 101–107. Australian Computer Society Inc., Darlinghurst (2006)

30.

Yu, Y.T., Lau, M.F.: A comparison of MC/DC, MUMCUT and several other coverage criteria for logical decisions. J. Syst. Softw. 79(5), 577–590 (2006). Quality SoftwareCrossRef

Titel: Comparing Formal Verification Approaches of Interlocking Systems
verfasst von: Anne Elisabeth Haxthausen
Hoang Nga Nguyen
Markus Roggenbach
Verlag: Springer International Publishing
Buch: Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification
Print ISBN: 978-3-319-33950-4

Electronic ISBN: 978-3-319-33951-1

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-319-33951-1_12

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"

Premium Partner