nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

On the Use of Static Checking in the Verification of Interlocking Systems

verfasst von : Anne E. Haxthausen, Peter H. Østergaard

Erschienen in: Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications

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

In the formal methods community, the correctness of interlocking tables is typically verified by model checking. This paper suggests to use a static checker for this purpose and it demonstrates for the RobustRailS verification tool set that the execution time and memory usage of its static checker are much less than of its model checker. Furthermore, the error messages of the static checker are much more informative than the counter examples produced by classical model checkers.

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 Formal Methods and Safety Certification: Challenges in the Railways Domain

Nächstes Kapitel Compositional Verification of Multi-station Interlocking Systems

Interlocking tables are also sometimes called control tables.

http://robustrails.man.dtu.dk.

These include points in the path and overlap, and points used for flank and front protection. For detail about flank and front protection, see [16].

This essentially means that they use the same track elements. For a complete definition, see [19].

It should here be noted that using this model checker in a second step for verifying the safety of the model of the instantiated interlocking system has actually turned out to be very efficient. For instance, it succeeded to verify the EDL line, where other model checkers failed within some given resources, cf. [22].

Banci, M., Fantechi, A., Gnesi, S.: Some Experiences on Formal Specification of Railway Interlocking Systems Using Statecharts (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 (DSL-CBI). In: Proceedings of the IEEE International Conference on Computer Science and Automation Engineering (CSAE 2011), 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 and protection systems (2011)

Fantechi, A.: Twenty-five years of formal methods and railways: what next? In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 167–183. Springer, Heidelberg (2014). doi:10.1007/978-3-319-05032-4_13 CrossRef

Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: Schnieder, E., Tarnai, G. (eds.) FORMS/FORMAT 2010 – Formal Methods for Automation and Safety in Railway and Automotive Systems, pp. 107–115. Springer, Heidelberg (2010)

Hvid Hansen, H., Ketema, J., Luttik, B., Mousavi, M.R., Pol, J., Santos, O.M.: Automated verification of executable UML models. In: Aichernig, B.K., Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 225–250. Springer, Heidelberg (2011). doi:10.1007/978-3-642-25271-6_12 CrossRef

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). doi:10.1007/978-3-642-21292-5_10 CrossRef

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., 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). doi:10.1007/978-3-642-12566-9_8 CrossRef

10.

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)CrossRefMATH

11.

James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H., Trumble, M., Williams, D.: Verification of scheme plans using CSP\(||\)B. In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 189–204. Springer, Heidelberg (2014). doi:10.1007/978-3-319-05032-4_15 CrossRef

12.

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, Heidelberg (2016). doi:10.1007/978-3-319-33951-1_10 CrossRef

13.

Mirabadi, A., Yazdi, M.B.: Automatic generation and verification of railway interlocking control tables using FSM and NuSMV. Transp. Probl. 4, 103–110 (2009)

14.

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. Electronic Proceedings in Theoretical Computer Science, vol. 111, pp. 3–28. Open Publishing Association, Rome (2013)

15.

George, C., Haff, P., Havelund, K., Haxthausen, A.E., Milne, R., Nielsen, C.b., Prehn, S., Wagner, K.R: The RAISE Language Group: The RAISE Specification Language. The BCS Practitioners Series. Prentice Hall Int. (1992)

16.

Theeg, G., Vlasenko, S.V., Anders, E.: Railway Signalling & Interlocking: International Compendium. Eurailpress, Germany (2009)

17.

Tombs, D., Robinson, N., Nikandros, G.: Signalling control table generation and verification. In: CORE 2002: Cost Efficient Railways through Engineering, p. 415. Railway Technical Society of Australasia/Rail Track Association of Australia (2002)

18.

Verified Systems International GmbH. RT-Tester Model-Based Test Case and Test Data Generator - RTT-MBT - User Manual (2013). Available on request from http://www.verified.de

19.

Vu, L.H.: Formal Development and Verification of Railway Control Systems - In the context of ERTMS/ETCS Level 2. Ph.D. thesis, Technical University of Denmark, DTU Compute (2015)

20.

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, Institute for Traffic Safety and Automation Engineerin, pp. 200–209. Technische Universität Braunschweig (2014)

21.

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.) Formal Techniques for Safety-Critical Systems. Communications in Computer and Information Science, vol. 476, pp. 223–238. Springer, Heidelberg (2015)

22.

Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modeling and verification of interlocking systems featuring sequential release. Sci. Comput. Program. (2016). http://dx.doi.org/10.1016/j.scico.2016.05.010

23.

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)

Titel: On the Use of Static Checking in the Verification of Interlocking Systems
verfasst von: Anne E. Haxthausen
Peter H. Østergaard
Verlag: Springer International Publishing
Buch: Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications
Print ISBN: 978-3-319-47168-6

Electronic ISBN: 978-3-319-47169-3

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-319-47169-3_19

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"