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
Visual counterexample explanation for model checking with OERITTE
Computer Technologies Laboratory, ITMO University, Saint Petersburg, Russia; Department of Electrical Engineering and Automation, Aalto University, Espoo, Finland.
Computer Technologies Laboratory, ITMO University, Saint Petersburg, Russia; Department of Electrical Engineering and Automation, Aalto University, Espoo, Finland.
VTT Technical Research Centre of Finland Ltd., 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: Proceedings: 2020 25th International Conference onEngineering of Complex ComputerSystems ICECCS 2020 / [ed] Yi Li; Alan Liew, IEEE, 2021, p. 1-10Conference paper, Published paper (Refereed)
Abstract [en]

Despite being one of the most reliable approaches for ensuring system correctness, model checking requires auxiliary tools to fully avail. In this work, we tackle the issue of its results being hard to interpret and present OERITTE, a tool for automatic visual counterexample explanation for function block diagrams. To learn what went wrong, the user can inspect a parse tree of the violated LTL formula and a table view of a counterexample, where important variables are highlighted. Then, on the function block diagram of the system under verification, they can receive a visualization of causality relationships between the calculated values of interest and intermediate results or inputs of the function block diagram. Thus, OERITTE serves to decrease formal model and specification debugging efforts along with making model checking more utilizable for complex industrial systems.

Place, publisher, year, edition, pages
IEEE, 2021. p. 1-10
Keywords [en]
user-friendly model checking, counterexample explanation, counterexample visualization
National Category
Computer Sciences
Research subject
Dependable Communication and Computation Systems
Identifiers
URN: urn:nbn:se:ltu:diva-83408DOI: 10.1109/ICECCS51672.2020.00008ISI: 000943471500001Scopus ID: 2-s2.0-85103483792OAI: oai:DiVA.org:ltu-83408DiVA, id: diva2:1539990
Conference
25th International Conference on Engineering of Complex Computer Systems (ICECCS 2020), Singapore (Hybrid Physical/Virtual), March 4-6, 2021
Note

ISBN för värdpublikation: 978-1-7281-8558-3;

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

Available from: 2021-03-26 Created: 2021-03-26 Last updated: 2025-04-25Bibliographically 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 Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

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