Formal verification of OIL component specifications using mCRL2

Olav Bunte (Corresponding author), Louis C.M. van Gool (Corresponding author), Tim A.C. Willemse (Corresponding author)

Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

2 Citaten (Scopus)
88 Downloads (Pure)


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

Originele taal-2Engels
Pagina's (van-tot)441-472
Aantal pagina's32
TijdschriftInternational Journal on Software Tools for Technology Transfer
Nummer van het tijdschrift3
StatusGepubliceerd - jun. 2022

Bibliografische nota

Publisher Copyright:
© 2022, The Author(s).


Duik in de onderzoeksthema's van 'Formal verification of OIL component specifications using mCRL2'. Samen vormen ze een unieke vingerafdruk.

Citeer dit