Satisfiability checker

Such logical relationships between dynamic properties can be very useful in the analysis of (both simulated as well as empirical) scenarios, especially when used in combination with the TTL Checker Tool mentioned earlier. For example, for the empirical trace 1, checking GPl pointed out that this properly was not satisfied. As a result, by a refutation process (following the tree in Fig. 6 top-down) it could be concluded that either IPl or IP2 failed (or a comhinafion of them). When, after further checking, 1P2 was found to be the cause of the failure, the analysis could proceed by focusing on LPl and LP2. Evenmally, LPl was found satisfied, whereas LP2 failed. Thus, (part of) the source of the incident could he reduced to failure of LP2, i.e., there was an agent (namely the pilot of the Hercules) that believed to have the permission to take off, whilst this was not communicated by the tower. A discussion with our domain expert confirmed that this was indeed the case. One level deeper, such local properties can even be related to executable properties. For instance, the failure of LP2 can be explained because the Hercules pilot applied property EPS. A full connection of local properties to executable properties is beyond the scope of this paper, but a detailed discussion can be found in [10]. 

Using the TTL Checker, all dynamic properties introduced in Sect. 6.1 have been checked against the three simulation traces discussed in Sect. 5 as well as the empirical trace discussed in Sect. 4.2. The results of these checks are shown in Table 3 (where X denotes satisfied ). As can be seen from the table, scenario 2 is indeed a nominal case in which aU expected properties hold. In contrast, in scenario 1, two simultaneous take-offs at crossing ranways occur (since GPl fails), which can evenmally be related to an incorrecdy derived behef of permission for take-off (failure of LP2). However, since the situation is corrected on time (GP2 succeeds), no collision occurs in this scenario. In scenario 3, GPl also fails, but in addition GP2 fails, which can be related partly to failure of LP3 (the simultaneous take-offs are observed, but too late) and to failure of LP6 (once the tower beheves that there are simultaneous take-offs, it is too late to communicate an abort request). As a result, the coUision is not prevented. As can be seen, the same system properties failed for the empirical trace as for scenario 1, which makes sense because these scenarios are identical. 

For a given state machine M and a temporal logic expression e, we can perform model checking. A model checker searches all possibilities of behaviors produced by M and checks whether the behaviors satisly the expression e. If the behaviors satisfy e then the model checker outputs yes otherwise no. For the latter case, it also produces a counter-example which is a concrete trace that violates e. 

A SLIM model can be evaluated using model checking techniques, in order to guarantee that it satisfies the required functional properties. To this aim, the model can be translated into a Labeled Transition System (LTS) and exhaustively analyzed by the model checker to check whether the properties hold. If a property does not hold, a counterexample trace can be generated to show an execution trace of the model that violates the property. To cope with the state explosion problem, advanced techniques can be applied, in particular sjun-bolic techniques based on Binary Decision Diagrams (BDD) [9] and SAT-based Bounded Model Checking [4,5,22,18] (BMC). Verification can also benefit from advanced techniques for compihng temporal properties into a symbolic LTS [12]. 

It can be used to formally verify the probabilistic model. Since the probability property was introduced to describe the failure behaviours of a component, the model checker can help to check criteria that the probability values must satisfy. 

OCRA allows to associate to a component a behavioral model representing its implementation. The language used for the behavioral model is SMV, the input language of the NuSMV model checker [10]. OCRA checks if the SMV model is a correct implementation of the specified component simply calling NuSMV to verify if the SMV model satisfies the implication A -> G for every contract (A, G) of the component. 

We consider CADP like a black-box. Yet, we should provide all inputs our translation generates LNT file, additional inputs must be presented depending on the concerned tool. For example, model-checker tool verifies if LNT specification satisfies a property expressed in temporal logic. In this case, we also specify a set of properties as a second input. After analyzing, CADP gives useful results for the correction of the initial model. For example, model-checker gives a false/true response for every checked property. 

So my proposal is that for the purpose of recording the epistemology of a safety case, models should be expressed as systems of constraints rather than as simulation models less is more. Until fairly recently, it would have been difficult to validate systems of constraints unlike simulation models, it was not feasible to run experimental calculations to check the predictions of the model against intuition and reality. Fortunately, we now have technology such as infinite bounded model checkers, based on highly effective constraint solvers for satisfiability modulo theories (SMT) that allow exploration of constraint-based models (see [18,19] for some simple examples). 

Then, the checker hands the generated symbolic expression to an SMT solver that checks if the expression is satisfiable. If so, a solution for the negated property was found, i.e., the property cannot always be true and, thus, was proven wrong. LLBMC uses the Boolector [6] SMT solver. CBMC supports several... 

---