A Domain-Oriented, Model-Based Approach for Construction and Verification of Railway Control Systems - Formal Methods and Hybrid Real-Time Systems - page 320

A Domain-Oriented, Model-Based Approach
for Construction and Verification of
Railway Control Systems

Anne E. Haxthausen 1 and Jan Peleska 2

1 Informatics and Mathematical Modelling
Technical University of Denmark, Lyngby, Denmark
[e-mail]
2 TZI, Universitat Bremen, Germany
[e-mail]

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 ex-
pressed in SystemC. This model is then compiled into object code. Veri-
fication is performed using four 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 behavioural equivalent to the SystemC model
from which it was compiled. (3) The correctness of the hardware/software
integration is checked by automated testing.
Keywords: domain engineering, domain-specific languages, code gener-
ation, formal methods, verification, railway control systems.

Dedicated to Dines Bjørner and Zhou Chaochen, for their 70th birthdays.

1 Introduction

Motivation. The development of modern railway and tramway control systems
represents a considerable challenge to both systems and software engineers: The
goal to increase the trac throughput while at the same time increasing the
availability and reliability of railway operations leads to a demand for more
elaborate safety mechanisms in order to keep the risk at the same low level
that has been established for European railways until today. The challenge is
further increased by the demand for shorter time-to-market periods and higher
competition among suppliers of the railway domain; both factors resulting in
a demand for a higher degree of automation for the development, verification,
validation and test phases of projects, without impairing the thoroughness of
safety-related quality measures and certification activities. Motivated by these