Formal Verification of an Industrial UML-like Model using mCRL2

Anna Stramaglia; Jeroen J.A. Keiren

doi:10.1007/978-3-031-15008-1_7

Formal Verification of an Industrial UML-like Model using mCRL2

Anna Stramaglia, Jeroen J.A. Keiren

Formal System Analysis

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

Abstract

Low-code development platforms are gaining popularity. Essentially, such platforms allow to shift from coding to graphical modeling, helping to improve quality and reduce development time. The Cordis SUITE is a low-code development platform that adopts the Unified Modeling Language (UML) to design complex machine-control applications. In this paper we introduce Cordis models and their semantics. To enable formal verification, we define an automatic translation of Cordis models to the process algebraic specification language mCRL2. As a proof of concept, we describe requirements of the control software of an industrial cylinder model developed by Cordis, and show how these can be verified using model checking. We show that our verification approach is effective to uncover subtle issues in the industrial model and its implementation.

Original language	English
Title of host publication	Formal Methods for Industrial Critical Systems - 27th International Conference, FMICS 2022, Proceedings
Editors	Jan Friso Groote, Marieke Huisman
Publisher	Springer
Pages	86-102
Number of pages	17
ISBN (Print)	9783031150074
DOIs	https://doi.org/10.1007/978-3-031-15008-1_7
Publication status	Published - 2022
Event	27th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2022 - Warsaw, Poland Duration: 14 Sept 2022 → 15 Sept 2022

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13487 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	27th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2022
Country/Territory	Poland
City	Warsaw
Period	14/09/22 → 15/09/22

Bibliographical note

Funding Information:
This work was supported partially by the MACHINAIDE project (ITEA3, No. 18030) and through EU regional development funding in the context of the OP-Zuid program (No. 02541). We thank Wieger Wesselink and Yousra Hafidi for contributions to the development of the mCRL2 translation, and Cordis Automation B.V. for their feedback on earlier versions of this paper.

Funding Information:
Acknowledgements. This work was supported partially by the MACHINAIDE project (ITEA3, No. 18030) and through EU regional development funding in the context of the OP-Zuid program (No. 02541). We thank Wieger Wesselink and Yousra Hafidi for contributions to the development of the mCRL2 translation, and Cordis Automation B.V. for their feedback on earlier versions of this paper.

Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Access to Document

10.1007/978-3-031-15008-1_7

Cite this

Stramaglia, A., & Keiren, J. J. A. (2022). Formal Verification of an Industrial UML-like Model using mCRL2. In J. F. Groote, & M. Huisman (Eds.), Formal Methods for Industrial Critical Systems - 27th International Conference, FMICS 2022, Proceedings (pp. 86-102). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13487 LNCS). Springer. https://doi.org/10.1007/978-3-031-15008-1_7

Stramaglia, Anna ; Keiren, Jeroen J.A. / Formal Verification of an Industrial UML-like Model using mCRL2. Formal Methods for Industrial Critical Systems - 27th International Conference, FMICS 2022, Proceedings. editor / Jan Friso Groote ; Marieke Huisman. Springer, 2022. pp. 86-102 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{033f7357a90a4909b4eb58d61cd1e84e,

title = "Formal Verification of an Industrial UML-like Model using mCRL2",

abstract = "Low-code development platforms are gaining popularity. Essentially, such platforms allow to shift from coding to graphical modeling, helping to improve quality and reduce development time. The Cordis SUITE is a low-code development platform that adopts the Unified Modeling Language (UML) to design complex machine-control applications. In this paper we introduce Cordis models and their semantics. To enable formal verification, we define an automatic translation of Cordis models to the process algebraic specification language mCRL2. As a proof of concept, we describe requirements of the control software of an industrial cylinder model developed by Cordis, and show how these can be verified using model checking. We show that our verification approach is effective to uncover subtle issues in the industrial model and its implementation.",

author = "Anna Stramaglia and Keiren, {Jeroen J.A.}",

note = "Funding Information: This work was supported partially by the MACHINAIDE project (ITEA3, No. 18030) and through EU regional development funding in the context of the OP-Zuid program (No. 02541). We thank Wieger Wesselink and Yousra Hafidi for contributions to the development of the mCRL2 translation, and Cordis Automation B.V. for their feedback on earlier versions of this paper. Funding Information: Acknowledgements. This work was supported partially by the MACHINAIDE project (ITEA3, No. 18030) and through EU regional development funding in the context of the OP-Zuid program (No. 02541). We thank Wieger Wesselink and Yousra Hafidi for contributions to the development of the mCRL2 translation, and Cordis Automation B.V. for their feedback on earlier versions of this paper. Publisher Copyright: {\textcopyright} 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 27th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2022 ; Conference date: 14-09-2022 Through 15-09-2022",

year = "2022",

doi = "10.1007/978-3-031-15008-1_7",

language = "English",

isbn = "9783031150074",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "86--102",

editor = "Groote, {Jan Friso} and Marieke Huisman",

booktitle = "Formal Methods for Industrial Critical Systems - 27th International Conference, FMICS 2022, Proceedings",

}

Stramaglia, A & Keiren, JJA 2022, Formal Verification of an Industrial UML-like Model using mCRL2. in JF Groote & M Huisman (eds), Formal Methods for Industrial Critical Systems - 27th International Conference, FMICS 2022, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13487 LNCS, Springer, pp. 86-102, 27th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2022, Warsaw, Poland, 14/09/22. https://doi.org/10.1007/978-3-031-15008-1_7

Formal Verification of an Industrial UML-like Model using mCRL2. / Stramaglia, Anna ; Keiren, Jeroen J.A.
Formal Methods for Industrial Critical Systems - 27th International Conference, FMICS 2022, Proceedings. ed. / Jan Friso Groote; Marieke Huisman. Springer, 2022. p. 86-102 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13487 LNCS).

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

TY - GEN

T1 - Formal Verification of an Industrial UML-like Model using mCRL2

AU - Stramaglia, Anna

AU - Keiren, Jeroen J.A.

N1 - Funding Information: This work was supported partially by the MACHINAIDE project (ITEA3, No. 18030) and through EU regional development funding in the context of the OP-Zuid program (No. 02541). We thank Wieger Wesselink and Yousra Hafidi for contributions to the development of the mCRL2 translation, and Cordis Automation B.V. for their feedback on earlier versions of this paper. Funding Information: Acknowledgements. This work was supported partially by the MACHINAIDE project (ITEA3, No. 18030) and through EU regional development funding in the context of the OP-Zuid program (No. 02541). We thank Wieger Wesselink and Yousra Hafidi for contributions to the development of the mCRL2 translation, and Cordis Automation B.V. for their feedback on earlier versions of this paper. Publisher Copyright: © 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

PY - 2022

Y1 - 2022

N2 - Low-code development platforms are gaining popularity. Essentially, such platforms allow to shift from coding to graphical modeling, helping to improve quality and reduce development time. The Cordis SUITE is a low-code development platform that adopts the Unified Modeling Language (UML) to design complex machine-control applications. In this paper we introduce Cordis models and their semantics. To enable formal verification, we define an automatic translation of Cordis models to the process algebraic specification language mCRL2. As a proof of concept, we describe requirements of the control software of an industrial cylinder model developed by Cordis, and show how these can be verified using model checking. We show that our verification approach is effective to uncover subtle issues in the industrial model and its implementation.

AB - Low-code development platforms are gaining popularity. Essentially, such platforms allow to shift from coding to graphical modeling, helping to improve quality and reduce development time. The Cordis SUITE is a low-code development platform that adopts the Unified Modeling Language (UML) to design complex machine-control applications. In this paper we introduce Cordis models and their semantics. To enable formal verification, we define an automatic translation of Cordis models to the process algebraic specification language mCRL2. As a proof of concept, we describe requirements of the control software of an industrial cylinder model developed by Cordis, and show how these can be verified using model checking. We show that our verification approach is effective to uncover subtle issues in the industrial model and its implementation.

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

U2 - 10.1007/978-3-031-15008-1_7

DO - 10.1007/978-3-031-15008-1_7

M3 - Conference contribution

AN - SCOPUS:85137987748

SN - 9783031150074

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 86

EP - 102

BT - Formal Methods for Industrial Critical Systems - 27th International Conference, FMICS 2022, Proceedings

A2 - Groote, Jan Friso

A2 - Huisman, Marieke

PB - Springer

T2 - 27th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2022

Y2 - 14 September 2022 through 15 September 2022

ER -

Stramaglia A , Keiren JJA. Formal Verification of an Industrial UML-like Model using mCRL2. In Groote JF, Huisman M, editors, Formal Methods for Industrial Critical Systems - 27th International Conference, FMICS 2022, Proceedings. Springer. 2022. p. 86-102. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-15008-1_7