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

Linh Hong Vu, Anne Elisabeth Haxthausen, Jan Peleska

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

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
Volume10598
PublisherSpringer
Publication date2017
Pages99-115
DOIs
Publication statusPublished - 2017
EventRSSRail 2017 - Pistoia, Italy
Duration: 14 Nov 201717 Nov 2017
Conference number: 2

Conference

ConferenceRSSRail 2017
Number2
CountryItaly
CityPistoia
Period14/11/201717/11/2017
SeriesLecture Notes in Computer Science
Volume10598
ISSN0302-9743

Keywords

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

Cite this

Vu, L. H., Haxthausen, A. E., & Peleska, J. (2017). A Domain-Specific Language for Generic Interlocking Models and Their Properties. In Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification (Vol. 10598, pp. 99-115). Springer. Lecture Notes in Computer Science, Vol.. 10598 https://doi.org/10.1007/978-3-319-68499-4_7
Vu, Linh Hong ; Haxthausen, Anne Elisabeth ; Peleska, Jan. / A Domain-Specific Language for Generic Interlocking Models and Their Properties. Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. Vol. 10598 Springer, 2017. pp. 99-115 (Lecture Notes in Computer Science, Vol. 10598).
@inproceedings{f387c785cd204262b23e43b4bb7e02a0,
title = "A Domain-Specific Language for Generic Interlocking Models and Their Properties",
abstract = "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.",
keywords = "Science, Railway interlocking systems, Domain-specific languages, Formal methods, Formal models, Formal verification",
author = "Vu, {Linh Hong} and Haxthausen, {Anne Elisabeth} and Jan Peleska",
year = "2017",
doi = "10.1007/978-3-319-68499-4_7",
language = "English",
volume = "10598",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "99--115",
booktitle = "Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification",

}

Vu, LH, Haxthausen, AE & Peleska, J 2017, A Domain-Specific Language for Generic Interlocking Models and Their Properties. in Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. vol. 10598, Springer, Lecture Notes in Computer Science, vol. 10598, pp. 99-115, RSSRail 2017, Pistoia, Italy, 14/11/2017. https://doi.org/10.1007/978-3-319-68499-4_7

A Domain-Specific Language for Generic Interlocking Models and Their Properties. / Vu, Linh Hong; Haxthausen, Anne Elisabeth; Peleska, Jan.

Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. Vol. 10598 Springer, 2017. p. 99-115 (Lecture Notes in Computer Science, Vol. 10598).

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

TY - GEN

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

AU - Vu, Linh Hong

AU - Haxthausen, Anne Elisabeth

AU - Peleska, Jan

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

KW - Science

KW - Railway interlocking systems

KW - Domain-specific languages

KW - Formal methods

KW - Formal models

KW - Formal verification

U2 - 10.1007/978-3-319-68499-4_7

DO - 10.1007/978-3-319-68499-4_7

M3 - Article in proceedings

VL - 10598

T3 - Lecture Notes in Computer Science

SP - 99

EP - 115

BT - Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification

PB - Springer

ER -

Vu LH, Haxthausen AE, Peleska J. A Domain-Specific Language for Generic Interlocking Models and Their Properties. In Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. Vol. 10598. Springer. 2017. p. 99-115. (Lecture Notes in Computer Science, Vol. 10598). https://doi.org/10.1007/978-3-319-68499-4_7