Formal Verification of OIL Component Specifications using mCRL2

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-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 languageEnglish
Title of host publicationFormal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Proceedings
EditorsMaurice H. ter Beek, Dejan Nickovic
PublisherSpringer
Pages231-251
Number of pages21
ISBN (Print)9783030582975
DOIs
Publication statusPublished - 2020
Event25th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2020 - Vienna, Austria
Duration: 2 Sep 20203 Sep 2020

Publication series

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

Conference

Conference25th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2020
CountryAustria
CityVienna
Period2/09/203/09/20

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

Cite this