Sökning: id:"swepub:oai:DiVA.org:ltu-72060" >
Counterexample visu...
Counterexample visualization and explanation for function block diagrams
-
- Pakonen, Antti (författare)
- VTT Technical Research Centre of Finland Ltd., Espoo, Finland
-
- Buzhinsky, Igor (författare)
- Department of Electrical Engineering and Automation, Aalto University, Espoo, Finland
-
- Vyatkin, Valeriy (författare)
- Luleå tekniska universitet,Datavetenskap
-
VTT Technical Research Centre of Finland Ltd, Espoo, Finland Department of Electrical Engineering and Automation, Aalto University, Espoo, Finland (creator_code:org_t)
- Piscataway, NJ : IEEE, 2018
- 2018
- Engelska.
-
Ingår i: 2018 IEEE 16th International Conference on Industrial Informatics (INDIN). - Piscataway, NJ : IEEE. - 9781538648292 ; , s. 747-753
- Relaterad länk:
-
https://urn.kb.se/re...
-
visa fler...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- formal verification
- model checking
- visualization of counterexamples
- explanation of counterexamples
- Dependable Communication and Computation Systems
- Kommunikations- och beräkningssystem
Publikations- och innehållstyp
- ref (ämneskategori)
- kon (ämneskategori)
Hitta via bibliotek
Till lärosätets databas