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

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussa › Conference article in proceedings › Scientific › vertaisarvioitu

1 Sitaatiot (Scopus)

Abstrakti

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.

Alkuperäiskieli	Englanti
Otsikko	IECON 2021 – 47th Annual Conference of the IEEE Industrial Electronics Society
Kustantaja	IEEE
Sivumäärä	6
ISBN (elektroninen)	978-1-6654-3554-3
ISBN (painettu)	978-1-6654-0256-9
DOI - pysyväislinkit	https://doi.org/10.1109/IECON48115.2021.9589122
Tila	Julkaistu - 13 marrask. 2021
OKM-julkaisutyyppi	A4 Artikkeli konferenssijulkaisussa
Tapahtuma	Annual Conference of the IEEE Industrial Electronics Society - Virtual, online, Toronto, Kanada Kesto: 13 lokak. 2021 → 16 lokak. 2021 Konferenssinumero: 47 https://ieeeiecon.org/

Julkaisusarja

Nimi	Proceedings of the Annual Conference of the IEEE Industrial Electronics Society
ISSN (elektroninen)	2577-1647

Conference

Conference	Annual Conference of the IEEE Industrial Electronics Society
Lyhennettä	IECON
Maa/Alue	Kanada
Kaupunki	Toronto
Ajanjakso	13/10/2021 → 16/10/2021
www-osoite	https://ieeeiecon.org/

Pääsy asiakirjaan

10.1109/IECON48115.2021.9589122

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

Muut tiedostot ja linkit

Linkki julkaisuun Scopuksessa

Siteeraa tätä

@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. julkaisussa 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, Kanada, 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).

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussa › Conference article in proceedings › Scientific › vertaisarvioitu

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

Abstrakti

Julkaisusarja

Conference

Pääsy asiakirjaan

Muut tiedostot ja linkit

Sormenjälki

Siteeraa tätä