Activity: Talks and presentations › Conference presentations
This talk describes a framework currently under development
for modelling, simulation and verification of relay interlocking
systems as used by the Danish railways.
The framework is centered around a domain-specific language (DSL) for
describing such systems, and provides
(1) graphical editors for creating DSL descriptions,
(2) a validator for checking that DSL descriptions are statically well-formed
(follow structural rules of the domain),
(3) a graphical simulator for simulating the dynamic behaviour of
relay interlocking systems, and
(4) generators that from a DSL description can derive a state
transition system model for the dynamic
behaviour of the described relay interlocking system and its physical
environment, as well as safety conditions (a model checker can then be
applied to verify that the system satisfies the safe conditions).
A description in the language consists of a track layout for the
station under control, train route tables, and circuit diagrams
describing the static layout of the circuits implementing the relay
The talk will finally touch upon how the framework is formally developed
using the RAISE formal method.
Note: Invited seminar talk.
Place: Universität Bremen