Research on Validation, Verification and Testing of Embedded Railway Applications


Projektbeschreibung: The European Rail Traffic Management System contains as its main component the European Train Control System (ETCS), which is similar in nature to the Chinese Train Control System (CTCS). These systems are described in various standardization documents in an informal way. This leads to different interpretations by the different suppliers of equipment, with subsequent problems in interoperability and compositionality. This is especially problematic for the transition from ETCS level 2 to level 3, where fixed signaling devices are replaced by simple control logic. In order to be able to formally verify and validate such systems, formal languages and ontologies such as temporal logics are needed. The various versions of ETCS lead to a so-called software product line, which is a core of reusable assets implementing common features for various instances. A challenging research question in this context is the validation of such product lines. The objective of this research is to develop a domain-specific specification language and associated tools for the formulation and verification of modules in the ETCS. In the research project, we will investigate the use of timed temporal logics for online-monitoring and testing of ETCS software applications.
The proposed methodology is to build on previous work in the context of CTCS-3, and in a first step to transfer it to ETCS. Then, using the UNISIG standardization documents, an ontology shall be built which describes and defines all important concepts in the chosen domain. On top of this ontology, a new formal specification language shall be defined which allows to express interfaces and interoperability features within the ETCS. For this language, a formal semantics and automated verification tools shall be developed. In particular, model checking tools used for online monitoring of timed traces of the system under test (SUT) shall be constructed and tailored to the domain-specific language. The language shall be applied in an extended case study for ETCS signaling devices.

Principal Investigators
Schlingloff, Holger Prof. Dr. (Details) (Software Engineering)

Duration of Project
Start date: 01/2013
End date: 12/2014

Last updated on 2020-16-03 at 23:18