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

considerations, this paper describes an approach for the construction, verification
and validation of railway control systems which has been elaborated by the
authors and their collaborators during the last decade.
Two Problem Categories. A closer analysis shows that the problems to be
solved can be structured according to two main categories: (1) The design of
novel generic control algorithms is stimulated by the availability of innovative
technologies offering new possibilities for safe and reliable train control mech-
anisms. In this category the objective is to elaborate generic theories ,thatis,
collections of theorems whose assumptions and implications are universally quan-
tified over, say, railway networks of a certain type. As an example, we mention
the investigation of distributed train control algorithms stimulated by the advent
of mobile communication technologies, now allowing to develop alternatives to
the centralised interlocking paradigm. For the verification of these algorithms
mechanised (first-order or higher-order logic) proof support is desirable.
(2) The development and verification of concrete system configurations ad-
dresses a problem frequently arising in conventional developments: Typically,
railway control systems are nowadays constructed following the principles of
object orientation and generics: The system is designed as a generic collection
of classes, structured according to certain design patterns, collaborations and
frameworks enforcing proven design principles and facilitating the utilisation of
specific hardware technology. Concrete systems are instantiated from the generic
collection using configuration data specifying the network to be controlled, avail-
able track elements (signals, sensors, points) etc. In spite of the elegance of this
approach, it suffers from the flaw that - when conventionally tested for a limited
number of different configurations - some software bugs are only revealed when
new configuration variants are used. Additionally, the verification of configura-
tion data requires a considerable effort, often necessitating customised verifica-
tion tool sets which in turn have to be qualified. As a consequence, also minor
configuration changes, induced, for example, by construction work on certain
track sections, require complex verification processes. The solution to these prob-
lems would be an automated verification suite allowing to verify each concrete
system instance together with its configuration . Here, automation is a crucial
requirement, since the conventional verification process currently only exercised
once on generic system level would be far too time-consuming and expensive to
be repeated on every concrete system instance. In this problem category, verifica-
tion does not involve universal quantification, since all configuration aspects are
completely determined. As a consequence, model-based development combined
with model or property checking, validated compilers or object code verifiers are
the technical means of choice for the development and verification process.
In this article, we focus on the second problem category, for a detailed description
of the first, the reader is referred to [21] and further references listed there.
Domain-specific Approach. In recent years, domain-specific methods for
software development have gained wide interest. One of the main objectives ad-
dressed by these techniques is the possibility for a given domain to reuse various