Book chapter
Merit and Blame Assignment with Kind 2
Formal Methods for Industrial Critical Systems, pp.212-220
Lecture Notes in Computer Science, Springer International Publishing
08/19/2021
DOI: 10.1007/978-3-030-85248-1_14
Abstract
We introduce two new major features of the open-source model checker Kind 2 which provide traceability information between specification and design elements such as assumptions, guarantees, or other behavioral constraints in synchronous reactive system models. This new version of Kind 2 can identify minimal sets of design elements, known as Minimal Inductive Validity Cores, which are sufficient to prove a given set of safety properties, and also determine the set of MUST elements, design elements that are necessary to prove the given properties. In addition, Kind 2 is able to find minimal sets of design constraints, known as Minimal Cut Sets, whose violation leads the system to an unsafe state. We illustrate with an example how to use the computed information for tracking the safety impact of model changes, and for analyzing the tolerance and resilience of a system against faults.
Details
- Title: Subtitle
- Merit and Blame Assignment with Kind 2
- Creators
- Daniel Larraz - University of IowaMickaël Laurent - University of IowaCesare Tinelli - University of Iowa
- Resource Type
- Book chapter
- Publication Details
- Formal Methods for Industrial Critical Systems, pp.212-220
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-030-85248-1_14
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Publisher
- Springer International Publishing; Cham
- Language
- English
- Date published
- 08/19/2021
- Academic Unit
- Computer Science
- Record Identifier
- 9984259492302771
Metrics
80 Record Views