What is the point: Formal analysis and test generation for a railway standard

Mark Bouwman; Djurre van der Wal; Bas Luttik; Mariëlle Stoelinga; Arend Rensink

doi:10.3850/978-981-14-8593-0_4410-cd

What is the point: Formal analysis and test generation for a railway standard

Mark Bouwman, Djurre van der Wal, Bas Luttik, Mariëlle Stoelinga, Arend Rensink

Formal Methods and Tools

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

4 Citations (Scopus)

127 Downloads (Pure)

Abstract

EULYNX is an EU-level collaboration between railway infrastructure managers to standardize signaling interfaces. The main goal of EULYNX is to provide, on an EU scale, a modular and flexible railroad architecture where components can easily be exchanged. This also opens the market for specialized manufacturers that do not supply the full range of control assets, but only single components. Related to EULYNX is FormaSig, an effort to establish the safety of the EULYNX standard with mathematical rigor. In particular, one of the main objectives of FormaSig is to translate the entire EULYNX standard from the semi-formal language SysML to the formal language mCRL2. The resulting mCRL2 models will subsequently be checked for important safety requirements and used for automated testing of actual EULYNX systems. This paper presents a first case study in this direction, focusing on the EULYNX Point interface, which we have converted to an mCRL2 model. We have also derived nine safety requirements, which have all been automatically compared with the mCRL2 model. Finally, we have used the mCRL2 model to test an industrial simulator of the EULYNX Point interface fully automatically.

Original language	English
Title of host publication	Proceedings of the 30th European Safety and Reliability Conference and the 15th Probabilistic Safety Assessment and Management Conference
Editors	Piero Baraldi, Francesco Di Maio, Enrico Zio
Place of Publication	Singapore
Publisher	Research Publishing Services
Pages	921-928
Number of pages	8
ISBN (Print)	978-981-14-8593-0
DOIs	https://doi.org/10.3850/978-981-14-8593-0_4410-cd
Publication status	Published - Nov 2020
Event	30th European Safety and Reliability Conference, ESREL 2020 and 15th Probabilistic Safety Assessment and Management Conference, PSAM 2020 - Venice, Virtual, Italy Duration: 1 Nov 2020 → 5 Nov 2020 https://www.esrel2020-psam15.org/

Conference

Conference	30th European Safety and Reliability Conference, ESREL 2020 and 15th Probabilistic Safety Assessment and Management Conference, PSAM 2020
Abbreviated title	ESREL 2020 PSAM 15
Country/Territory	Italy
City	Venice, Virtual
Period	1/11/20 → 5/11/20
Internet address	https://www.esrel2020-psam15.org/

Keywords

Formal analysis
MCRL2
Railway systems
SysML
Test automation
22/2 OA procedure

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.3850/978-981-14-8593-0_4410-cd

Bouwman2020whatFinal published version, 202 KBLicence: Taverne

Cite this

Bouwman, M., van der Wal, D., Luttik, B., Stoelinga, M., & Rensink, A. (2020). What is the point: Formal analysis and test generation for a railway standard. In P. Baraldi, F. Di Maio, & E. Zio (Eds.), Proceedings of the 30th European Safety and Reliability Conference and the 15th Probabilistic Safety Assessment and Management Conference (pp. 921-928). Research Publishing Services. https://doi.org/10.3850/978-981-14-8593-0_4410-cd

Bouwman, Mark ; van der Wal, Djurre ; Luttik, Bas et al. / What is the point : Formal analysis and test generation for a railway standard. Proceedings of the 30th European Safety and Reliability Conference and the 15th Probabilistic Safety Assessment and Management Conference. editor / Piero Baraldi ; Francesco Di Maio ; Enrico Zio. Singapore : Research Publishing Services, 2020. pp. 921-928

@inproceedings{646367b0701e4200880382bea0e6e7bd,

title = "What is the point: Formal analysis and test generation for a railway standard",

abstract = "EULYNX is an EU-level collaboration between railway infrastructure managers to standardize signaling interfaces. The main goal of EULYNX is to provide, on an EU scale, a modular and flexible railroad architecture where components can easily be exchanged. This also opens the market for specialized manufacturers that do not supply the full range of control assets, but only single components. Related to EULYNX is FormaSig, an effort to establish the safety of the EULYNX standard with mathematical rigor. In particular, one of the main objectives of FormaSig is to translate the entire EULYNX standard from the semi-formal language SysML to the formal language mCRL2. The resulting mCRL2 models will subsequently be checked for important safety requirements and used for automated testing of actual EULYNX systems. This paper presents a first case study in this direction, focusing on the EULYNX Point interface, which we have converted to an mCRL2 model. We have also derived nine safety requirements, which have all been automatically compared with the mCRL2 model. Finally, we have used the mCRL2 model to test an industrial simulator of the EULYNX Point interface fully automatically.",

keywords = "Formal analysis, MCRL2, Railway systems, SysML, Test automation, 22/2 OA procedure",

author = "Mark Bouwman and {van der Wal}, Djurre and Bas Luttik and Mari{\"e}lle Stoelinga and Arend Rensink",

note = "Funding Information: FormaSig and this work (by extension) are fully funded by DB Netz AG and ProRail; at the same time, the vision illustrated in this article is not part of the strategy of DB Netz AG or ProRail, but reflects the personal views of the authors. Publisher Copyright: {\textcopyright} ESREL2020-PSAM15 Organizers.Published by Research Publishing, Singapore.; 30th European Safety and Reliability Conference, ESREL 2020 and 15th Probabilistic Safety Assessment and Management Conference, PSAM 2020, ESREL 2020 PSAM 15 ; Conference date: 01-11-2020 Through 05-11-2020",

year = "2020",

month = nov,

doi = "10.3850/978-981-14-8593-0_4410-cd",

language = "English",

isbn = "978-981-14-8593-0",

pages = "921--928",

editor = "Piero Baraldi and {Di Maio}, Francesco and Enrico Zio",

booktitle = "Proceedings of the 30th European Safety and Reliability Conference and the 15th Probabilistic Safety Assessment and Management Conference",

publisher = "Research Publishing Services",

url = "https://www.esrel2020-psam15.org/",

}

Bouwman, M, van der Wal, D, Luttik, B, Stoelinga, M & Rensink, A 2020, What is the point: Formal analysis and test generation for a railway standard. in P Baraldi, F Di Maio & E Zio (eds), Proceedings of the 30th European Safety and Reliability Conference and the 15th Probabilistic Safety Assessment and Management Conference. Research Publishing Services, Singapore, pp. 921-928, 30th European Safety and Reliability Conference, ESREL 2020 and 15th Probabilistic Safety Assessment and Management Conference, PSAM 2020, Venice, Virtual, Italy, 1/11/20. https://doi.org/10.3850/978-981-14-8593-0_4410-cd

What is the point: Formal analysis and test generation for a railway standard. / Bouwman, Mark; van der Wal, Djurre; Luttik, Bas et al.
Proceedings of the 30th European Safety and Reliability Conference and the 15th Probabilistic Safety Assessment and Management Conference. ed. / Piero Baraldi; Francesco Di Maio; Enrico Zio. Singapore: Research Publishing Services, 2020. p. 921-928.

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

TY - GEN

T1 - What is the point

T2 - 30th European Safety and Reliability Conference, ESREL 2020 and 15th Probabilistic Safety Assessment and Management Conference, PSAM 2020

AU - Bouwman, Mark

AU - van der Wal, Djurre

AU - Luttik, Bas

AU - Stoelinga, Mariëlle

AU - Rensink, Arend

N1 - Funding Information: FormaSig and this work (by extension) are fully funded by DB Netz AG and ProRail; at the same time, the vision illustrated in this article is not part of the strategy of DB Netz AG or ProRail, but reflects the personal views of the authors. Publisher Copyright: © ESREL2020-PSAM15 Organizers.Published by Research Publishing, Singapore.

PY - 2020/11

Y1 - 2020/11

N2 - EULYNX is an EU-level collaboration between railway infrastructure managers to standardize signaling interfaces. The main goal of EULYNX is to provide, on an EU scale, a modular and flexible railroad architecture where components can easily be exchanged. This also opens the market for specialized manufacturers that do not supply the full range of control assets, but only single components. Related to EULYNX is FormaSig, an effort to establish the safety of the EULYNX standard with mathematical rigor. In particular, one of the main objectives of FormaSig is to translate the entire EULYNX standard from the semi-formal language SysML to the formal language mCRL2. The resulting mCRL2 models will subsequently be checked for important safety requirements and used for automated testing of actual EULYNX systems. This paper presents a first case study in this direction, focusing on the EULYNX Point interface, which we have converted to an mCRL2 model. We have also derived nine safety requirements, which have all been automatically compared with the mCRL2 model. Finally, we have used the mCRL2 model to test an industrial simulator of the EULYNX Point interface fully automatically.

AB - EULYNX is an EU-level collaboration between railway infrastructure managers to standardize signaling interfaces. The main goal of EULYNX is to provide, on an EU scale, a modular and flexible railroad architecture where components can easily be exchanged. This also opens the market for specialized manufacturers that do not supply the full range of control assets, but only single components. Related to EULYNX is FormaSig, an effort to establish the safety of the EULYNX standard with mathematical rigor. In particular, one of the main objectives of FormaSig is to translate the entire EULYNX standard from the semi-formal language SysML to the formal language mCRL2. The resulting mCRL2 models will subsequently be checked for important safety requirements and used for automated testing of actual EULYNX systems. This paper presents a first case study in this direction, focusing on the EULYNX Point interface, which we have converted to an mCRL2 model. We have also derived nine safety requirements, which have all been automatically compared with the mCRL2 model. Finally, we have used the mCRL2 model to test an industrial simulator of the EULYNX Point interface fully automatically.

KW - Formal analysis

KW - MCRL2

KW - Railway systems

KW - SysML

KW - Test automation

KW - 22/2 OA procedure

UR - http://www.scopus.com/inward/record.url?scp=85107292800&partnerID=8YFLogxK

U2 - 10.3850/978-981-14-8593-0_4410-cd

DO - 10.3850/978-981-14-8593-0_4410-cd

M3 - Conference contribution

AN - SCOPUS:85107292800

SN - 978-981-14-8593-0

SP - 921

EP - 928

BT - Proceedings of the 30th European Safety and Reliability Conference and the 15th Probabilistic Safety Assessment and Management Conference

A2 - Baraldi, Piero

A2 - Di Maio, Francesco

A2 - Zio, Enrico

PB - Research Publishing Services

CY - Singapore

Y2 - 1 November 2020 through 5 November 2020

ER -

Bouwman M, van der Wal D, Luttik B, Stoelinga M , Rensink A. What is the point: Formal analysis and test generation for a railway standard. In Baraldi P, Di Maio F, Zio E, editors, Proceedings of the 30th European Safety and Reliability Conference and the 15th Probabilistic Safety Assessment and Management Conference. Singapore: Research Publishing Services. 2020. p. 921-928 doi: 10.3850/978-981-14-8593-0_4410-cd

What is the point: Formal analysis and test generation for a railway standard

Abstract

Conference

Keywords

UN SDGs

Access to Document

Other files and links

Fingerprint

Cite this