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 -