Formal Verification of OIL Component Specifications using mCRL2

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

1 Citaat (Scopus)

Samenvatting

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.

Originele taal-2Engels
TitelFormal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Proceedings
RedacteurenMaurice H. ter Beek, Dejan Nickovic
UitgeverijSpringer
Pagina's231-251
Aantal pagina's21
ISBN van geprinte versie9783030582975
DOI's
StatusGepubliceerd - 2020
Evenement25th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2020 - Vienna, Oostenrijk
Duur: 2 sep. 20203 sep. 2020

Publicatie series

NaamLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12327 LNCS
ISSN van geprinte versie0302-9743
ISSN van elektronische versie1611-3349

Congres

Congres25th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2020
Land/RegioOostenrijk
StadVienna
Periode2/09/203/09/20

Vingerafdruk

Duik in de onderzoeksthema's van 'Formal Verification of OIL Component Specifications using mCRL2'. Samen vormen ze een unieke vingerafdruk.

Citeer dit