Verification, Validation and Test for Railway Control Systems
based on Domain-Specific Descriptions
Author: Anne E.~Haxthausen and Jan Peleska
Abstract:
In this paper we present a method for the verification of route based
railway control systems developed from domain-specific descriptions
following an approach suggested by the authors in earlier publications. A
domain-specific description consists of a network description, a route
description and a hardware description. The network description is given a
state transition system semantics that describes the dynamic behaviour of
the uncontrolled domain and in terms of which one can specify the safety
requirements. From the route description and hardware description one can
automatically derive an executable system also having a state transition
system semantics. The safety properties of the executable software can be
automatically verified by model checking, and the executable integrated
hardware/software system can be automatically tested.
postscript file
(251KB)