Oeritte: User-Friendly Counterexample Explanation for Model Checking
No Thumbnail Available
Access rights
openAccess
URL
Journal Title
Journal ISSN
Volume Title
A1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä
This publication is imported from Aalto University research portal.
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
Other link related to publication (opens in new window)
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
Other link related to publication (opens in new window)
Date
2021-04-15
Major/Subject
Mcode
Degree programme
Language
en
Pages
15
61383-61397
61383-61397
Series
IEEE Access, Volume 9
Abstract
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.Description
Publisher Copyright: CCBY Copyright: Copyright 2021 Elsevier B.V., All rights reserved.
Keywords
Counterexample explanation, counterexample visualization, Delays, function block diagram, Input variables, Model checking, NuSMV, Power generation, Safety, Tools, user-friendly model checking, Visualization
Other note
Citation
Ovsiannikova, P, Buzhinsky, I, Pakonen, A & Vyatkin, V 2021, ' Oeritte : User-Friendly Counterexample Explanation for Model Checking ', IEEE Access, vol. 9, 9405616, pp. 61383-61397 . https://doi.org/10.1109/ACCESS.2021.3073459