This document presents a method for effective development of software
for a product line of similar railway control systems.
The software is constructed in three steps:
first a specifications in a domain-specific language is created,
then a formal behavioural controller model is automatically created from
the specification,
and finally the model is compiled into executable object code.
Formal verification is performed automatically by tools at three levels:
(1) the specification is checked to follow the rules of the domain,
(2) the controller model is checked to ensure safety, and
(3) the object code is verified to be a correct implementation of the
controller model.
| Publication status | Published - 2011 |
|---|
This document is a delivery to Rail Net Denmark (Banedanmark) as a part of the Public Sector Consultancy service offered by the Technical University of Denmark.