Keywords

1 Introduction

Kind 2  [6] is an open-sourceFootnote 1 SMT-based model checker for safety properties of finite- and infinite-state synchronous reactive systems. It takes as input models written in an extension of the Lustre language [11]. The extension allows the specification of assume-guarantee-style contracts for the modeled system and its components which enables modular and compositional reasoning and considerably increases scalability. Kind 2 ’s contract language [5] is expressive enough to allow one to represent any (LTL) regular safety property by recasting it in terms of invariant properties. Kind 2 runs concurrently several model checking engines which cooperate to prove or disprove contracts and properties. In particular, it combines two induction-based model checking techniques, k-induction [16] and IC3 [4], with various auxiliary invariant generation methods.

One clear strength of model checkers is their ability to return precise error traces witnessing the violation of a given safety property. In addition to being invaluable to help identify and correct bugs, error traces also represent a checkable unsafety certificate. Similarly, some model checkers are able to return some form of corroborating evidence when they declare a safety property to be satisfied by a system under analysis. For instance, Kind 2 can produce an independently checkable proof certificate for the properties that it claims to have proven [14]. However, these certificates, in the form of a k-inductive invariant, give limited user-level insight on what elements of the system model contribute to the satisfaction of the properties.

Contributions. We describe two new diagnostic features of Kind 2 that provide more insights on verified properties: (1) the identification of minimal sets of model elements that are sufficient to prove a given set of safety properties, as well as the subset of design elements that are necessary to prove the given properties; (2) the computation of minimal sets of design constraints whose violation leads the system to falsify one of more of the given properties.

Although these two pieces of information are closely related, each of them can be naturally mapped to a typical use case in model-based software development: respectively, merit assignment and blame assignment. With the former the focus is on assessing the quality of a system specification, tracking the safety impact of model changes, and assisting in the synthesis of optimal implementations. With the latter, the goal is to determine the tolerance and resilience of a system against faults or cyber-attacks.

In general, proof-based traceability information can be used to perform a variety of engineering analyses, including vacuity detection [12]; coverage analysis [7, 9]; impact analysis [15], design optimization; and robustness analysis [17, 18]. Identifying which model elements are required for a proof, and assessing the relative importance of different model elements is critical to determine the quality of the overall model (including its assume-guarantee specification), determining when and where to implement changes, identifying components that need to be reverified, and measure the tolerance and resilience of the system against faults and attacks.

2 Running Example

We will use a simple model to illustrate the concepts and the functionality of Kind 2 introduced in this paper. Suppose we want to design a component for an airplane that controls the pitch motion of the aircraft, and suppose one of the system requirements is that the aircraft should not ascend beyond a certain altitude. The controller must read the current altitude of the aircraft from a sensor, and modify the next position of the aircraft’s nose accordingly. Moreover, we want the system to be fault-tolerant to sensor failures. One way to improve system fault-tolerance is to introduce some redundancy. In particular, we can equip the system with three different altimeters so the controller receives three independent altitude values. Then the controller, with the help of a dedicated component, a triplex voter, takes the average of the two altitude values that are closest to each other—as they are more likely to be close to the actual altitude. For simplicity, we will ignore other relevant signals that should be considered in a real setting to control the elevation of the aircraft.

Following a model-based design, we model an abstraction of the system’s environment to which the aircraft’s controller will react. We also model the fact that the system relies on possibly imperfect readings of the current altitude by the sensors to decide the next pitch value. Finally, we provide a specification for the controller’s behavior so that it satisfies the system requirement of interest.

Fig. 1.
figure 1

System model and subcomponents. Operators \({-}{>}\), abs and => are respectively the initialization operator, the absolute value function, and Boolean implication.

Full size image

Our model is described in Fig. 1 in Kind 2 ’s input language where system components are called nodes. The main component, SystemModel, is an observer node that represents the full system consisting in this case of just three subcomponents: one node modeling the controller, one modeling a triplex voter, and another one modeling the environment. The observer has three inputs: alt1, alt2, and alt3, representing the altitude values from each altimeter, and an output act_alt, representing the current altitude of the aircraft, which we are modeling as a product of the environment in response to the pitch value generated by the controller.

Kind 2 allows the user to specify contracts for individual nodes, either as special Lustre comments added directly inside the node declaration, or as the instantiation of an external stand-alone contract that can be imported in the body of other contracts. The contract of SystemModel, included directly in the node, specifies assumptions on the altitude values provided by the sensors and on a number of symbolic constants (TH, UB and ERR) which act in effect as model parameters. The contract assumes at line 4 that those constants are positive, or non-negative for ERR. The assumptions at lines 5–7 account for fact that, while the altitude value produced by each altimeter is not 100% accurate in actual settings, its error is bounded by a constant (ERR)Footnote 2. The contract includes a guarantee (line 8) that formalizes the requirement that aircraft maintain its altitude below a certain threshold TH at all times. The body of SystemModel is simply the parallel composition of a triplex voter, that takes the sensor values and computes an estimated altitude for the controller as explained above, the controller component, and the environment node.

Fig. 2.
figure 2

Low-level specification of the Triplex voter.

Full size image

A full specification for the TriplexVoter is given in Fig. 2. We do not specify the body of the Controller and the Environment nodes in our model because their details are not important for our purposes. Instead, we abstract their dynamics with an assume-guarantee contract that captures the relevant behavior. In the Controller’s case, we model the guarantee that the controller will produce a negative pitch value whenever the sensor altitude indicates that the aircraft is getting too close to the threshold value TH—with “too close” meaning that the difference between the current altitude and the threshold is smaller than UB + ERR where UB represents an upper bound on the change in altitude from one execution step to the next (see below).

Fig. 3.
figure 3

Contract specification for the Environment component of SystemModel.

Full size image

The declaration of the Environment component and its contract are shown separately in Fig. 3. With alt representing the actual altitude of the aircraft, the contract’s guarantees capture salient constraints on the physics of our model by specifying that a positive pitch value (which has the effect of raising the nose of the aircraft and lowering its tail) makes the aircraft ascend, a negative value makes it descend, and a zero value keeps it at the same altitude.Footnote 3 The contract also states that the actual altitude starts at zero, is alway non-negative, and does not change by more than a constant value (UB) in one sampling frame, where a sampling frame is identified with one execution step of the synchronous model (one global clock tick) for simplicity. The latter constraint on the altitude change rate captures physical limitations on the speed of the aircraft.

Kind 2 can easily prove that property (guarantee) R1 of SystemModel is invariant. However, a few interesting questions arise: (1) Is property R1 satisfied because of the conditions we imposed on the behavior of Controller, or does the property trivially hold due to the stated assumptions over the environment and the sensors? (2) Are all the assumptions over the environment and the sensors in fact necessary to prove the satisfaction of property R1? (3) How resilient is the system against the failure of one or more assumptions? We present in the following the new features of Kind 2 that help us answer these questions. A demo video associated to this paper can be found here [1].

3 The New Features

The first of the two new features offered by Kind 2 consists in identifying which parts of the input model were used to construct an inductive proof of invariance for R1. The new functionality relies on the concept of inductive validity core introduced by Ghassabani et al. [8]. Generally speaking, given a set of model elements M and an invariant property P, an inductive validity core (IVC) for P is a subset of M that is enough to prove P invariant. Kind 2 allows the user to choose among four sets of model elements: assumptions/guarantees, node calls, equations in node definitionsFootnote 4, and assertionsFootnote 5. In our running example, we consider \(P={\textsf {R1}}\) and \(M=S_1\cup C_2\cup E_3 \cup \{{\textsf {L1}}\}\) where \(S_1=\{{\textsf {S1}},{\textsf {S2}},{\textsf {S3}}\}\), \(C_2=\{{\textsf {C1}},{\textsf {C2}},{\textsf {C3}}\}\), and \(E_3=\{{\textsf {E1}},{\textsf {E2}},{\textsf {E3}},{\textsf {E4}},{\textsf {E5}},{\textsf {E6}},{\textsf {E7}}\}\). In particular, note that M is an IVC, although not a very interesting one. In practice, for complex enough models, smaller IVCs exist. In particular is often possible to compute efficiently a smaller IVC that contains few or no irrelevant elements. We can ensure that the elements of an IVC for a property P are necessary by requiring it to be minimal, that is, to have no proper subset that is also IVC for P. Kind 2 offers the option to compute a small but possibly non-minimal IVC, a minimal IVC (MIVC), or all minimal IVCs.

IVCs for Coverage and Change Impact Analysis. If a property P of a system S has multiple MIVCs, inspecting all of them provides insights on the different ways S satisfies P. Moreover, given all the MIVCs for P, it is possible to partition all the model elements into three sets [15]: a MUST set of elements which are required for proving P in every case, a MAY set of elements which are optional, and a set of elements that are irrelevant. This categorization provides complete traceability between specification and design elements, and can be used for coverage analysis [9] and tracking the safety impact of model changes. For instance, a change to one of the elements in the \( MAY \) set for P will not affect the satisfaction of P but will definitely impact some other property Q if it occurs in the \( MUST \) set for Q.

IVCs for Fault-Tolerance or Cyber-resiliency Analysis. Another use of IVCs, is in the analysis of a system’s tolerance to faults [18] or resiliency to cyber-attacks [17]. For instance, an empty MUST set for a system S and its invariant P indicates that the property is satisfied by S in various ways, making the system fault tolerant or resilient against cyber-attacks as far as property P is concerned. In contrast, a large MUST set suggest a more brittle system, with multiple points of failure or a big attack surface.

Quantifying a System’s Resilience. To help quantify the resilience of a system, Kind 2 also supports the computation of minimal cut sets (aka, minimal correction sets) for an invariance property. Given a set of model elements M and an invariant property P, a cut set C for P is a subset of M such that P is no longer invariant for \(M \setminus C\). A minimal cut set (MCS) for P is a cut set none of whose proper subsets is a cut set for P. A smallest cut set is an MCS of minimum cardinality. Kind 2 provides options to compute a (single) smallest cut set, all the MCSs, and all the MCSs up to a given cardinality bound. In the context of fault or security analyses, the cardinality of an MCS for a property P represents the number of design elements that must fail or be compromised for P to be violated. The smaller the MCS, or the higher the number of MCSs of small cardinality, the greater the probability that the property can be violated.

Running Example. If we ask Kind 2 to generate an IVC for the invariant R1 of the system presented in Sect. 2, Kind 2 generates a IVC with 9 elements: assumptions S1, S2, S3, and C1 from SystemModel’s contract, the (only) guarantee L1 in Controller’s contract, and all guarantees in the contract of Environment except for E2, E4, and E5. This tells us already that E2, E4, and E5 are not necessary to satisfy property R1 and is enough to answer the second of the questions listed at the end of Sect. 2. Moreover, since the guarantee L1 of Controller is part of the IVC, it is likely that the controller’s behavior is relevant for the satisfaction of R1. However, we can not be sure because the generated IVC is not necessarily minimal.

To confirm that L1 is indeed necessary we can ask Kind 2 to identify a true MIVC, a more expensive task computationally. When we do that, Kind 2 returns the same set. This confirms the necessity of the guarantee L1 but only for the specific proof of R1’s invariance found by Kind 2. It might still be the case that the guarantee is not required in general, that is, there may be other proofs that do not use L1, which would be confirmed by the discovery of a different MIVC that does not contain it. In other words, at this point we do not know whether L1 is a must element for R1. To determine that, we can ask Kind 2 to compute the MUST set for property R1 in addition to the MIVC. In that case, Kind 2 will return the same set as the MUST set, which confirms that all the included elements are required and the excluded ones are irrelevant.

Note that the last result also means that assumptions S1, S2, and S3 are always necessary, and thus, property R1 requires all three sensors to behave accordingly to their specification. Put differently, the analysis shows that the introduced redundancy mechanism does not actually make the system more fault tolerant. After reviewing the model, however, one can conclude that to benefit from the triplex voter we must decrease the safety limit value LIMIT in the controller’s contract. Specifically, it is enough to decrease it as follows, doubling the error bound value:

figure a

After this change, Kind 2 stops classifying assumptions S1, S2, and S3 as MUST elements. It computes a new MIVC of 8 elements which differs from the one computed for the previous version of the model for the absence of S3. To confirm that this MIVC is not the only solution, we can ask Kind 2 to compute all the MIVCs instead of a single one. This makes Kind 2 show two additional MIVCs that are symmetric to the computed MIVC: one set that contains S1 and S3 rather than S1 and S2, and another one that contains S2 and S3 instead S1 and S2. In alternative, we could ask Kind 2 to compute all the MCSs for the revised model. In that case, Kind 2 will find the following MCSs: \(\{{\textsf {E1}}\}\), \(\{{\textsf {E3}}\}\), \(\{{\textsf {E6}}\}\), \(\{{\textsf {E7}}\}\), \(\{{\textsf {C1}}\}\), \(\{{\textsf {L1}}\}\), \(\{{\textsf {S1}},{\textsf {S2}}\}\), \(\{{\textsf {S1}},{\textsf {S3}}\}\), \(\{{\textsf {S2}},{\textsf {S3}}\}\). This confirms that the system can now tolerate the failure of one of its three altimeters.

The exercise above illustrates how the new traceability feature in Kind 2 could be used to detect a subtle flaw in our enhanced model that prevented it from making the system fault-tolerant despite the triplication of the altitude sensors. We stress how a simple safety analysis, verifying the invariance of R1 would not help detect such flaw.

4 Implementation Details

Kind 2 is written in OCaml. All logical reasoning done by Kind 2 eventually reduces to queries to an external SMT solver. The implementation of the new features required around 2.8 KLOC. The computation of a small IVC for a property P is based on algorithm IVC_UC by Ghassabani et al. [8]. It consists of three main steps: (i) reducing the value of k for the k-inductive proof of property P (obtained by finding a k-inductive strengthening \(Q = Q_1 \wedge \cdots \wedge Q_n\) of P); (ii) reducing the number of conjuncts in invariant Q by removing those not needed in the proof; (iii) computing an UNSAT core over the model constraints in the same query to the backend SMT solver that checks that Q is a k-inductive strengthening of P. The computation of a single MIVC is based on algorithm IVC_UCBF, also by Ghassabani et al. [8]. The main idea is to generate a small IVC first, and then minimize it using a brute-force approach that removes one model element at a time and (model) checks that the property P still holds.

To compute all MIVCs we adapted algorithm UMIVC by Berryhill and Veneris [3] which in turn is a generalization of previous work [2, 10]. It basically explores in an efficient way the power set of model elements. The algorithm implemented in Kind 2 can be seen as an instantiation of UMIVC where all MCSs of cardinality 1 are precomputed. The major difference with UMIVC is that our algorithm is able to identify the MUST set from the generated set of MCSs, which can be use to check for early termination of the algorithm and to enhance the minimization of the intermediate IVCs generated during the process.

The problem of finding one cut set for a system S and a property P with at most k model elements is reduced to a model checking problem. Every violation of property P in this problem leads to a cut set. Kind 2 keeps solving this model checking problem using smaller and smaller bounds until there is no more violations. When that happens, it can extract a cut set of minimal cardinality. Kind 2 is also able to find all possible MCSs with cardinality smaller than a given bound by incrementally adding constraints that block the previous solutions. When there are no more minimal sets within the current cardinality bound, it increases that bound by one and repeats the process. It ends this process when the cardinality bound equals the number of model elements considered, having computed at that point all possible MCSs.

We refer the interested reader to a related technical report [13] for further implementation details and experimental results.