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

the concern of describing what there should be (the applications), this ensures
that different applications are based on the same conceptual understanding.
Then from the domain-model one can establish a model of domain-specific de-
scriptions and their static semantics, a model of the application generators and
a model of the code verifier. For the case study we have formulated such models
in the formal RAISE Specification Language, RSL, [33].

Related Work. The overview given in this paper is based on results pub-
lished in [21,26,28,22,23,25,24,17,20,29,3,30]. Our work has been inspired by
Dines Bjørner's TripTych dogma and formal techniques for software develop-
ment described in [7,8,9,4,10,11].
The domain model used in our case study only includes aspects needed for our
development framework. For domain models capturing a much broader collection
of aspects for railways we consider Dines Bjørner's formal railway domain models
(see e.g. [6,12]) as very promising candidates.
Object code verification has been investigated by several authors, see [32]
for an approach that has influenced our work in a considerable way. While our
results have a similar formal basis - for example, our notion of I/O-equivalence
is a specialisation of the “correct implementation relation” defined in [32] - we
exploit the specific restrictions of our model-based development framework in
order to simplify the equivalence proofs in a considerable way.
For other complementary and competing approaches for the development and
verification of railway control systems the reader is referred to the contributions
in [37,35,36,15], and for a survey of new results and current trends the reader is
referred to the paper [5].

Paper Overview. First, in Sections 2-3, we give an overview of our approach
and informally describe a case study used to illustrate our approach. Then, in
Section 4, we outline how a domain-specific description language for our case
study can be formally developed from a static domain model. Next, in Section 5,
we outline the development of application generators. In Section 6, we explain
how the safety requirements can be verified. After that, in Section 7, we outline
our approach for object code verification and we sketch how an associated code
verifier can be formally developed. Finally, in Section 8, we discuss the work
presented in this paper.

2 Method and Toolchain - Overview

Our approach requires a domain-specific language DSL and tools supporting the
language. The main tool components required are:

1. A data collector for producing syntactically correct DSL text documents.
2. A static semantics checker for DSL documents.
3. Generators parsing DSL documents in order to create (1) executable con-
troller models with transition system semantics (expressed in SystemC), (2)