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

assets when developing software, e.g. to develop a generic system from which one
can instantiate concrete systems. Additionally, the use of domain-specific lan-
guages (DSLs) as front-ends for development tools is advocated. In contrast to
general-purpose specification and programming languages, DSLs facilitate their
utilisation by domain experts who are not specialists in the field of information
technology, because they use the terminology of the application domain.
Inspired by these considerations, we have suggested an approach for e-
cient construction of a family of similar tramway or railway control systems
in [23,24] and exemplified it for a class of route-based tramway control systems.
The idea is to provide a framework consisting of (1) a generic control system
that can be instantiated with configuration data, (2) a DSL front-end for spec-
ifying application-specific parameters and (3) a generator from domain-specific
descriptions into configuration data and instantiation rules for the concrete sys-
tem. Hence, for each control system to be developed, application-specific para-
meters are described in the domain-specific language and from this specification
a control system can automatically be generated. An advantage of the front-end
consists in the fact that it is much simpler to specify the parameters of a sys-
tem in the domain-specific language and then apply the generator, than it is
to program the configuration data directly. This speeds up the production time
and reduces the risk of errors; furthermore, it can be done by domain experts
without requiring the assistance of programming specialists.
While this approach clearly offers advantages, it requires careful work to de-
velop such a language, generator and generic control system and to automatically
verify that generated control systems are safe. For this purpose we use formal
methods.
Automated Verification Approach. As “programming” language for the
control systems we have chosen SystemC [19] that allows for formal reasoning
based on an operational transition system semantics. SystemC serves both as
a compilation target from semi-formal DSL descriptions to semantically well-
founded formal specifications and as high-level programming language which
can be compiled into executable code. Our development approach prescribes
that each time a SystemC control system model is generated and compiled into
object code, verification shall be performed at two levels: (1) The SystemC con-
trol system model is verified to be safe by means of bounded model checking
combined with an inductive proof strategy, and (2) the object code is verified
to be a correct implementation of the SystemC control system model. For this
purpose, the framework provides support tools: a proof obligation generator and
an object code verifier.
Development of Languages and Tools. For the development of a domain-
specific language and support tools our suggestion is to follow the TripTych
dogma by Dines Bjørner (see for instance [9]) making a domain model describ-
ing the concepts of the application domain prior to the actual development of
applications. Apart from separating the concern of describing what there is from