Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Oeritte: User-Friendly Counterexample Explanation for Model Checking
Computer Technologies Laboratory, ITMO University, 197101 Saint Petersburg, Russia; Department of Electrical Engineering and Automation, Aalto University, 02150 Espoo, Finland.
Computer Technologies Laboratory, ITMO University, 197101 Saint Petersburg, Russia; Department of Electrical Engineering and Automation, Aalto University, 02150 Espoo, Finland.
VTT Technical Research Centre of Finland Ltd., 02044 Espoo, Finland.
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Computer Science. Computer Technologies Laboratory, ITMO University, 197101 Saint Petersburg, Russia; Department of Electrical Engineering and Automation, Aalto University, 02150 Espoo, Finland.ORCID iD: 0000-0002-9315-9920
2021 (English)In: IEEE Access, E-ISSN 2169-3536, Vol. 9, p. 61383-61397Article in journal (Refereed) Published
Abstract [en]

Thorough verification is a part of the design process of instrumentation and control systems if they must comply with crucial safety requirements. Model checking can be applied to the formal model of such a system to reason about its correctness based on the specification provided. When a violation occurs, the model checking tool outputs the proof of the violation in the form of a failure trace, which represents a state sequence of system model transitions where the requirement does not hold. This sequence, however, even for modular systems, is a mere table of values. Due to the lack of any insights into the inner model processes and structures that caused a problem, the debugging process of the formal model becomes time and effort consuming. The tool presented in this paper, Oeritte, is aimed at assisting the analyst in this challenge. It implements a method for automatic visual counterexample explanation which includes reasoning both over the falsified LTL formula and over the NuSMV function block diagram of the formal model of the system. The tool is applied to an industrial-sized safety control system of a nuclear power plant.

Place, publisher, year, edition, pages
IEEE, 2021. Vol. 9, p. 61383-61397
Keywords [en]
Counterexample explanation, counterexample visualization, function block diagram, NuSMV, user-friendly model checking
National Category
Computer Systems
Research subject
Dependable Communication and Computation Systems
Identifiers
URN: urn:nbn:se:ltu:diva-84134DOI: 10.1109/ACCESS.2021.3073459ISI: 000645048000001Scopus ID: 2-s2.0-85104629291OAI: oai:DiVA.org:ltu-84134DiVA, id: diva2:1549266
Note

Validerad;2021;Nivå 2;2021-05-05 (alebob);

Finansiär: Finnish Research Programme on Nuclear Power Plant Safety 2018–2022 (SAFIR 2022); Government of the Russian Federation (08-08)

Available from: 2021-05-05 Created: 2021-05-05 Last updated: 2022-04-13Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Vyatkin, Valeriy

Search in DiVA

By author/editor
Vyatkin, Valeriy
By organisation
Computer Science
In the same journal
IEEE Access
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 47 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf