Description
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 interlocking system. 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
| Period | 11 Nov 2009 |
|---|---|
| Held at | Unknown |