key: cord-0048660-cqylfzlk
authors: Menghi, Claudio; Rizzi, Alessandro Maria; Bernasconi, Anna
title: Integrating Topological Proofs with Model Checking to Instrument Iterative Design
date: 2020-03-13
journal: Fundamental Approaches to Software Engineering
DOI: 10.1007/978-3-030-45234-6_3
sha: 47d1e29cd02a953100597d733adb723b55d847ba
doc_id: 48660
cord_uid: cqylfzlk

System development is not a linear, one-shot process. It proceeds through refinements and revisions. To support assurance that the system satisfies its requirements, it is desirable that continuous verification can be performed after each refinement or revision step. To achieve practical adoption, formal verification must accommodate continuous verification efficiently and effectively. Model checking provides developers with information useful to improve their models only when a property is not satisfied, i.e., when a counterexample is returned. However, it is desirable to have some useful information also when a property is instead satisfied. To address this problem we propose TOrPEDO, an approach that supports verification in two complementary forms: model checking and proofs. While model checking is typically used to pinpoint model behaviors that violate requirements, proofs can instead explain why requirements are satisfied. In our work, we introduce a specific notion of proof, called Topological Proof. A topological proof produces a slice of the original model that justifies the property satisfaction. Because models can be incomplete, TOrPEDO supports reasoning on requirements satisfaction, violation, and possible satisfaction (in the case where satisfaction depends on unknown parts of the model). Evaluation is performed by checking how topological proofs support software development on 12 modeling scenarios and 15 different properties obtained from 3 examples from literature. Results show that: (i) topological proofs are [Formula: see text]60% smaller than the original models; (ii) after a revision, in [Formula: see text]78% of cases, the property can be re-verified by relying on a simple syntactic check.

One of the goals of software engineering and formal methods is to provide automated verification tools that support designers in producing models of an envisioned system which follows a set of properties of interest. Designers benefit from automated support to understand why their system does not behave as expected (e.g., counterexamples), but they might find it also useful to retrieve information when the system already follows the specified requirements. While model checkers provide the former, theorem provers sustain the latter. Theorem provers usually rely on some form of deductive mechanism that, given a set of axioms, iteratively applies a set of rules until a theorem is proved. The proof consists of the specific sequence of deductive rules applied to prove the theorem. In the literature, many approaches have dealt with an integration of model checking and theorem proving at various levels (e.g., [48, 60, 53, 36] ). These approaches are oriented to produce certified model checking procedures rather than tools that actually help the design process. Even when the idea is to provide a practically useful framework [49, 50] , the output consists of deductive proofs that are usually difficult to understand and hardly connectable with the designer's modeling choices. Moreover, verification techniques only take into account completely specified designs. This is a remarkable limitation in practical contexts, where the designer may start by providing an initial, high-level version of the model, which is iteratively narrowed down as design progresses and uncertainties are removed [13, 42, 8, 19, 65, 43] . A recent work [4, 5] considered cases in which a partial knowledge of the system model is available. However, the presented approach was mainly theoretical and lacked a practical implementation.

We formulate our problem on models that contain uncertain parts. We choose Partial Kripke Structures (PKSs) as a formalism to represent general models for the following reasons: (i) PKSs have been used in requirement elicitation to reason about system behavior from different points of view [19, 8] , and are a common theoretical reference language used in the formal method community for the specification of uncertain models (e.g, [26, 9, 27, 10] ); (ii) other modeling formalisms commonly used in software development [23, 64] , such as Modal Transition Systems [37] (MTSs), can be converted into PKSs through a simple transformation [26] making our solution easily applicable to those models.

Kripke Structures (KSs) are particular instances of PKSs that represent complete models. Requirements on the model are expressed in Linear-time Temporal Logic (LTL). As such, the approach presented in the following is generic: it can be applied on models that contain uncertain parts (PKSs) or not (KSs), and can be easily adapted to support MTSs.

Verification techniques that consider PKSs return three alternative values: true if the property holds in the partial model, false if it does not hold, and maybe if the property possibly holds, i.e., its satisfaction depends on the parts of the model that still need to be refined. As models are revised, i.e., they are modified during design iterations, designers need support to understand why properties are satisfied, or possibly satisfied.

A comprehensive and integrated design framework able to support software designers in understanding such motivation is still missing. We tackle this problem by presenting TOrPEDO (TOpological Proof drivEn Development frame-wOrk), a novel automated verification framework, that:

(i) supports a modeling formalism which allows a partial specification of the system design;

(ii) allows performing analysis and verification in the context of systems in which "incompleteness" represents a conceptual uncertainty; (iii) provides guidance in producing model revisions through complementary outputs: counterexamples and proofs; (iv) when the system is completely specified, allows understanding which changes impact or not the satisfaction of certain properties.

TOrPEDO is based on the novel notion of topological proof (TP), which tries to overcome the complexity of deductive proofs and is designed to make proofs understandable on the original system design. A TP is a slice of the original model that specifies which part of it impacts the property satisfaction. If the slice defined by the TP is not preserved during a revision, there is no assurance that the property holds (possibly holds) in the revised model. This paper proposes an algorithm to compute topological proofs-which relies on the notion of unsatisfiable cores (UCs) [56] -and proves its correctness on PKSs. It also proposes an algorithm that checks whether a TP is preserved in a model revision. This simple syntactic check avoids (in many cases) the execution of the model checking procedure. While architectural decomposition and composition of components can be considered during the system development [42] , in this work we present our solution by assuming that the system is modeled as a single PKS. However, our framework can be extended to consider the composition of components, such as the parallel composition of PKSs or MTSs. This can be done by extracting the portions of the TP that refer to the different components.

TOrPEDO has been implemented on top of NuSMV [14] and PLTL-MUP [58] . The implementation has been exploited to evaluate TOrPEDO by considering a set of examples coming from literature including both completely specified and partially specified models. We considered 3 different example models and 4 variations for each model that was presented in the literature [12, 20] . We considered 15 properties, i.e., 5 for each example, leading to a total of 60 (3×4×5) scenarios that require the evaluation of a property on a model. We evaluated how our framework supports model design by comparing the size of the generated topological proofs against the size of the original models. Results show that topological proofs are ≈60% smaller than the original models. Moreover, after a revision, in ≈78% of cases, our syntactic check avoids the re-execution of the model checker.

Organization. Section 2 describes TOrPEDO. Section 3 discusses the background. Sections 4 and 5 present the theoretical results and the algorithms that support TOrPEDO. Section 6 evaluates the achieved results. Section 7 discusses related work. Section 8 concludes.

TOrPEDO is a proof based development framework which allows verifying PKSs and evaluating their revisions. To illustrate TOrPEDO, we use a simple model describing the states of a vacuum-cleaner robot that has to satisfy the requirements in Fig. 2 , specified through LTL formulae and English natural language.

Textual requirements φ1: the robot is drawing dust (suck ) only if it has reached the cleaning site. φ2: the robot must be turned on before it can move. φ3: if the robot is on and stationary (¬move), it must be drawing dust (suck ). φ4: the robot must move before it is allowed to draw dust (suck ). Fig. 2 : Natural language and LTL formulation of the requirements of the vacuum-cleaner robot. G and W are the "globally" and "weak until" LTL operators.

The TOrPEDO framework is illustrated in Fig. 3 and carries out verification in four phases: initial design, analysis, revision, and re-check.

The model of the system is expressed using a PKS M ( 1 ), which can be generated from other languages, along with the property of interest φ, in LTL ( 2 ).

Running example. The PKS presented in Fig. 1 is defined over two atomic propositions representing actions that a robot can perform: move, i.e., the agent travels to the cleaning site; suck , i.e., the agent is drawing the dust, and two atomic propositions representing conditions that can trigger actions: on, true when the robot is turned on; reached , true when the robot has reached the cleaning site. The state OFF represents the robot being shut down, IDLE the robot being tuned on w.r.t. a cleaning call, MOVING the robot reaching the cleaning site, and CLEANING the robot performing its duty. Each state is labeled with the actions move and suck and the conditions on and reached . Given an action or condition α and a state s, we use the notation: α = to indicate that α occurs when the robot is in state s; α = ⊥ to indicate that α does not occur when the robot is in state s; α =? to indicate that there is uncertainty on whether α occurs when the robot is in state s.

TOrPEDO provides automated analysis support, which includes the following elements:

(i) Information about what is wrong in the current design. This information includes a definitive-counterexample, which indicates a behavior that depends on already performed design choices and violates the properties of interest. The definitive-counterexample ( 3 ⊥-CE) can be used to produce a revised version M of M that satisfies or possibly satisfies the property of interest.

The image part with relationship ID rId3 was not found in the file. In the following we will use the notation x-topological proofs or x-TP to indicate arbitrarily definitive-topological or possible-topological proofs. The results returned by TORPEDO for the different properties in our motivating example are presented in Table 1 . Property φ 2 is satisfied, φ 3 is not. In those cases TOR-PEDO returns respectively a definitive-proof and a definitive-counterexample. Since φ 1 and φ 4 are possibly satisfied, in both cases a possible-counterexample and a possible-topological proof are returned.

Running example. For φ 1 the possible-counterexample shows a run that may violate the property of interest. The possible-topological proof in Table 1 shows that if OFF remains the only initial state (TPI), reached still holds in CLEANING, and suck does not hold in OFF and IDLE , while unknown in MOVING (TPP), property φ 1 remains possibly satisfied. In addition, all transitions must be preserved (TPT). 3 Note that the proof highlights portions of the model that influence the property satisfaction. For example, by inspecting the proof, the designer understands that she can change the value of the proposition reached in all the states of the PKS, with the exception of the state CLEANING, without making the property violated. Table 1 : Results provided by TOrPEDO for properties φ 1 , φ 2 , φ 3 and φ 4 . , ⊥ and ? indicate that the property is satisfied, violated and possibly satisfied. Running example. The designer may want to propose a revision that still does not violate properties φ 1 , φ 2 , and φ 4 . Thus, she changes the values of some atomic propositions: move becomes in state CLEANING and reached becomes ⊥ in state IDLE . Since φ 1 , φ 2 , and φ 4 were previously not violated, TOrPEDO performs the re-check phase for each property.

The automated verification tool provided by TOrPEDO checks whether all the changes in the current model revision are compliant with the x-TPs ( 10 ), i.e., changes applied to the revised model do not include parts that had to be preserved according to the x-topological proof. If a property of interest is (possibly) satisfied in a previous model, and the revision of the model is compliant with the property x-TP, the designer has the guarantee that the property is (possibly) satisfied in the revision. Thus, she can perform another model revision round ( 7 ) or approve the current design ( 11 ) . Otherwise, TOrPEDO re-executes the analysis ( 12 ).

Running example. In the vacuum-cleaner case, the revision passes the recheck and the designer proceeds to a new revision phase.

We present background notions by relying on standard notations for the selected formalisms (see for example [26, 9, 10, 30] ).

Partial Kripke Structures ( 1 ) are state machines that can be adopted when the value of some propositions is uncertain on selected states. A PKS represents a system as a set of states and transitions between these states. Uncertainty on the AP is represented through the value ?. The model in Fig. 1 is a PKS where propositions in AP are used to model actions and conditions. LTL properties ( 2 ) . For KSs we consider the classical LTL semantics [M |= φ] over infinite words that associates to a model M and a formula φ a truth value in the set {⊥, }. The interested reader may refer, for example, to [3] . Let M be a KS and φ be an LTL property. We assume that the function Check, such that res, c = Check(M , φ), returns a tuple res, c , where res is the model checking result in { , ⊥} and c is the counterexample if res = ⊥, else an empty set.

The three-valued LTL semantics [9] [M |= φ] associates to a model M and a formula φ a truth value in the set {⊥, ?, } and is defined based on the information ordering > ? > ⊥. The three-valued LTL semantics is defined by considering paths of the model M . A path π is an infinite sequence of states s 0 , s 1 , . . . such that, for all i ≥ 0, (s i , s i+1 ) ∈ R. We use the symbol π i to indicate the infinite sub-sequence of π that starts at position i, and P ath(s) to indicate all the paths that start in the state s.

). Let M = S, R, S 0 , AP, L be a PKS, π = s 0 , s 1 , . . . be a path, and φ be an LTL formula. Then, the three-valued semantics [(M, π) |= φ] is defined inductively as follows:

Let M = S, R, S 0 , AP, L be a PKS, and φ be an LTL formula.

The conjunction (resp. disjunction) is defined as the minimum (resp. maximum) of its arguments, following the order ⊥ < ? < . These functions are extended to sets with min(∅)= and max(∅)=⊥. The comp operator maps to ⊥, ⊥ to , and ? to ?. The semantics of the G ("globally") and W ("weak until") operators is defined as usual [28] .

Model Checking. Checking KSs with respect to LTL properties can be done by using classical model checking procedures. For example, the model checking problem of property φ on a KS M can be reduced to the satisfiability problem of the LTL formula Φ M ∧ ¬φ, where Φ M represents the behaviors of model M .

Checking a PKS M with respect to an LTL property φ considering the threevalued semantics is done by performing twice the classical model checking procedure for KSs [10] , one considering an optimistic approximation M opt and one considering a pessimistic approximation M pes . These two procedures consider the LTL formula φ = F(φ), where F transforms φ with the following steps: (i) negate φ; (ii) convert ¬φ in negation normal form; (iii) replace every subformula ¬α, where α is an atomic proposition, with a new proposition α.

To create the optimistic and pessimistic approximations M opt and M pes , the PKS M = S, R, S 0 , AP, L is first converted into its complement-closed version M c = S, R, S 0 , AP c , L c where the set of atomic propositions AP c = AP ∪AP is such that AP = {α | α ∈ AP }. Atomic propositions in AP are called complement-closed propositions. Function L c is such that, for all s ∈ S and α ∈ AP , L c (s, α) = L(s, α) and, for all s ∈ S and α ∈ AP , L c (s, p) = comp(L(s, p)). 

, and, for all s ∈ S, α ∈ AP c , and L c (s, α) =?, then L pes (s, α) = ⊥ (resp. L opt (s, α) = ).

Let A be a KS and φ be an LTL formula, A |= * φ is true if no path that satisfies the formula F(φ) is present in A. 

We call Check * the function that computes the result of operator |= * . It takes as input either M pes or M opt and the property F(φ), and returns a tuple res, c , where res is the model checking result in { , ⊥}, and c can be an empty set (when M satisfies φ), a definitive-counterexample ( 3 , when M violates φ), or a possible-counterexample ( 5 , when M possibly-satisfies φ).

We define how models can be revised and the notion of topological proof, that is used to describe why a property φ is (possibly) satisfied in a PKS M .

Initial design and revisions ( 1 , 3 ) . In the initial design a preliminary PKS is manually defined or automatically obtained from other modeling formalisms.

During a revision, a designer can add and remove states and transitions and/or change the labeling of the atomic propositions in the states of the PKS. Let M = S, R, S 0 , AP, L and M = S , R , S 0 , AP , L be two PKSs. Then M is a revision of M if and only if AP ⊆ AP . Informally, the only constraint the designer has to respect during a revision is not to remove propositions from the set of atomic propositions. This condition is necessary to ensure that any property that can be evaluated on M can also be evaluated on M , i.e., every atomic proposition has a value in each of the states of the automaton. The deactivation of a proposition can instead be simulated by associating its value to ⊥ in all the states of M .

Topological proofs ( 4 , 6 ) . The pursued proof is made of a set of clauses specifying certain topological properties of M , which ensure that the property is (possibly) satisfied. Table 1 , for property φ 1 , CLEANING, reached , is a TPP-clause that constrains the atomic proposition reached to be labeled as true ( ) in the state CLEANING; OFF , {OFF , IDLE } is a TPT-clause that constrains the transition from OFF to OFF and from OFF to IDLE to not be removed; and {OFF } is a TPI-clause that constrains the state OFF to remain the initial state of the system.

A state s is constrained: by a TPP-clause s, α, v if s = s , by a TPT-clause s, T if s = s or s ∈ T , and by a TPI-clause S 0 if s ∈ S 0 . Intuitively, a PKS Ω-related to M is a PKS obtained from M by changing any topological aspect that does not impact on the set of TP-clauses Ω. Any transition whose source state is not the source state of a transition included in the TPT-clauses can be added or removed from the PKS and any value of a proposition that is not constrained by a TPP-clause can be changed. States can be always added and they can be removed if they are not constrained by any TPT-, TPP-, or TPI-clause. Initial states cannot be changed if Ω contains a TPI-clause. Intuitively, an x-topological proof is a set of TP-clauses Ω such that every PKS M that satisfies the conditions specified in Definition 4 is such that [M |= φ] ≥ x. We call -TP a definitive-topological proof and ?-TP a possibletopological proof. In Definition 5, the operator ≥ assumes that values , ?, ⊥ are ordered considering the classical information ordering > ? > ⊥ among the truth values [9] .

Regarding the PKS in Fig. 1 , Table 1 shows two ?-TPs for properties φ 1 and φ 4 , and one -TP for property φ 2 . Proof Sketch. We prove the first statement of the Theorem; the proof of the second statement is obtained by following the same steps.

If Ω is a -TP, it is a -TP for φ in M , since M is an Ω -revision of M (by Definition 6). Furthermore, since Ω is a -TP for φ in M , then [M |= φ] ≥ (by Definition 5).

This section describes the algorithms that support the analysis and re-check phases of TOrPEDO.

To analyze a PKS M = S, R, S 0 , AP, L ( 1 ), TOrPEDO uses the three-valued model checking framework based on Theorem 1. The model checking result is provided as output by the analysis phase of TOrPEDO, whose behavior is described in Algorithm 1. The procedure Ctp KS (Compute Topological Proofs) to compute x-TPs is described in Algorithm 2. It takes as input a PKS M , its optimistic/pessimistic approximation, i.e., denoted generically as the KS A, and an LTL formula ψsatisfied in A-corresponding to the transformed property F(φ) (see Section 3). The three steps of the algorithm are described in the following.

Sys2LTL. Encoding of the KS A and the LTL formula ψ into an LTL formula η(C A ∪ {ψ}). The KS A = S, R, S 0 , AP c , L A (where L A is the optimistic or pessimistic function, L opt or L pes , as defined in Section 3) and the LTL formula ψ are used to generate an LTL formula where C A are sets of LTL clauses obtained from the KS A. 4 The set of clauses that encodes the KS is Table 2 . Note that the clauses in C A are defined on the set of atomic propositions AP S = AP c ∪ {p(s)|s ∈ S}, i.e., AP S includes an additional atomic proposition p(s) for each state s, which is true when the KS is in state s. The size of the encoding depends on the cardinality of C A i.e., in the worst case, 1 + |S| + |S| × |AP c | + |S| × |S|.

GetUC. Computation of the Unsatisfiable Core (UC) η(C A ∪{ψ}) of η(C A ∪ {ψ}). Since the property ψ is satisfied on A, η(C A ∪ {ψ}) is unsatisfiable and the computation of its UC core is performed by using the PLTLMUP approach [58] . Let C = {ϕ 1 , ϕ 2 , . . . , ϕ n } be a set of LTL formulae, such that η(C) = ϕ∈C ϕ is unsatisfiable, then the function η(C ) = GetUC(η(C)) returns an unsatisfiable core η(C ) = ϕ∈C ϕ of ϕ∈C ϕ. In our case, since the property holds on the KS A, GetUC(η(C A ∪ {ψ})) returns a subset of clauses η(C A ∪ {ψ}), where C A = C KS ∪ C REG such that C KS ⊆ C KS and C REG ⊆ C REG . Lemma 1. Let A be a KS and let ψ be an LTL property. Let also η(C A ∪ {ψ}) be the LTL formula computed in the step Sys2LTL of the algorithm. Then, any unsatisfiable core η(

Proof Sketch. As the property φ is satisfied by M , the LTL formula η(C A ∪{ψ}), where ψ = F(φ) must be unsatisfiable as discussed in the Section 3. Indeed, F(φ) simply perform some proposition renaming on the negation of the formula ψ. As C A encodes a KS, c∈C A c is satisfied. As such, the unsatisfiability is caused by the contradiction of some of the clauses in C A and the property ψ, and as a consequence ψ must be a part of the UC.

GetTP. Analysis of C A and extraction of the topological proof. The set C A , where C A = C KS ∪ C REG , contains clauses regarding the KS (C KS and C REG ) and the property of interest (ψ) that made the formula η(C A ∪{ψ}) unsatisfiable.

Since we are interested in clauses related to the KS that caused unsatisfiability, we extract the topological proof Ω, whose topological proof clauses are obtained from the clauses in C KS as specified in Table 3 . Since the set of atomic propositions of A is AP c = AP ∪ AP , in the table we use α for propositions in AP and α for propositions in AP .

The elements in C REG are not considered in the TP computation as, given an LTL clause G(¬p(s) ∨ ¬p(s )), either state s or s is constrained by other TP-clauses that will be preserved in the model revisions.

Lemma 2. Let A be a KS and let ψ be an LTL property. Let also η(C A ∪ {ψ}) be the LTL formula computed in the step Sys2LTL of the algorithm, where C A = C REG ∪ C KS , and let η(C A ∪ {ψ}) be an unsatisfiable core, where C A = C REG ∪ C KS . Then, if G(¬p(s) ∨ ¬p(s )) ∈ C REG , either:

(i) there exists an LTL clause in C KS that constrains state s (or state s ); or

Proof Sketch. We indicate G(¬p(s) ∨ ¬p(s )) as τ (s, s ). Assume per absurdum that conditions (i) and (ii) are violated, i.e., no LTL clause in C KS constrains state s or s and η(C A ∪ {ψ}) is not an unsatisfiable core of η(C A ∪ {ψ}).

s )} must also be satisfiable. Indeed, it does not exist any LTL clause that constrains state s (or state s ) and, in order to generate a contradiction, the added LTL clause must generate it using the LTL clauses obtained from the LTL property ψ. This is a contradiction. Thus, conditions (i) and (ii) must be satisfied.

The Analyze procedure in Algorithm 1 obtains a TP ( 4 , 6 ) for a PKS by first computing the related optimistic or pessimistic approximation (i.e., a KS) and then exploiting the computation of the TP for such KS. Proof Sketch. Assume that the Analyze procedure returns the value and a -TP. We show that every Ω-related PKS M is such that [M |= φ] ≥ x (Definition 5). If Analyze returns the value , it must be that M pes |= * φ by Lines 5 and 7 of Algorithm 1. Furthermore, by Line 7, ψ = F(φ) and A = M pes .

Let N = S N , R N , S 0,N , AP N , L N be a PKS Ω-related to M . Let η(C A ∪ {ψ}) be the LTL formula associated with A and ψ and let η(C B ∪ {ψ}) be the LTL formula associated with B = N pes and ψ. Let us consider an UC η(C A ∪{ψ}) of η(C A ∪ {ψ}), where C A = C KS ∪ C REG , C KS ⊆ C KS and C REG ⊆ C REG . We show that C A ⊆ C B , i.e., the UC is also an UC for the LTL formula associated with the approximation B of the PKS N .

-C A ⊆ C B , i.e., (C KS ∪ C REG ) ⊆ C B . By Lemma 2 we can avoid considering C REG . By construction (see Line 2 of Algorithm 2) any clause c ∈ C KS belongs to one rule among CR, CL pes, , CL pes,⊥ or c = c i :

• if c = c i then, by the rules in Table 3 , there is a TPI-clause {S 0 } ∈ Ω. By Definition 4, S 0 = S 0 . Thus, c i ∈ C B since N is Ω-related to M . • if c ∈ CR then, by rules in Table 3 , there is a TPT-clause s, T ∈ Ω where s ∈ S and T ⊆ R. By Definition 4, Table 3 , there is a TPP-clause s, α, L(s, α) ∈ Ω where s ∈ S and α ∈ AP . By Definition 4, L (s, α) = L(s, α). Thus, c ∈ C B since N is Ω-related to M .

Since N is Ω-related to M , it has preserved the elements of Ω. Thus η(C A ∪{ψ}) is also an UC of C B . It follows that [N |= φ] = .

The proof from the case in which Analyze procedure returns the value ? and a ?-TP can be derived from the first case. This Lemma allows us to prove the following Theorem. The analysis and re-check algorithms assume that the three-valued LTL semantics is considered. While the thorough LTL semantics [10] has been shown to provide an evaluation of formulae that better reflects the natural intuition, the two semantics coincide in the case of self-minimizing LTL formulae. In this case, our results are correct also w.r.t. the thorough semantics. Note that, as shown in [24] , most practically useful LTL formulae are self-minimizing. Future work will consider how to extend the analysis and re-check to completely support the thorough LTL semantics.

We implemented TOrPEDO as a Scala stand alone application and made it available online [62] . We evaluated how the analysis helps in creating models revisions and how frequently running the re-check algorithm allows the user to avoid the re-execution of the analysis algorithm from scratch.

We considered a set of example PKSs proposed in the literature to evaluate the χChek [20] model checker and defined a set of properties (see Table 4 ) inspired by the original properties and based on the LTL property patterns [18] . 5 support ( 2 ). We checked how the size of the proofs compares w.r.t. the size of the original models. Intuitively, since the proofs represent constraints Table 5 summarizes the obtained results (columns under the label analysis). We show the cardinalities |S|, |R| and |AP | of the sets of states, transitions, and atomic propositions of each considered PKS M , the number |?| of couples of a state s with an atomic proposition α such that L(s, α) =?, the total size |M | of the model, and the size |Ω p | x of the proofs, where p indicates the considered LTL property and x indicates whether p is satisfied (x = ) or possibly satisfied (x =?). Proofs are ≈ 60% smaller than their respective initial models. Thus, we conclude that the proofs are significantly coincise w.r.t. the original model enabling a flexible design. support ( 3 ) . We checked how the results output by the re-check algorithm were useful in producing PKSs revisions. To evaluate the usefulness we assumed that, for each category of examples, the designer produced revisions following the order specified in Table 5 . The columns under the label re-check contain the different properties that have been analyzed for each category. A cell contains if the re-check was passed by the considered revised model, i.e., a true value was returned by the re-check algorithm, otherwise. The dash symbolis used when the model of the corresponding line is not a revision (i.e., the first model of each category) or when the observed property was false in the previous model, i.e., an x-TP was not produced. We inspected the results produced by the re-check algorithm to evaluate their benefit in verifying if revisions were violating the proofs. Table 5 shows that, in ≈ 32% of the cases, the TOrPEDO re-check notified the designer that the proposed revision violated some of the clauses contained in the Ω-proof, while in ≈ 78% the re-check allowed designers to avoid re-runnning the analysis (and thus the model checker). Scalability. The analysis phase of TOrPEDO combines three-valued model checking and UCs computation, therefore its scalability improves as the performance of frameworks enhances. Three-valued model checking is as expensive as classical model checking [9] , i.e., it is linear in the size of the model and exponential in the size of the property. UCs computation is FPSPACE complete [55] . In our cases running TOrPEDO required on average 8.1s and for the callee examples, 8.2s for the caller examples, and 7.15s for the caller-callee examples. 6 However, while model checking is currently supported by very efficient techniques, UCs computation of LTL formulae is still far from being applicable in complex scenarios. For example, we manually designed an additional PKS with 10 states and 5 atomic propositions and 26 transitions and defined a property satisfied by the PKS and with a -TP proof that requires every state of the PKS to be constrained by a TPP-clause. We run TOrPEDO and measure the time required to compute this proof. Computing the proof required 1m33s. This results show that TOrPEDO has a limited scalability due to the low efficiency of the procedure that extracts the unsatisfiable core. For an analysis of the scalability of the extraction of the unsatisfiable core the interested reader can refer to [58] . We believe that reporting the current lack of FM techniques to support the proposed framework (that, as just discussed, is effective in our preliminary evaluation), is a further contribution of this paper.

Partial knowledge has been considered in requirement analysis and elicitation [46, 45, 38, 13] , in novel robotic planners [40, 41, 43] , software models [66, 65, 22, 1] , and testing [15, 63, 67] . Several researchers analyzed the model checking problem for partially specified systems [44, 12] , considering both threevalued [37, 25, 9, 10, 28] and multi-valued [30, 11] semantics. Other works apply model checking to incremental program development [33, 6] . However, all these model checking approaches do not provide an explanation on why a property is satisfied, by means of a certificate or proof. Although several works have tackled this problem [4, 60, 50, 49, 29, 16] , differently from this work, they mostly aim to automate proof reproducibility.

Tao and Li [61] propose a theoretical solution to model repair: the problem of finding the minimum set of states in a KS which makes a formula satisfiable. However, the problem is different from the one addressed in this paper. Furthermore, the framework is only theoretical and based on complete systems.

Approaches were proposed in the literature to provide explanations by using different artifacts. For example, some works proposed using witnesses. A witness is a path of the model that satisfies a formula of interest [7, 34, 48] . Other works (e.g., [31, 59] ) studied how to enrich counterexamples with additional information in a way that allows better understanding the property violation. Work has also been done to generate abstractions of the counterexamples that are easier to understand (e.g., [21] ). Alur et al. [2] analyzed the problem of synthesizing a controller that satisfies a given specification. When the specification is not realizable, a counter-strategy is returned as a witness. Pencolé et al. [51] analyzed model consistency, i.e., the problem of checking whether the system run-time behaviour is consistent with a formal specification. Bernasconi et al. [4] proposed an approach that combines model checking and deductive proofs in a multi-valued context. The notion of topological proof proposed in this work is substantially different from the notion of deductive proof.

Some works (e.g., [52, 54] ) considered how to understand why a property is unsatisfiable. This problem is different from the one considered in this paper.

Approaches that detect unsatisfiable cores of propositional formulae were proposed in the literature [47, 39, 17, 32, 57] . Understanding whether these approaches can be re-used to develop more efficient techniques to detect the unsatisfiable cores of LTL formulae is definitely an interesting future work direction, which deserves to be considered in a separate work since it is far from trivial.

We have proposed TOrPEDO, an integrated framework that supports the iterative creation of model revisions. The framework provides a guide for the designer who wishes to preserve slices of her model that contribute to satisfy fundamental requirements while other parts of the model are modified. For these purposes, the notion of topological proof has been formally and algorithmically described. This corresponds to a set of constraints that, if kept when changing the proposed model, ensure that the behavior of the model w.r.t. the property of interest is preserved. Our Lemmas and Theorems prove the soundness of our framework, i.e., how it preserves correctness in the case of PKS and LTL. The proposed framework can be used as baseline for other FM frameworks, and can be extended by considering other modeling formalisms that can be mapped onto PKSs.

TOrPEDO was evaluated by showing the effectiveness of the analysis and re-check algorithms included in the framework. Results showed that proofs are smaller than the original models, and can be verified in most of the cases using a simple syntactic check, paving the way for an extensive evaluation on real case scenarios. However, the scalability of existing tools, upon which TOrPEDO is based, is not sufficient to efficiently support the proposed framework when bigger models are considered.

From under-approximations to over-approximations and back

Counter-strategy guided refinement of GR(1) temporal logic specifications

Principles of Model Checking

From model checking to a temporal proof for partial models

From model checking to a temporal proof for partial models: preliminary example

The software model checker blast

Symbolic model checking using sat procedures instead of bdds

A manifesto for model merging

Model checking partial state spaces with 3-valued temporal logics

Generalized model checking: Reasoning about partial state spaces

Model checking with multi-valued logics

Multi-valued symbolic model-checking

Software assurance in an uncertain world

Nusmv 2: An opensource tool for symbolic model checking

Compositional specifications for ioco testing

Witnessing network transformations

A scalable algorithm for minimal unsatisfiable core extraction

Patterns in property specifications for finite-state verification

A framework for multi-valued reasoning over inconsistent viewpoints

χChek: A model checker for multi-valued reasoning

A single-instance incremental SAT formulation of proof-and counterexample-based abstraction

Partial models: Towards modeling and reasoning with uncertainty

Ltsa-ws: a tool for model-based verification of web service compositions and choreography

Model checking vs. generalized model checking: Semantic minimizations for temporal logics

Abstraction-based model checking using modal transition systems

On the expressiveness of 3-valued models

LTL generalized model checking revisited

LTL generalized model checking revisited. International journal on software tools for technology transfer

Certifying proofs for LTL model checking

Multi-valued model checking via classical model checking

Proof-like counter-examples

Minimal unsatisfiable core extraction for SMT

Extreme model checking

A temporal logic based theory of test coverage and generation

Semantical considerations on modal logic

From complementation to certification

A modal process logic

Deriving event-based transition systems from goal-oriented requirements models

Algorithms for computing minimal unsatisfiable subsets of constraints

Multi-robot LTL planning under uncertainty

Towards multi-robot applications planning under uncertainty

Supporting verificationdriven incremental distributed design of components

A verification-driven framework for iterative design of controllers. Formal Aspects of Computing

Dealing with incompleteness in automatabased model checking

COVER: Change-based Goal Verifier and Reasoner

Integrating goal model analysis with iterative design

Boosting minimal unsatisfiable core extraction

Certifying model checkers

From falsification to verification

From model checking to a temporal proof

Diagnosing discrete event systems using nominal models only

Behavioral diagnosis of LTL specifications at operator level

An integration of model checking with automated proof checking

Sorry Dave, I'm Afraid I Can't Do That: Explaining Unachievable Robot Tasks Using Natural Language

On the complexity of computing minimal unsatisfiable LTL formulas

Enhancing unsatisfiable cores for LTL with information on temporal relevance

Enhanced unsatisfiable cores for QBF: Weakening universal to existential quantifiers

Finding minimal unsatisfiable subsets in linear temporal logic using BDDs

A game-based framework for ctl counterexamples and 3-valued abstraction-refinement

Evidence-based model checking

The complexity of linear-time temporal logic model repair

Testing concurrent systems: A formal approach

Partial behaviour modelling: Foundations for incremental and iterative model-based software engineering

Supporting incremental behaviour model elaboration

Synthesis of partial behavior models from properties and scenarios

Compositional testing with ioco

), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use

Acknowledgments. This work has received funding from the European Research Council under the European Union's Horizon 2020 research and innovation programme (grant agreement No 694277).