Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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
Counterexample visualization and explanation for function block diagrams
VTT Technical Research Centre of Finland Ltd., 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.ORCID iD: 0000-0002-9315-9920
2018 (English)In: 2018 IEEE 16th International Conference on Industrial Informatics (INDIN), Piscataway, NJ: IEEE, 2018, p. 747-753, article id 8472025Conference paper, Published paper (Refereed)
Abstract [en]

Model checking is a proven, effective method for verifying instrumentation and control system application logics. If a model of the system being verified does not satisfy a specification, the failure scenario is presented to the user as a counterexample trace. Analysis of the counterexample can be time-consuming if the trace is long, the model is large, or the specification is complex. Spurious counterexamples (“false negatives”) often exacerbate the problem. In this paper, we present a method that assists in identifying the root of the failure in both the model and the specification, by animating the model of the function block diagram as well as the LTL property. We also introduce a practical tool for visualizing LTL properties by animation and highlighting of important values based on causality. Using 43 actual design issues identified in practical nuclear industry projects, we then evaluate usefulness of the property visualization and explanation features.

Place, publisher, year, edition, pages
Piscataway, NJ: IEEE, 2018. p. 747-753, article id 8472025
Series
IEEE International Conference on Industrial Informatics INDIN, ISSN 1935-4576
Keywords [en]
formal verification, model checking, visualization of counterexamples, explanation of counterexamples
National Category
Computer Sciences
Research subject
Dependable Communication and Computation Systems
Identifiers
URN: urn:nbn:se:ltu:diva-72060DOI: 10.1109/INDIN.2018.8472025ISI: 000450180200109Scopus ID: 2-s2.0-85055594626ISBN: 978-1-5386-4829-2 (electronic)OAI: oai:DiVA.org:ltu-72060DiVA, id: diva2:1271267
Conference
16th IEEE International Conference on Industrial Informatics, INDIN 2018, Porto, Portugal, 18-20 July 2018
Available from: 2018-12-17 Created: 2018-12-17 Last updated: 2019-01-14Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records BETA

Vyatkin, Valeriy

Search in DiVA

By author/editor
Vyatkin, Valeriy
By organisation
Computer Science
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 2 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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