Merit and Blame Assignment with Kind 2

TL;DR

This paper presents new features in the Kind 2 model checker that enhance traceability, identify minimal core elements for safety proofs, and analyze system resilience, aiding in safety assessment and fault analysis.

Contribution

Introduction of traceability features, minimal inductive validity cores, and minimal cut sets in Kind 2 for improved safety and fault analysis of reactive systems.

Findings

Successfully identified minimal sets of design elements for safety properties

Determined necessary design elements for safety proofs

Evaluated the effectiveness of new features in initial experiments

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. The computed information can be used for several purposes, including assessing the quality of a system specification, tracking the safety impact of model changes, and analyzing the tolerance and resilience of a system against faults or cyber-attacks. We describe these new capabilities in some detail and report on an initial experimental evaluation of some of them.