A Domain-Specific Language for Generic Interlocking Models and Their Properties

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedings – Annual report year: 2017Researchpeer-review

View graph of relations

State-of-the-art railway interlocking systems typically adhere to the product line paradigm, where each individual system is obtained by instantiating a generic system with configuration data. In this paper, we present a domain-specific language, IDL, for specifying generic behavioural models and generic properties of interlocking systems. An IDL specification of a generic model consists of generic variable declarations and generic transition rules, and generic properties are generic state invariants. Generic models and generic properties can be instantiated with configuration data. This results in concrete models and concrete properties that can be used as input for a model checker to formally verify that the system model satisfies desired state invariants. The language and a configuration data instantiator based on the semantics have been implemented as components of the RobustRailS tool set for formal specification and verification of interlocking systems. They have successfully been applied to (1) define a generic model and generic safety properties for the new Danish interlocking systems and to (2) instantiate these generic artefacts for real-world stations and lines in Denmark. A novelty of this work is to provide a domain-specific language for generic models and an instantiator tool taking not only configuration data but also a generic model as input instead of using a hard-coded generator for instantiating only one fixed generic model and its properties with configuration data.
Original languageEnglish
Title of host publicationReliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification
Publication date2017
Publication statusPublished - 2017
EventRSSRail 2017 - Pistoia, Italy
Duration: 14 Nov 201717 Nov 2017
Conference number: 2


ConferenceRSSRail 2017
SeriesLecture Notes in Computer Science
CitationsWeb of Science® Times Cited: No match on DOI

    Research areas

  • Science, Railway interlocking systems, Domain-specific languages, Formal methods, Formal models, Formal verification

ID: 139267638