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 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 |
|---|---|
| Pages (from-to) | 441-472 |
| Number of pages | 32 |
| Journal | International Journal on Software Tools for Technology Transfer |
| Volume | 24 |
| Issue number | 3 |
| DOIs | |
| Publication status | Published - Jun 2022 |
Bibliographical note
Funding Information:This work was carried out as part of the VOICE-B project, which is funded by Canon Production Printing.
Funding
This work was carried out as part of the VOICE-B project, which is funded by Canon Production Printing.
Keywords
- Domain specific languages
- Model checking
- Model transformation
- Verification
Fingerprint
Dive into the research topics of 'Formal verification of OIL component specifications using mCRL2'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver