Counterexample visualization and explanation for function block diagrams

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

Researchers

Research units

  • VTT Technical Research Centre of Finland
  • Luleå University of Technology
  • St. Petersburg National Research University of Information Technologies, Mechanics and Optics (ITMO)

Abstract

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.

Details

Original languageEnglish
Title of host publicationProceedings of the IEEE 16th International Conference on Industrial Informatics, INDIN 2018
Publication statusPublished - 24 Sep 2018
MoE publication typeA4 Article in a conference publication
EventIEEE International Conference on Industrial Informatics - University of Porto's Engineering Faculty (FEUP), Porto, Portugal
Duration: 18 Jul 201820 Jul 2018
Conference number: 16
https://web.fe.up.pt/~indin2018/
https://web.fe.up.pt/~indin2018/

Publication series

NameIEEE International Conference on Industrial Informatics
PublisherIEEE
ISSN (Print)1935-4576
ISSN (Electronic)2378-363X

Conference

ConferenceIEEE International Conference on Industrial Informatics
Abbreviated titleINDIN
CountryPortugal
CityPorto
Period18/07/201820/07/2018
Internet address

    Research areas

  • Explanation of counterexamples, Formal verification, Model checking, Visualization of counterexamples

ID: 29462298