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
Change-based causes in counterexample explanationfor model checking
Computer Technologies Laboratory, ITMO University, Saint Petersburg, Russia; Department of Electrical Engineering and Automation, Aalto University, Espoo, Finland.
Department of Electrical Engineering and Automation, Aalto University, Espoo, Finland.
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Computer Science. Computer Technologies Laboratory, ITMO University, Saint Petersburg, Russia; Department of Electrical Engineering and Automation, Aalto University, Espoo, Finland.ORCID iD: 0000-0002-9315-9920
2021 (English)In: IECON 2021 – 47th Annual Conference of the IEEE Industrial Electronics Society, Institute of Electrical and Electronics Engineers (IEEE), 2021, p. 4804-4809Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2021. p. 4804-4809
Series
Annual Conference of Industrial Electronics Society, E-ISSN 2577-1647
National Category
Computer Systems Computer Sciences
Research subject
Dependable Communication and Computation Systems
Identifiers
URN: urn:nbn:se:ltu:diva-90106DOI: 10.1109/IECON48115.2021.9589122ISI: 000767230600075Scopus ID: 2-s2.0-85119488207OAI: oai:DiVA.org:ltu-90106DiVA, id: diva2:1650562
Conference
IECON 2021 - 47th Annual Conference of the IEEE Industrial Electronics Society, Toronto, Canada, October13-16, 2021
Note

ISBN för värdpublikation: 978-1-6654-3554-3

Available from: 2022-04-07 Created: 2022-04-07 Last updated: 2022-04-28Bibliographically 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
Computer SystemsComputer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 54 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