Formal verification of an industrial UML-like model using mCRL2 (extended version)

Anna Stramaglia; Jeroen J. A. Keiren

Formal verification of an industrial UML-like model using mCRL2 (extended version)

Anna Stramaglia, Jeroen J. A. Keiren

Formal System Analysis

Research output: Working paper › Preprint › Academic

44 Downloads (Pure)

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
Publication status	Published - 17 May 2022

Bibliographical note

pre-print of a paper that is submitted to FMICS 2022

Keywords

eess.SY
cs.LO
cs.SY

Access to Document

2205.08146v1

1 Conference contribution

Formal Verification of an Industrial UML-like Model using mCRL2
Stramaglia, A. & Keiren, J. J. A., 2022, Formal Methods for Industrial Critical Systems - 27th International Conference, FMICS 2022, Proceedings. Groote, J. F. & Huisman, M. (eds.). Springer, p. 86-102 17 p. (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

Cite this

@techreport{537f496ac57a426d9d05f0fdbc93dd1c,

title = "Formal verification of an industrial UML-like model using mCRL2 (extended version)",

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. ",

keywords = "eess.SY, cs.LO, cs.SY",

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

note = "pre-print of a paper that is submitted to FMICS 2022",

year = "2022",

month = may,

day = "17",

language = "English",

type = "WorkingPaper",

}

TY - UNPB

T1 - Formal verification of an industrial UML-like model using mCRL2 (extended version)

AU - Stramaglia, Anna

AU - Keiren, Jeroen J. A.

N1 - pre-print of a paper that is submitted to FMICS 2022

PY - 2022/5/17

Y1 - 2022/5/17

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.

KW - eess.SY

KW - cs.LO

KW - cs.SY

M3 - Preprint

BT - Formal verification of an industrial UML-like model using mCRL2 (extended version)

ER -

Formal verification of an industrial UML-like model using mCRL2 (extended version)

Abstract

Bibliographical note

Keywords

Access to Document

Fingerprint

Research output

Formal Verification of an Industrial UML-like Model using mCRL2

Cite this