Conformance in the Railway Industry: Single-Input-Change Testing a EULYNX Controller

Djurre van der Wal; Marcus Gerhold; Mariëlle Stoelinga

doi:10.1007/978-3-031-43681-9_14

Conformance in the Railway Industry: Single-Input-Change Testing a EULYNX Controller

Djurre van der Wal^*, Marcus Gerhold, Mariëlle Stoelinga

^*Corresponding author for this work

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

33 Downloads (Pure)

Abstract

We propose a novel framework for model-based testing against specifications from EULYNX, a SysML-based standard from the railway industry for the controllers of systems such as points, signals, sensors, and crossings. The main challenge here is the sheer complexity: with state spaces exceeding 10e+10 states, it is hard to derive test suites that achieve a meaningful type of coverage.

We tackle this problem by moving away from the traditional interleaving semantics for SysML. Instead, we propose a synchronous semantics in terms of Finite State Machines (FSMs), leveraging the fact that EULYNX is implemented on Programmable Logic Controllers (PLCs). Then, we deploy Single-Input-Change Deterministic Finite State Machines (SIC-DFSMs), which ensures fully deterministic tests thus minimizing scalability issues.

Our focus lies on the EULYNX specification for point controllers. The generated test suite achieves maximal transition coverage, but test execution time remains substantial. We introduce an additional test suite that achieves maximal transition label coverage. Remarkably, this smaller suite successfully identifies the same four faults as the larger suite.

Original language	English
Title of host publication	Formal Methods for Industrial Critical Systems
Subtitle of host publication	28th International Conference, FMICS 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings
Editors	Alessandro Cimatti, Laura Titolo
Pages	242-258
Number of pages	17
ISBN (Electronic)	978-3-031-43681-9
DOIs	https://doi.org/10.1007/978-3-031-43681-9_14
Publication status	Published - 17 Sept 2023
Event	28th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2023 - Antwerp, Belgium Duration: 20 Sept 2023 → 22 Sept 2023 Conference number: 28

Publication series

Name	Lecture Notes in Computer Science book series
Volume	14290

Conference

Conference	28th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2023
Abbreviated title	FMICS 2023
Country/Territory	Belgium
City	Antwerp
Period	20/09/23 → 22/09/23

Keywords

Conformance testing
Model-based testing
Programmable logic controllers
Railways
Safety-critical systems
Single-Input-Change
2023 OA procedure

Access to Document

10.1007/978-3-031-43681-9_14

978-3-031-43681-9_14Final published version, 454 KBLicence: Taverne

FMICS'23 Best Paper Award
van der Wal, D. (Recipient), Stoelinga, M. I. A. (Recipient) & Gerhold, M. (Recipient), 20 Jul 2023
Prize

Cite this

Wal, D. V. D., Gerhold, M., & Stoelinga, M. (2023). Conformance in the Railway Industry: Single-Input-Change Testing a EULYNX Controller. In A. Cimatti, & L. Titolo (Eds.), Formal Methods for Industrial Critical Systems: 28th International Conference, FMICS 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings (pp. 242-258). (Lecture Notes in Computer Science book series; Vol. 14290). https://doi.org/10.1007/978-3-031-43681-9_14

Wal, Djurre van der ; Gerhold, Marcus ; Stoelinga, Mariëlle. / Conformance in the Railway Industry: Single-Input-Change Testing a EULYNX Controller. Formal Methods for Industrial Critical Systems: 28th International Conference, FMICS 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings. editor / Alessandro Cimatti ; Laura Titolo. 2023. pp. 242-258 (Lecture Notes in Computer Science book series).

@inbook{97719a3635164193a62ff789a8be595a,

title = "Conformance in the Railway Industry: Single-Input-Change Testing a EULYNX Controller",

abstract = "We propose a novel framework for model-based testing against specifications from EULYNX, a SysML-based standard from the railway industry for the controllers of systems such as points, signals, sensors, and crossings. The main challenge here is the sheer complexity: with state spaces exceeding 10e+10 states, it is hard to derive test suites that achieve a meaningful type of coverage.We tackle this problem by moving away from the traditional interleaving semantics for SysML. Instead, we propose a synchronous semantics in terms of Finite State Machines (FSMs), leveraging the fact that EULYNX is implemented on Programmable Logic Controllers (PLCs). Then, we deploy Single-Input-Change Deterministic Finite State Machines (SIC-DFSMs), which ensures fully deterministic tests thus minimizing scalability issues.Our focus lies on the EULYNX specification for point controllers. The generated test suite achieves maximal transition coverage, but test execution time remains substantial. We introduce an additional test suite that achieves maximal transition label coverage. Remarkably, this smaller suite successfully identifies the same four faults as the larger suite.",

keywords = "Conformance testing, Model-based testing, Programmable logic controllers, Railways, Safety-critical systems, Single-Input-Change, 2023 OA procedure",

author = "Wal, {Djurre van der} and Marcus Gerhold and Mari{\"e}lle Stoelinga",

note = "Funding Information: Acknowledgements. This paper is a product of the FormaSig project, fully funded by DB Netz AG and ProRail. The vision illustrated in this article reflects the personal views of the authors, and is not part of the strategy of DB Netz AG or ProRail. We thank the SIGNON Group (https://signon-group.com/) for providing access to the source code of the software simulator. Funding Information: This paper is a product of the FormaSig project, fully funded by DB Netz AG and ProRail. The vision illustrated in this article reflects the personal views of the authors, and is not part of the strategy of DB Netz AG or ProRail. We thank the SIGNON Group (https://signon-group.com/) for providing access to the source code of the software simulator. Publisher Copyright: {\textcopyright} 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 28th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2023, FMICS 2023 ; Conference date: 20-09-2023 Through 22-09-2023",

year = "2023",

month = sep,

day = "17",

doi = "10.1007/978-3-031-43681-9_14",

language = "English",

isbn = "978-3-031-43680-2",

series = "Lecture Notes in Computer Science book series",

pages = "242--258",

editor = "Alessandro Cimatti and Laura Titolo",

booktitle = "Formal Methods for Industrial Critical Systems",

}

Wal, DVD, Gerhold, M & Stoelinga, M 2023, Conformance in the Railway Industry: Single-Input-Change Testing a EULYNX Controller. in A Cimatti & L Titolo (eds), Formal Methods for Industrial Critical Systems: 28th International Conference, FMICS 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings. Lecture Notes in Computer Science book series, vol. 14290, pp. 242-258, 28th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2023, Antwerp, Belgium, 20/09/23. https://doi.org/10.1007/978-3-031-43681-9_14

Conformance in the Railway Industry: Single-Input-Change Testing a EULYNX Controller. / Wal, Djurre van der; Gerhold, Marcus ; Stoelinga, Mariëlle.
Formal Methods for Industrial Critical Systems: 28th International Conference, FMICS 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings. ed. / Alessandro Cimatti; Laura Titolo. 2023. p. 242-258 (Lecture Notes in Computer Science book series; Vol. 14290).

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

TY - CHAP

T1 - Conformance in the Railway Industry: Single-Input-Change Testing a EULYNX Controller

AU - Wal, Djurre van der

AU - Gerhold, Marcus

AU - Stoelinga, Mariëlle

N1 - Conference code: 28

PY - 2023/9/17

Y1 - 2023/9/17

N2 - We propose a novel framework for model-based testing against specifications from EULYNX, a SysML-based standard from the railway industry for the controllers of systems such as points, signals, sensors, and crossings. The main challenge here is the sheer complexity: with state spaces exceeding 10e+10 states, it is hard to derive test suites that achieve a meaningful type of coverage.We tackle this problem by moving away from the traditional interleaving semantics for SysML. Instead, we propose a synchronous semantics in terms of Finite State Machines (FSMs), leveraging the fact that EULYNX is implemented on Programmable Logic Controllers (PLCs). Then, we deploy Single-Input-Change Deterministic Finite State Machines (SIC-DFSMs), which ensures fully deterministic tests thus minimizing scalability issues.Our focus lies on the EULYNX specification for point controllers. The generated test suite achieves maximal transition coverage, but test execution time remains substantial. We introduce an additional test suite that achieves maximal transition label coverage. Remarkably, this smaller suite successfully identifies the same four faults as the larger suite.

AB - We propose a novel framework for model-based testing against specifications from EULYNX, a SysML-based standard from the railway industry for the controllers of systems such as points, signals, sensors, and crossings. The main challenge here is the sheer complexity: with state spaces exceeding 10e+10 states, it is hard to derive test suites that achieve a meaningful type of coverage.We tackle this problem by moving away from the traditional interleaving semantics for SysML. Instead, we propose a synchronous semantics in terms of Finite State Machines (FSMs), leveraging the fact that EULYNX is implemented on Programmable Logic Controllers (PLCs). Then, we deploy Single-Input-Change Deterministic Finite State Machines (SIC-DFSMs), which ensures fully deterministic tests thus minimizing scalability issues.Our focus lies on the EULYNX specification for point controllers. The generated test suite achieves maximal transition coverage, but test execution time remains substantial. We introduce an additional test suite that achieves maximal transition label coverage. Remarkably, this smaller suite successfully identifies the same four faults as the larger suite.

KW - Conformance testing

KW - Model-based testing

KW - Programmable logic controllers

KW - Railways

KW - Safety-critical systems

KW - Single-Input-Change

KW - 2023 OA procedure

U2 - 10.1007/978-3-031-43681-9_14

DO - 10.1007/978-3-031-43681-9_14

M3 - Chapter

SN - 978-3-031-43680-2

T3 - Lecture Notes in Computer Science book series

SP - 242

EP - 258

BT - Formal Methods for Industrial Critical Systems

A2 - Cimatti, Alessandro

A2 - Titolo, Laura

T2 - 28th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2023

Y2 - 20 September 2023 through 22 September 2023

ER -

Wal DVD, Gerhold M , Stoelinga M. Conformance in the Railway Industry: Single-Input-Change Testing a EULYNX Controller. In Cimatti A, Titolo L, editors, Formal Methods for Industrial Critical Systems: 28th International Conference, FMICS 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings. 2023. p. 242-258. (Lecture Notes in Computer Science book series). doi: 10.1007/978-3-031-43681-9_14