{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T20:10:04Z","timestamp":1773259804783,"version":"3.50.1"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2011,3,1]],"date-time":"2011-03-01T00:00:00Z","timestamp":1298937600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2011,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>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.<\/jats:p>","DOI":"10.1007\/s00165-009-0143-6","type":"journal-article","created":{"date-parts":[[2009,12,16]],"date-time":"2009-12-16T16:08:25Z","timestamp":1260979705000},"page":"191-219","source":"Crossref","is-referenced-by-count":42,"title":["A formal approach for the construction and verification of railway control systems"],"prefix":"10.1145","volume":"23","author":[{"given":"Anne E.","family":"Haxthausen","sequence":"first","affiliation":[{"name":"Department of Informatics and Mathematical Modelling, Technical University of Denmark, bld 321, 2800, Lyngby, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Peleska","sequence":"additional","affiliation":[{"name":"Department of Mathematics and Computer Science, Universit\u00e4t Bremen, Bremen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian","family":"Kinder","sequence":"additional","affiliation":[{"name":"Department of Mathematics and Computer Science, Universit\u00e4t Bremen, Bremen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Accellera (2004) Property specification language version 1.1"},{"key":"e_1_2_1_2_2_2","unstructured":"Berkenk\u00f6tter K (2006) OCL-based validation of a railway domain profile. In: OCLApps 2006\u2014OCL for (meta-)models in multiple application domains"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Badban B Fr\u00e4nzle 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","DOI":"10.1145\/1188895.1188902"},{"key":"e_1_2_1_2_4_2","unstructured":"Bj\u00f8rner D George CW Stig Hansen B Laustrup H Prehn S (1997) A railway system coordination\u201997 case study workshop example. Technical Report 93 UNU\/IIST P.O.Box 3058 Macau"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner D (2003) Domain engineering: a \u201cradical innovation\u201d for Software and Systems Engineering? A Biased Account. In: Dershowitz N (ed) The Zohar Manna international symposium on \u201cverification: theory & practice\u201d. Springer Heidelberg Germany July 2003","DOI":"10.1007\/978-3-540-39910-0_5"},{"key":"e_1_2_1_2_6_2","unstructured":"Bj\u00f8rner 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\u20192003) Budapest\/Hungary. L\u2019Harmattan Hongrie 15\u201316 May 2003"},{"key":"e_1_2_1_2_7_2","unstructured":"Bj\u00f8rner 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"},{"key":"e_1_2_1_2_8_2","volume-title":"Software engineering, vol 1: abstraction and modelling. Texts in theoretical computer science","author":"Bj\u00f8rner D","year":"2006"},{"key":"e_1_2_1_2_9_2","volume-title":"Software engineering, vol 2: specification of systems and languages. Texts in theoretical computer science","author":"Bj\u00f8rner D","year":"2006"},{"key":"e_1_2_1_2_10_2","volume-title":"Software engineering, vol 3: domains, requirements and software design. Texts in theoretical computer science","author":"Bj\u00f8rner D","year":"2006"},{"key":"e_1_2_1_2_11_2","unstructured":"Bj\u00f8rner D (2006) The r\u00f4le of domain engineering in software development October 2006. In: Invited keynote paper and talk: IPSJ\/SIGSE software engineering symposium 2006 Tokyo"},{"key":"e_1_2_1_2_12_2","unstructured":"Bj\u00f8rner 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"},{"key":"e_1_2_1_2_13_2","unstructured":"Dyhrberg R Christensen N (2004) A domain-specific language for tramway control systems. Master\u2019s thesis Informatics and Mathematical Modelling Technical University of Denmark DTU"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Drechsler R Gro\u00dfe D (2005) System level validation using formal techniques. In: IEE Proceedings-computers and digital techniques 152(3):393\u2013406","DOI":"10.1049\/ip-cdt:20045073"},{"key":"e_1_2_1_2_15_2","unstructured":"European Committee for Electrotechnical Standardization (2001) EN 50128\u2014railway applications\u2014communications signalling and processing systems\u2014software for railway control and protection systems. CENELEC Brussels"},{"key":"e_1_2_1_2_16_2","volume-title":"Integration of software specification techniques for applications in engineering, Lecture Notes in Computer Science, vol 3147","author":"Ehrig H","year":"2004"},{"key":"e_1_2_1_2_17_2","unstructured":"Gjaldb\u00e6k 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"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.5555\/515361"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Goos G Zimmermann W (1999) Verification of compilers. In: Correct system design. Springer Berlin pp 201\u2013230","DOI":"10.1007\/3-540-48092-7_10"},{"key":"e_1_2_1_2_20_2","unstructured":"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"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.879808"},{"key":"e_1_2_1_2_22_2","unstructured":"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 \u201999\u2014Formale Techniken f\u00fcr die Eisenbahnsicherung Fortschritt-Berichte VDI Reihe 12 Nr. 436. VDI-Verlag D\u00fcsseldorf pp 263\u2013271"},{"key":"e_1_2_1_2_23_2","unstructured":"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"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1016\/S1474-6670(17)32426-6"},{"key":"e_1_2_1_2_25_2","unstructured":"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\u20192003) Budapest\/Hungary pp 83\u201390. L\u2019Harmattan Hongrie"},{"key":"e_1_2_1_2_26_2","unstructured":"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\u201315 June 2000. Braunschweig Germany pp 211\u2013217"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.5555\/128869"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"M\u00fcller W Ruf J Rosenstiel W (2003) SystemC\u2014methodologies and applications chap 4. Kluwer Dordrecht pp 97\u2013126","DOI":"10.1007\/b105968"},{"key":"e_1_2_1_2_29_2","unstructured":"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\u201315 June 2000. Braunschweig Germany pp 147\u2013152"},{"key":"e_1_2_1_2_30_2","unstructured":"Peleska J Gro\u00dfe D Haxthausen AE Drechsler R (2004) Automated verification for train control systems. In: Schnieder E Tarnai G (eds) Proceedings of the FORMS\/FORMAT 2004\u2014formal methods for automation and safety in railway and automotive systems pp 252\u2013265. Technical University of Braunschweig ISBN 3-9803363-8-7"},{"key":"e_1_2_1_2_31_2","unstructured":"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"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050027"},{"key":"e_1_2_1_2_33_2","unstructured":"The RAISE Language Group (1992) The RAISE specification language. The BCS practitioners series. Prentice Hall International"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.5555\/993859"},{"key":"e_1_2_1_2_35_2","unstructured":"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"},{"key":"e_1_2_1_2_36_2","unstructured":"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"},{"key":"e_1_2_1_2_37_2","unstructured":"Tarnai G Schnieder E (eds) (2003) Proceedings of the symposium on formal methods for railway operation and control systems (FORMS\u20192003) Budapest L\u2019Harmattan Hongrie"},{"key":"e_1_2_1_2_38_2","unstructured":"XForms 1.0. Available under http:\/\/www.w3.org\/TR\/xforms"},{"key":"e_1_2_1_2_39_2","unstructured":"Extensible Markup Language (XML). Available under http:\/\/www.w3.org\/XML\/"},{"key":"e_1_2_1_2_40_2","unstructured":"The Extensible Stylesheet Language Family (XSL). Available under http:\/\/www.w3.org\/Style\/XSL"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-009-0143-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-009-0143-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-009-0143-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:59:24Z","timestamp":1641484764000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-009-0143-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,3]]},"references-count":40,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,3]]}},"alternative-id":["10.1007\/s00165-009-0143-6"],"URL":"https:\/\/doi.org\/10.1007\/s00165-009-0143-6","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,3]]}}}