Formal Verification of OIL Component Specifications using mCRL2

Olav Bunte; Louis C.M. van Gool; Tim A.C. Willemse

doi:10.1007/978-3-030-58298-2_10

Formal Verification of OIL Component Specifications using mCRL2

Olav Bunte, Louis C.M. van Gool, Tim A.C. Willemse

Formal System Analysis

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

Abstract

To aid in making software bug-free, several high-tech companies are moving from coding to modelling. In some cases model checking techniques are explored or have already been adopted to get more value from these models. This also holds for Canon Production Printing, where the language OIL was developed for modelling control-software components. In this paper we present OIL and give its semantics. We define a translation from OIL to mCRL2 to enable the use of model checking techniques. Moreover, we discuss informal validity requirements on OIL component specifications and show how these can be formalised and verified using model checking. To test the feasibility of these techniques, we apply them to two models of systems used in production.

Original language	English
Title of host publication	Formal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Proceedings
Editors	Maurice H. ter Beek, Dejan Nickovic
Publisher	Springer
Pages	231-251
Number of pages	21
ISBN (Print)	9783030582975
DOIs	https://doi.org/10.1007/978-3-030-58298-2_10
Publication status	Published - 2020
Event	25th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2020 - Vienna, Austria Duration: 2 Sep 2020 → 3 Sep 2020

Publication series

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

Conference

Conference	25th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2020
Country	Austria
City	Vienna
Period	2/09/20 → 3/09/20

Access to Document

10.1007/978-3-030-58298-2_10

Link to publication in Scopus

Fingerprint Dive into the research topics of 'Formal Verification of OIL Component Specifications using mCRL2'. Together they form a unique fingerprint.

Cite this

Bunte, O., van Gool, L. C. M., & Willemse, T. A. C. (2020). Formal Verification of OIL Component Specifications using mCRL2. In M. H. ter Beek, & D. Nickovic (Eds.), Formal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Proceedings (pp. 231-251). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12327 LNCS). Springer. https://doi.org/10.1007/978-3-030-58298-2_10

Bunte, Olav ; van Gool, Louis C.M. ; Willemse, Tim A.C. / Formal Verification of OIL Component Specifications using mCRL2. Formal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Proceedings. editor / Maurice H. ter Beek ; Dejan Nickovic. Springer, 2020. pp. 231-251 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{e25f43f35e444d4bb93228ce6e7812fa,

title = "Formal Verification of OIL Component Specifications using mCRL2",

abstract = "To aid in making software bug-free, several high-tech companies are moving from coding to modelling. In some cases model checking techniques are explored or have already been adopted to get more value from these models. This also holds for Canon Production Printing, where the language OIL was developed for modelling control-software components. In this paper we present OIL and give its semantics. We define a translation from OIL to mCRL2 to enable the use of model checking techniques. Moreover, we discuss informal validity requirements on OIL component specifications and show how these can be formalised and verified using model checking. To test the feasibility of these techniques, we apply them to two models of systems used in production.",

author = "Olav Bunte and {van Gool}, {Louis C.M.} and Willemse, {Tim A.C.}",

year = "2020",

doi = "10.1007/978-3-030-58298-2_10",

language = "English",

isbn = "9783030582975",

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

publisher = "Springer",

pages = "231--251",

editor = "{ter Beek}, {Maurice H.} and Dejan Nickovic",

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

address = "Germany",

note = "25th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2020 ; Conference date: 02-09-2020 Through 03-09-2020",

}

Bunte, O , van Gool, LCM & Willemse, TAC 2020, Formal Verification of OIL Component Specifications using mCRL2. in MH ter Beek & D Nickovic (eds), Formal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12327 LNCS, Springer, pp. 231-251, 25th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2020, Vienna, Austria, 2/09/20. https://doi.org/10.1007/978-3-030-58298-2_10

Formal Verification of OIL Component Specifications using mCRL2. / Bunte, Olav ; van Gool, Louis C.M.; Willemse, Tim A.C.

Formal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Proceedings. ed. / Maurice H. ter Beek; Dejan Nickovic. Springer, 2020. p. 231-251 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12327 LNCS).

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

TY - GEN

T1 - Formal Verification of OIL Component Specifications using mCRL2

AU - Bunte, Olav

AU - van Gool, Louis C.M.

AU - Willemse, Tim A.C.

PY - 2020

Y1 - 2020

N2 - To aid in making software bug-free, several high-tech companies are moving from coding to modelling. In some cases model checking techniques are explored or have already been adopted to get more value from these models. This also holds for Canon Production Printing, where the language OIL was developed for modelling control-software components. In this paper we present OIL and give its semantics. We define a translation from OIL to mCRL2 to enable the use of model checking techniques. Moreover, we discuss informal validity requirements on OIL component specifications and show how these can be formalised and verified using model checking. To test the feasibility of these techniques, we apply them to two models of systems used in production.

AB - To aid in making software bug-free, several high-tech companies are moving from coding to modelling. In some cases model checking techniques are explored or have already been adopted to get more value from these models. This also holds for Canon Production Printing, where the language OIL was developed for modelling control-software components. In this paper we present OIL and give its semantics. We define a translation from OIL to mCRL2 to enable the use of model checking techniques. Moreover, we discuss informal validity requirements on OIL component specifications and show how these can be formalised and verified using model checking. To test the feasibility of these techniques, we apply them to two models of systems used in production.

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

U2 - 10.1007/978-3-030-58298-2_10

DO - 10.1007/978-3-030-58298-2_10

M3 - Conference contribution

AN - SCOPUS:85091287799

SN - 9783030582975

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

SP - 231

EP - 251

BT - Formal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Proceedings

A2 - ter Beek, Maurice H.

A2 - Nickovic, Dejan

PB - Springer

T2 - 25th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2020

Y2 - 2 September 2020 through 3 September 2020

ER -

Bunte O , van Gool LCM , Willemse TAC. Formal Verification of OIL Component Specifications using mCRL2. In ter Beek MH, Nickovic D, editors, Formal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Proceedings. Springer. 2020. p. 231-251. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-58298-2_10