Applied Bounded Model Checking for Interlocking System Designs

Anne Elisabeth Haxthausen; Jan Peleska; Ralf Pinger

doi:10.1007/978-3-319-05032-4_16

Applied Bounded Model Checking for Interlocking System Designs

Anne Elisabeth Haxthausen, Jan Peleska, Ralf Pinger

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

239 Downloads (Pure)

Abstract

In this paper the verification and validation of interlocking systems is investigated. Reviewing both geographical and route-related interlocking, the verification objectives can be structured from a perspective of computer science into (1) verification of static semantics, and (2) verification of behavioural (operational) semantics. The former checks that the plant model – that is, the software components reflecting the physical components of the interlocking system – has been set up in an adequate way. The latter investigates trains moving through the network, with the objective to uncover potential safety violations. From a formal methods perspective, these verification objectives can be approached by theorem proving, global, or bounded model checking. This paper explains the techniques for application of bounded model checking techniques, and discusses their advantages in comparison to the alternative approaches

Original language	English
Title of host publication	Software Engineering and Formal Methods. Revised Selected Papers
Volume	8368
Publisher	Springer
Publication date	2014
Pages	205–220
ISBN (Print)	978-3-319-05031-7
ISBN (Electronic)	978-3-319-05032-4
DOIs	https://doi.org/10.1007/978-3-319-05032-4_16
Publication status	Published - 2014
Event	11th International Conference on Software Engineering and Formal Methods (SEFM) 2013 - Madrid, Spain Duration: 25 Sep 2013 → 27 Sep 2013 http://antares.sip.ucm.es/sefm2013/

Conference

Conference	11th International Conference on Software Engineering and Formal Methods (SEFM) 2013
Country	Spain
City	Madrid
Period	25/09/2013 → 27/09/2013
Other	Collocated Workshops: BEAT2, WS-FMDS, FM-RAIL-Bok, MoKMaSD, and OpenCert, September 23-24, 2013
Internet address	http://antares.sip.ucm.es/sefm2013/

Series	Lecture Notes in Computer Science
Volume	8368
ISSN	0302-9743

Access to Document

10.1007/978-3-319-05032-4_16

FMRailBOKAccepted author manuscript, 321 KB

Fingerprint Dive into the research topics of 'Applied Bounded Model Checking for Interlocking System Designs'. Together they form a unique fingerprint.

Cite this

@inproceedings{b3787f53cfdb47e5a84acdad9993c2bd,

title = "Applied Bounded Model Checking for Interlocking System Designs",

abstract = "In this paper the verification and validation of interlocking systems is investigated. Reviewing both geographical and route-related interlocking, the verification objectives can be structured from a perspective of computer science into (1) verification of static semantics, and (2) verification of behavioural (operational) semantics. The former checks that the plant model – that is, the software components reflecting the physical components of the interlocking system – has been set up in an adequate way. The latter investigates trains moving through the network, with the objective to uncover potential safety violations. From a formal methods perspective, these verification objectives can be approached by theorem proving, global, or bounded model checking. This paper explains the techniques for application of bounded model checking techniques, and discusses their advantages in comparison to the alternative approaches ",

author = "Haxthausen, {Anne Elisabeth} and Jan Peleska and Ralf Pinger",

year = "2014",

doi = "10.1007/978-3-319-05032-4_16",

language = "English",

isbn = "978-3-319-05031-7",

volume = "8368",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "205–220",

booktitle = "Software Engineering and Formal Methods. Revised Selected Papers",

note = "11th International Conference on Software Engineering and Formal Methods (SEFM) 2013, SEFM 2013 ; Conference date: 25-09-2013 Through 27-09-2013",

url = "http://antares.sip.ucm.es/sefm2013/",

}

Haxthausen, AE, Peleska, J & Pinger, R 2014, Applied Bounded Model Checking for Interlocking System Designs. in Software Engineering and Formal Methods. Revised Selected Papers. vol. 8368, Springer, Lecture Notes in Computer Science, vol. 8368, pp. 205–220, 11th International Conference on Software Engineering and Formal Methods (SEFM) 2013, Madrid, Spain, 25/09/2013. https://doi.org/10.1007/978-3-319-05032-4_16

Applied Bounded Model Checking for Interlocking System Designs. / Haxthausen, Anne Elisabeth; Peleska, Jan; Pinger, Ralf.

Software Engineering and Formal Methods. Revised Selected Papers. Vol. 8368 Springer, 2014. p. 205–220 (Lecture Notes in Computer Science, Vol. 8368).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Applied Bounded Model Checking for Interlocking System Designs

AU - Haxthausen, Anne Elisabeth

AU - Peleska, Jan

AU - Pinger, Ralf

PY - 2014

Y1 - 2014

N2 - In this paper the verification and validation of interlocking systems is investigated. Reviewing both geographical and route-related interlocking, the verification objectives can be structured from a perspective of computer science into (1) verification of static semantics, and (2) verification of behavioural (operational) semantics. The former checks that the plant model – that is, the software components reflecting the physical components of the interlocking system – has been set up in an adequate way. The latter investigates trains moving through the network, with the objective to uncover potential safety violations. From a formal methods perspective, these verification objectives can be approached by theorem proving, global, or bounded model checking. This paper explains the techniques for application of bounded model checking techniques, and discusses their advantages in comparison to the alternative approaches

AB - In this paper the verification and validation of interlocking systems is investigated. Reviewing both geographical and route-related interlocking, the verification objectives can be structured from a perspective of computer science into (1) verification of static semantics, and (2) verification of behavioural (operational) semantics. The former checks that the plant model – that is, the software components reflecting the physical components of the interlocking system – has been set up in an adequate way. The latter investigates trains moving through the network, with the objective to uncover potential safety violations. From a formal methods perspective, these verification objectives can be approached by theorem proving, global, or bounded model checking. This paper explains the techniques for application of bounded model checking techniques, and discusses their advantages in comparison to the alternative approaches

U2 - 10.1007/978-3-319-05032-4_16

DO - 10.1007/978-3-319-05032-4_16

M3 - Article in proceedings

SN - 978-3-319-05031-7

VL - 8368

T3 - Lecture Notes in Computer Science

SP - 205

EP - 220

BT - Software Engineering and Formal Methods. Revised Selected Papers

PB - Springer

T2 - 11th International Conference on Software Engineering and Formal Methods (SEFM) 2013

Y2 - 25 September 2013 through 27 September 2013

ER -