A Formalisation of SysML State Machines in mCRL2

Mark Bouwman; Bas Luttik; Djurre van der Wal

doi:10.1007/978-3-030-78089-0_3

A Formalisation of SysML State Machines in mCRL2

Mark Bouwman (Corresponding author)
, Bas Luttik
, Djurre van der Wal

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

8 Citations (Scopus)

9 Downloads (Pure)

Abstract

This paper reports on a formalisation of the semi-formal modelling language SysML in the formal language mCRL2, in order to unlock formal verification and model-based testing using the mCRL2 toolset for SysML models. The formalisation focuses on a fragment of SysML used in the railway standardisation project EULYNX. It comprises the semantics of state machines, communication between objects via ports, and an action language called ASAL. It turns out that the generic execution model of SysML state machines can be elegantly specified using the rich data and process languages of mCRL2. This is a big step towards an automated translation as the generic model can be configured with a formal description of a specific set of state machines in a straightforward manner.

Original language	English
Title of host publication	Formal Techniques for Distributed Objects, Components, and Systems
Subtitle of host publication	41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14–18, 2021, Proceedings
Editors	Kirstin Peters, Tim A. Willemse
Place of Publication	Cham
Publisher	Springer
Pages	42-59
Number of pages	18
ISBN (Electronic)	978-3-030-78089-0
ISBN (Print)	978-3-030-78088-3
DOIs	https://doi.org/10.1007/978-3-030-78089-0_3
Publication status	Published - 8 Jun 2021
Event	41st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2021 held as part of 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021 - Virtual, Online Duration: 14 Jun 2021 → 18 Jun 2021

Publication series

Name	Lecture Notes in Computer Science (LNCS)
Volume	12719
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	41st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2021 held as part of 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021
City	Virtual, Online
Period	14/06/21 → 18/06/21

Funding

Acknowledgement. FormaSig and, by extension, this work are fully funded by Pro-Rail and DB Netz AG. The vision presented in this article does not necessarily reflect the strategy of DB Netz AG or ProRail, but reflects the personal views of the authors. FormaSig and, by extension, this work are fully funded by Pro-Rail and DB Netz AG. The vision presented in this article does not necessarily reflect the strategy of DB Netz AG or ProRail, but reflects the personal views of the authors. We also thank the anonymous reviewers for their constructive suggestions, which led to improvements of the paper.

Access to Document

10.1007/978-3-030-78089-0_3

pdfFinal published version, 614 KBLicence: TAVERNE

Cite this

Bouwman, M., Luttik, B., & van der Wal, D. (2021). A Formalisation of SysML State Machines in mCRL2. In K. Peters, & T. A. Willemse (Eds.), Formal Techniques for Distributed Objects, Components, and Systems: 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14–18, 2021, Proceedings (pp. 42-59). (Lecture Notes in Computer Science (LNCS); Vol. 12719). Springer. https://doi.org/10.1007/978-3-030-78089-0_3

Bouwman, Mark ; Luttik, Bas ; van der Wal, Djurre. / A Formalisation of SysML State Machines in mCRL2. Formal Techniques for Distributed Objects, Components, and Systems: 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14–18, 2021, Proceedings. editor / Kirstin Peters ; Tim A. Willemse. Cham : Springer, 2021. pp. 42-59 (Lecture Notes in Computer Science (LNCS)).

@inproceedings{ac3f7cb81c4c4408876519e3d89cd8eb,

title = "A Formalisation of SysML State Machines in mCRL2",

abstract = "This paper reports on a formalisation of the semi-formal modelling language SysML in the formal language mCRL2, in order to unlock formal verification and model-based testing using the mCRL2 toolset for SysML models. The formalisation focuses on a fragment of SysML used in the railway standardisation project EULYNX. It comprises the semantics of state machines, communication between objects via ports, and an action language called ASAL. It turns out that the generic execution model of SysML state machines can be elegantly specified using the rich data and process languages of mCRL2. This is a big step towards an automated translation as the generic model can be configured with a formal description of a specific set of state machines in a straightforward manner.",

author = "Mark Bouwman and Bas Luttik and \{van der Wal\}, Djurre",

note = "Funding Information: Acknowledgement. FormaSig and, by extension, this work are fully funded by Pro-Rail and DB Netz AG. The vision presented in this article does not necessarily reflect the strategy of DB Netz AG or ProRail, but reflects the personal views of the authors. Funding Information: FormaSig and, by extension, this work are fully funded by Pro-Rail and DB Netz AG. The vision presented in this article does not necessarily reflect the strategy of DB Netz AG or ProRail, but reflects the personal views of the authors. We also thank the anonymous reviewers for their constructive suggestions, which led to improvements of the paper. Publisher Copyright: {\textcopyright} 2021, IFIP International Federation for Information Processing.; 41st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2021 held as part of 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021 ; Conference date: 14-06-2021 Through 18-06-2021",

year = "2021",

month = jun,

day = "8",

doi = "10.1007/978-3-030-78089-0\_3",

language = "English",

isbn = "978-3-030-78088-3",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "42--59",

editor = "Kirstin Peters and Willemse, \{Tim A.\}",

booktitle = "Formal Techniques for Distributed Objects, Components, and Systems",

address = "Germany",

}

Bouwman, M , Luttik, B & van der Wal, D 2021, A Formalisation of SysML State Machines in mCRL2. in K Peters & TA Willemse (eds), Formal Techniques for Distributed Objects, Components, and Systems: 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14–18, 2021, Proceedings. Lecture Notes in Computer Science (LNCS), vol. 12719, Springer, Cham, pp. 42-59, 41st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2021 held as part of 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Virtual, Online, 14/06/21. https://doi.org/10.1007/978-3-030-78089-0_3

A Formalisation of SysML State Machines in mCRL2. / Bouwman, Mark (Corresponding author); Luttik, Bas; van der Wal, Djurre.
Formal Techniques for Distributed Objects, Components, and Systems: 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14–18, 2021, Proceedings. ed. / Kirstin Peters; Tim A. Willemse. Cham: Springer, 2021. p. 42-59 (Lecture Notes in Computer Science (LNCS); Vol. 12719).

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

TY - GEN

T1 - A Formalisation of SysML State Machines in mCRL2

AU - Bouwman, Mark

AU - Luttik, Bas

AU - van der Wal, Djurre

N1 - Funding Information: Acknowledgement. FormaSig and, by extension, this work are fully funded by Pro-Rail and DB Netz AG. The vision presented in this article does not necessarily reflect the strategy of DB Netz AG or ProRail, but reflects the personal views of the authors. Funding Information: FormaSig and, by extension, this work are fully funded by Pro-Rail and DB Netz AG. The vision presented in this article does not necessarily reflect the strategy of DB Netz AG or ProRail, but reflects the personal views of the authors. We also thank the anonymous reviewers for their constructive suggestions, which led to improvements of the paper. Publisher Copyright: © 2021, IFIP International Federation for Information Processing.

PY - 2021/6/8

Y1 - 2021/6/8

N2 - This paper reports on a formalisation of the semi-formal modelling language SysML in the formal language mCRL2, in order to unlock formal verification and model-based testing using the mCRL2 toolset for SysML models. The formalisation focuses on a fragment of SysML used in the railway standardisation project EULYNX. It comprises the semantics of state machines, communication between objects via ports, and an action language called ASAL. It turns out that the generic execution model of SysML state machines can be elegantly specified using the rich data and process languages of mCRL2. This is a big step towards an automated translation as the generic model can be configured with a formal description of a specific set of state machines in a straightforward manner.

AB - This paper reports on a formalisation of the semi-formal modelling language SysML in the formal language mCRL2, in order to unlock formal verification and model-based testing using the mCRL2 toolset for SysML models. The formalisation focuses on a fragment of SysML used in the railway standardisation project EULYNX. It comprises the semantics of state machines, communication between objects via ports, and an action language called ASAL. It turns out that the generic execution model of SysML state machines can be elegantly specified using the rich data and process languages of mCRL2. This is a big step towards an automated translation as the generic model can be configured with a formal description of a specific set of state machines in a straightforward manner.

UR - https://www.scopus.com/pages/publications/85111347532

U2 - 10.1007/978-3-030-78089-0_3

DO - 10.1007/978-3-030-78089-0_3

M3 - Conference contribution

AN - SCOPUS:85111347532

SN - 978-3-030-78088-3

T3 - Lecture Notes in Computer Science (LNCS)

SP - 42

EP - 59

BT - Formal Techniques for Distributed Objects, Components, and Systems

A2 - Peters, Kirstin

A2 - Willemse, Tim A.

PB - Springer

CY - Cham

T2 - 41st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2021 held as part of 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021

Y2 - 14 June 2021 through 18 June 2021

ER -

Bouwman M , Luttik B, van der Wal D. A Formalisation of SysML State Machines in mCRL2. In Peters K, Willemse TA, editors, Formal Techniques for Distributed Objects, Components, and Systems: 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14–18, 2021, Proceedings. Cham: Springer. 2021. p. 42-59. (Lecture Notes in Computer Science (LNCS)). doi: 10.1007/978-3-030-78089-0_3

A Formalisation of SysML State Machines in mCRL2

Abstract

Publication series

Conference

Funding

Access to Document

Other files and links

Fingerprint

Cite this