Logo Universität Bremen


Universität Bremen - Fachbereich 3 - Informatik


Startseite Detail

Towards a Framework for Modelling and Verification of Relay Interlocking Systems

Datum: 11.11.2009

Ort: Cartesium Rotunde

Vortragende(r): Prof. Dr. Anne E. Haxthausen (Technical University of Denmark)


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. A DSL description for a relay interlocking system
consists of circuit diagrams for the electrical circuits implementing the system,
a track layout diagram describing the station under control, and train route
tables describing the interlocking rules for the use of routes through the station.
The framework provides: (1) a graphical editor for creating DSL descriptions,
(2) a validator (integrated with the editor) 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 of the dynamic behaviour of the described relay interlocking sys-
tem and its physical environment, as well as safety conditions (a model checker
can then be applied to this output to verify that the system satisfies the safety
conditions). The talk will also touch upon how the framework can be formally
developed using the RAISE formal method.


Anne Haxthausen is associate professor at the Department of Informatics
and Mathematical Modelling, Technical University of Denmark. She received
the Ph.D. degree from the Technical University of Denmark in 1989. From
1988 to 1994 she was employed at Dansk Datamatik Center and CRI A/S in
Denmark. In 1993 she was guest researcher at Electrotechnical Laboratory in
Japan. Since 1995, she has been associated with the Technical University of
Her main research interests include formal specification languages and meth-
ods for software development, and span from the mathematical foundations and
development of such methods and languages to their practical industrial applica-
tion. She has contributed to the development of several methods and languages.
For instance, she was one of the key persons in the ESPRIT projects RAISE
(Rigorous Approach to Industrial Software Engineering) and LaCoS (Large-
scale Correct Software using formal methods) in which the RAISE method,
language and tools were developed. She has also contributed to the design and
semantics of CASL, the Common Algebraic Specification Language, as part of
the international Common Framework Initiative for algebraic specification and
development of software (CoFI). During the last decade she has been doing re-
search into domain-specific languages, automated model/code generation from
domain-specific descriptions, automated verification at model-level, and auto-
mated code verification.
Current industrial applications of her research work focus on the develop-
ment and verification of safety critical applications such as railway control systems.