Change-based causes in counterexample explanation for model checking

Polina Ovsiannikova; Antti Pakonen; Valeriy Vyatkin

doi:10.1109/IECON48115.2021.9589122

Change-based causes in counterexample explanation for model checking

Polina Ovsiannikova, Antti Pakonen, Valeriy Vyatkin

Research output: Chapter in Book/Report/Conference proceeding › Conference article in proceedings › Scientific › peer-review

1 Citation (Scopus)

Abstract

Formal verification by means of model checking avails in discovering design issues of safety systems at the early stages. However, a significant amount of time and effort is required to decipher its results and localize the failure, especially in complex logic. This work continues our previous study on the visual explanation of failure traces and introduces change-based causes. Additionally, inspired by the types of properties that revealed model failures in projects of VTT in the Finnish nuclear industry, we define a new form of explanation – a hybrid influence graph. The new approach was implemented in a tool called Oeritte and evaluated using two practical examples of failures in nuclear instrumentation and control systems.

Original language	English
Title of host publication	IECON 2021 – 47th Annual Conference of the IEEE Industrial Electronics Society
Publisher	IEEE
Number of pages	6
ISBN (Electronic)	978-1-6654-3554-3
ISBN (Print)	978-1-6654-0256-9
DOIs	https://doi.org/10.1109/IECON48115.2021.9589122
Publication status	Published - 13 Nov 2021
MoE publication type	A4 Conference publication
Event	Annual Conference of the IEEE Industrial Electronics Society - Virtual, online, Toronto, Canada Duration: 13 Oct 2021 → 16 Oct 2021 Conference number: 47 https://ieeeiecon.org/

Publication series

Name	Proceedings of the Annual Conference of the IEEE Industrial Electronics Society
ISSN (Electronic)	2577-1647

Conference

Conference	Annual Conference of the IEEE Industrial Electronics Society
Abbreviated title	IECON
Country/Territory	Canada
City	Toronto
Period	13/10/2021 → 16/10/2021
Internet address	https://ieeeiecon.org/

Keywords

counterexample explanation
user-friendly model checking
causality
function block diagrams

Access to Document

10.1109/IECON48115.2021.9589122

https://cris.vtt.fi/en/publications/change-based-causes-in-counterexample-explanation-for-model-check

Cite this

@inproceedings{b5507b85d182491dafa2dfbef6f200ff,

title = "Change-based causes in counterexample explanation for model checking",

abstract = "Formal verification by means of model checking avails in discovering design issues of safety systems at the early stages. However, a significant amount of time and effort is required to decipher its results and localize the failure, especially in complex logic. This work continues our previous study on the visual explanation of failure traces and introduces change-based causes. Additionally, inspired by the types of properties that revealed model failures in projects of VTT in the Finnish nuclear industry, we define a new form of explanation – a hybrid influence graph. The new approach was implemented in a tool called Oeritte and evaluated using two practical examples of failures in nuclear instrumentation and control systems.",

keywords = "counterexample explanation, user-friendly model checking, causality, function block diagrams",

author = "Polina Ovsiannikova and Antti Pakonen and Valeriy Vyatkin",

note = "Funding Information: This work was supported, in part, by the Finnish Research Programme on Nuclear Power Plant Safety 2018-2022 (SAFIR 2022) and by the Government of the Russian Federation under Grant 08-08. Publisher Copyright: {\textcopyright} 2021 IEEE.; 47th Annual Conference of the IEEE Industrial Electronics Society, IECON 2021 ; Conference date: 13-10-2021 Through 16-10-2021; Annual Conference of the IEEE Industrial Electronics Society, IECON ; Conference date: 13-10-2021 Through 16-10-2021",

year = "2021",

month = nov,

day = "13",

doi = "10.1109/IECON48115.2021.9589122",

language = "English",

isbn = "978-1-6654-0256-9",

series = "Proceedings of the Annual Conference of the IEEE Industrial Electronics Society",

publisher = "IEEE",

booktitle = "IECON 2021 – 47th Annual Conference of the IEEE Industrial Electronics Society",

address = "United States",

url = "https://ieeeiecon.org/",

}

Ovsiannikova, P, Pakonen, A & Vyatkin, V 2021, Change-based causes in counterexample explanation for model checking. in IECON 2021 – 47th Annual Conference of the IEEE Industrial Electronics Society. Proceedings of the Annual Conference of the IEEE Industrial Electronics Society, IEEE, Annual Conference of the IEEE Industrial Electronics Society, Toronto, Ontario, Canada, 13/10/2021. https://doi.org/10.1109/IECON48115.2021.9589122

Change-based causes in counterexample explanation for model checking. / Ovsiannikova, Polina; Pakonen, Antti; Vyatkin, Valeriy.
IECON 2021 – 47th Annual Conference of the IEEE Industrial Electronics Society. IEEE, 2021. (Proceedings of the Annual Conference of the IEEE Industrial Electronics Society).

Research output: Chapter in Book/Report/Conference proceeding › Conference article in proceedings › Scientific › peer-review

TY - GEN

T1 - Change-based causes in counterexample explanation for model checking

AU - Ovsiannikova, Polina

AU - Pakonen, Antti

AU - Vyatkin, Valeriy

N1 - Conference code: 47

PY - 2021/11/13

Y1 - 2021/11/13

N2 - Formal verification by means of model checking avails in discovering design issues of safety systems at the early stages. However, a significant amount of time and effort is required to decipher its results and localize the failure, especially in complex logic. This work continues our previous study on the visual explanation of failure traces and introduces change-based causes. Additionally, inspired by the types of properties that revealed model failures in projects of VTT in the Finnish nuclear industry, we define a new form of explanation – a hybrid influence graph. The new approach was implemented in a tool called Oeritte and evaluated using two practical examples of failures in nuclear instrumentation and control systems.

AB - Formal verification by means of model checking avails in discovering design issues of safety systems at the early stages. However, a significant amount of time and effort is required to decipher its results and localize the failure, especially in complex logic. This work continues our previous study on the visual explanation of failure traces and introduces change-based causes. Additionally, inspired by the types of properties that revealed model failures in projects of VTT in the Finnish nuclear industry, we define a new form of explanation – a hybrid influence graph. The new approach was implemented in a tool called Oeritte and evaluated using two practical examples of failures in nuclear instrumentation and control systems.

KW - counterexample explanation

KW - user-friendly model checking

KW - causality

KW - function block diagrams

UR - http://www.scopus.com/inward/record.url?scp=85119488207&partnerID=8YFLogxK

U2 - 10.1109/IECON48115.2021.9589122

DO - 10.1109/IECON48115.2021.9589122

M3 - Conference article in proceedings

SN - 978-1-6654-0256-9

T3 - Proceedings of the Annual Conference of the IEEE Industrial Electronics Society

BT - IECON 2021 – 47th Annual Conference of the IEEE Industrial Electronics Society

PB - IEEE

T2 - Annual Conference of the IEEE Industrial Electronics Society

Y2 - 13 October 2021 through 16 October 2021

ER -

Change-based causes in counterexample explanation for model checking

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this