Abstract
This paper describes a complete model-based development and verification approach for railway control systems. For each control system to be generated, the user makes a description of the application-specific parameters in a domain-specific language. This description is automatically transformed into an executable control system model expressed in SystemC. This model is then compiled into object code. Verification is performed using three main methods applied to different levels. (0) The domain-specific description is validated wrt. internal consistency by static analysis. (1) The crucial safety properties are verified for the SystemC model by means of bounded model checking. (2) The object code is verified to be I/O behaviourally equivalent to the SystemC model from which it was compiled.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Accellera (2004) Property specification language version 1.1
Berkenkötter K (2006) OCL-based validation of a railway domain profile. In: OCLApps 2006—OCL for (meta-)models in multiple application domains
Badban B, Fränzle M, Peleska J, Teige T (2006) Test automation for hybrid systems. In: Proceedings of the third international Workshop on SOFTWARE QUALITY ASSURANCE (SOQUA 2006), Portland Oregon, USA
Bjørner D, George CW, Stig Hansen B, Laustrup H, Prehn S (1997) A railway system, coordination’97, case study workshop example. Technical Report 93, UNU/IIST, P.O.Box 3058, Macau
Bjørner D (2003) Domain engineering: a “radical innovation” for Software and Systems Engineering? A Biased Account. In: Dershowitz N (ed) The Zohar Manna international symposium on “verification: theory & practice”. Springer, Heidelberg, Germany, July 2003
Bjørner D (2003) New results and current trends in formal techniques for the development of software for transportation systems. In: Proceedings of the symposium on formal methods for railway operation and control systems (FORMS’2003), Budapest/Hungary. L’Harmattan Hongrie, 15–16 May 2003
Bjørner D (2003) Railways systems: towards a domain theory. Technical report, Informatics and Mathematical Modelling, Technical University of Denmark, Building 322, Richard Petersens Plads, DK-2800 Kgs.Lyngby, Denmark
Bjørner D (2006) Software engineering, vol 1: abstraction and modelling. Texts in theoretical computer science. Springer, Berlin
Bjørner D (2006) Software engineering, vol 2: specification of systems and languages. Texts in theoretical computer science. Springer, Berlin
Bjørner D (2006) Software engineering, vol 3: domains, requirements and software design. Texts in theoretical computer science. Springer, Berlin
Bjørner D (2006) The rôle of domain engineering in software development, October 2006. In: Invited keynote paper and talk: IPSJ/SIGSE software engineering symposium 2006, Tokyo
Bjørner D (2006) Domain engineering, August 2006, reprinted March 2007. To appear as a chapter in a book based on the BCS FACS Evening Seminars to be published by Springer, UK
Dyhrberg R, Christensen N (2004) A domain-specific language for tramway control systems. Master’s thesis, Informatics and Mathematical Modelling, Technical University of Denmark, DTU
Drechsler R, Große D (2005) System level validation using formal techniques. In: IEE Proceedings-computers and digital techniques 152(3):393–406
European Committee for Electrotechnical Standardization (2001) EN 50128—railway applications—communications, signalling and processing systems—software for railway control and protection systems. CENELEC, Brussels
Ehrig, H, Damm, W, Desel, J, Große-Rhode, M, Reif, W, Schnieder, E, Westkämper, E (eds) (2004) Integration of software specification techniques for applications in engineering, Lecture Notes in Computer Science, vol 3147. Springer, Berlin ISBN 3-540-23135-8
Gjaldbæk T, Haxthausen AE (2003) Modelling and verification of interlocking systems for railway lines. In: Proceedings of the 10th IFAC symposium on control in transportation systems. Elsevier Science Ltd, Oxford. ISBN 0-08-044059-2
Grötker T, Liao S, Martin G, Swan S (2002) System design with SystemC. Kluwer, Dordrecht
Goos G, Zimmermann W (1999) Verification of compilers. In: Correct system design. Springer, Berlin, pp 201–230
Haxthausen AE, Christensen N, Dyhrberg R (2004) From domain model to domain-specific language for railway control systems. In: Proceedings of formal methods for automation and safety in railway and automotive systems (FORMS/FORMAT 2004), Braunschweig, Germany
Haxthausen AE, Peleska J (2000) Formal development and verification of a distributed railway control system. IEEE Trans Softw Eng 26(8): 687–701
Haxthausen AE, Peleska J (2000) Formal methods for the specification and verification of distributed railway control systems: from algebraic specifications to distributed hybrid real-time systems. In: Forms ’99—Formale Techniken für die Eisenbahnsicherung Fortschritt-Berichte VDI, Reihe 12, Nr. 436. VDI-Verlag, Düsseldorf, pp 263–271
Haxthausen AE, Peleska J (2002) A domain specific language for railway control systems. In: Proceedings of the sixth biennial world conference on integrated design and process technology, (IDPT2002), Pasadena, California
Haxthausen AE, Peleska J (2003) Automatic verification, validation and test for railway control systems based on domain-specific descriptions. In: Proceedings of the 10th IFAC symposium on control in transportation systems. Elsevier Science Ltd, Oxford
Haxthausen AE, Peleska J (2003) Generation of executable railway control components from domain-specific descriptions. In: Proceedings of the symposium on formal methods for railway operation and control systems (FORMS’2003), Budapest/Hungary, pp 83–90. L’Harmattan Hongrie
Lindegaard MP, Viuf P, Haxthausen AE (2000) Modelling railway interlocking systems. In: Proceedings of the 9th IFAC symposium on control in transportation systems 2000, 13–15 June 2000. Braunschweig, Germany, pp 211–217
Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems. Springer, Berlin
Müller W, Ruf J, Rosenstiel W (2003) SystemC—methodologies and applications, chap 4. Kluwer, Dordrecht, pp 97–126
Peleska J, Baer A, Haxthausen AE (2000) Towards domain-specific formal specification languages for railway control systems. In: Proceedings of the 9th IFAC symposium on control in transportation systems 2000, 13–15 June 2000. Braunschweig, Germany, pp 147–152
Peleska J, Große D, Haxthausen AE, Drechsler R (2004) Automated verification for train control systems. In: Schnieder E, Tarnai G (eds) Proceedings of the FORMS/FORMAT 2004—formal methods for automation and safety in railway and automotive systems, pp 252–265. Technical University of Braunschweig, ISBN 3-9803363-8-7
Peleska J, Haxthausen AE (2007) Object code verification for safety-critical railway control systems. In: Proceedings of formal methods for automation and safety in railway and automotive systems (FORMS/FORMAT 2007), Braunschweig, Germany. GZVB e.V., ISBN 13:978-3-937655-09-3
Pnueli A, Shtrichman O, Siegel M (1998) The code validation tool CVT: automatic verification of a compilation process. Int J Softw Tools Technol Transf 2(2): 192–201
The RAISE Language Group (1992) The RAISE specification language. The BCS practitioners series. Prentice Hall International
Rumbaugh J, Jacobson I, Booch G (2004) The unified modeling language —reference manual, 2nd edn. Addison-Wesley, Reading
Schnieder E, Tarnai G (eds) (2004) Proceedings of formal methods for automation and safety in railway and automotive systems (FORMS/FORMAT 2004), Technical University of Braunschweig, Braunschweig, Germany
Schnieder E, Tarnai G (eds) (2007) Proceedings of formal methods for automation and safety in railway and automotive systems (FORMS/FORMAT 2007), Braunschweig, Germany. GZVB e.V., ISBN 13:978-3-937655-09-3
Tarnai G, Schnieder E (eds) (2003) Proceedings of the symposium on formal methods for railway operation and control systems (FORMS’2003), Budapest, L’Harmattan Hongrie
XForms 1.0. Available under http://www.w3.org/TR/xforms
Extensible Markup Language (XML). Available under http://www.w3.org/XML/
The Extensible Stylesheet Language Family (XSL). Available under http://www.w3.org/Style/XSL
Author information
Authors and Affiliations
Corresponding author
Additional information
Zhiming Liu and Jim Woodcock
Rights and permissions
About this article
Cite this article
Haxthausen, A.E., Peleska, J. & Kinder, S. A formal approach for the construction and verification of railway control systems. Form Asp Comp 23, 191–219 (2011). https://doi.org/10.1007/s00165-009-0143-6
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-009-0143-6