Formal Development and Verification of Railway Control Systems - In the context of ERTMS/ETCS Level 2

Linh Hong Vu

Research output: Book/ReportPh.D. thesis

10666 Downloads (Pure)


This dissertation presents a holistic, formal method for efficient modelling and verification of safety-critical railway control systems that have product line characteristics, i.e., each individual system is constructed by instantiating common generic applications with concrete configuration data. The proposed method is based on a combination of formal methods and domain-specific approaches. While formal methods offer mathematically rigorous specification, verification and validation, domain-specific approaches encapsulate the use of formal methods with familiar concepts and notions of the domain, hence making the method easy for the railway engineers to use. Furthermore, the method features a 4-step verification and validation approach that can be integrated naturally into different phases of the software development process. This 4-step approach identifies possible errors in generic applications or configuration data as early as possible in the software development cycle, and facilitates debugging/troubleshooting if errors are discovered. The proposed method has successfully been applied to case studies of the forthcoming Danish railway interlocking systems that are compatible with the European standardized railway control systems ERTMS/ETCS Level 2. Experiments showed that the method can be used for specification, verification and validation of systems of industrial size.
Original languageEnglish
Place of PublicationKgs. Lyngby
PublisherTechnical University of Denmark
Number of pages276
Publication statusPublished - 2015
SeriesDTU Compute PHD-2015


Dive into the research topics of 'Formal Development and Verification of Railway Control Systems - In the context of ERTMS/ETCS Level 2'. Together they form a unique fingerprint.

Cite this