Counterexample visualization and explanation for function block diagrams

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


Research units

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


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.


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

Publication series

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


ConferenceIEEE International Conference on Industrial Informatics
Abbreviated titleINDIN
Internet address

    Research areas

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

ID: 29462298