Causal Analysis and Repair of Systems

Abstract

A system consists of hardware and software components and makes life-critical decisions, for example, in a pacemaker. The interactions between the components of a system lead to a high degree of concurrency, which makes it a complex task to verify whether a system model violates a property of its specification. Different approaches exist to verify whether a system satisfies its specification. Test procedures are often used but are labor intensive and time-consuming. In contrast, Model checking tools systematically search through the state-space of a system model to verify whether a property in the specification is violated. When a model checker finds a property violation, it usually returns a counterexample in the form of an execution that leads to this property violation. Model Checkers are even more efficient in finding property violation than testing procedures. Realistic systems also consist of hardware components that can fail, for instance, due to fatigue of material. In these systems, a property violation cannot always be prevented. Safety standards such as ISO26262 ISO26262 recommend to justify by safety cases that a property violation is sufficiently improbable, and therefore the system is acceptably dependable. For a safety analysis, it does not suffice to find a single counterexample, but an enumeration of the possible property violations is needed. Causality Checking is an algorithmic method that utilizes a model checker to enumerate causes that explain every property violation in a model. In Causality Checking, a cause for a property violation is based on the counterfactual conditional that if the cause occurs, the property violation occurs, and if the cause would not have occurred, the property violation would not have occurred. In the analysis, Causality Checking compares the action sequences in the executions of a system model and computes causes in the form of ordered actions. Causality checking is implemented in the tool QuantUM, which analyzes the SysML model of a system, computes causes for the property violations of the system, and represents these causes in a fault tree. Causality checking is a promising approach to support the safety analysis of systems. The first significant contribution of this work is to extend and improve Causality Checking. For a safety analysis, it is essential to compute every possibility of the system to result in a property violation. Therefore, we propose revised cause definitions and analyses compared to that are complete and compute each cause for a property violation in a system. Furthermore, we explicitly compute the action order in a cause, which has not been done before. The results show that these order relations help to understand the occurrence of a property violation and the difference between causes where the action sets are subsets of one another. We demonstrate that Causality Checking can support the safety analysis by a case study considering an autonomous driving assistant. Contrary to manual driving, an autonomous driving assistant cannot rely on a driver and needs to be fail-operational, which means that the function to drive a car is provided, even in the event of a system failure. Therefore, we propose also a method to analyze whether the system is fail-operational. The results show that Causality Checking supports the safety analysis of a system. Furthermore, the automated nature of the presented analyses allows a developer to compare and evaluate design decisions early in the development of a system. The second significant contribution of this work is to adapt the idea of causes to real-time models. In an embedded system, such as a pacemaker, time is an essential aspect for the correctness of the system. We can describe such a timed system by a real-time model where time passes continuously within a location of the model and not explicitly by transit to another location. The timed counterexample of a real-time model contains a sequence of actions and time constraints that limit the possible delay values within a location. An assignment of every delay value in the timed counterexample is an execution. Considering that for the same timed counterexample, one execution can lead to a property violation and another execution can not. Both executions contain the same sequence of actions and differ only in the chosen delay values. Hence, Causality Checking cannot compute a cause for this violation, since it analyzes only the action sequences in an untimed system. In this thesis, we propose a dynamic and a static analysis that analyze a timed counterexample and compute causes for a property violation. The dynamic analysis compares the possible delay values in a timed counterexample. It computes causal ranges in which every delay assignment leads to a property violation and an alternative value assignment exists that does not lead to a property violation. Accordingly, the counterfactual conditional is satisfied and the causal range is causal. The static analysis is a repair method that computes alternative time constraints for a timed counterexample such that the property violation is no longer reachable. Since alternate time constraints prevent the property violation that occurs with the original time constraints, the counterfactual conditional is fulfilled and the original time constraints can be assumed as causal for the property violation. These alternative time constraints are potential repairs for the real-time model underlying the timed counterexample. The alternative time constraints affect the possible executions of the real-time model, and therefore may change the functional behavior of the real-time model. We propose an admissibility test to ensure that the altered time constraint does not change the functional behavior of the real-time model and is, therefore, a repair for the real-time model. We apply both the dynamic and static analysis to several real-time models from literature and show that the computed causes help to understand the occurrence of property violations and to prevent violations in real-time models. The presented approaches automatically compute causes for the occurrence of system failures in systems with and without real-time aspects. Integrating these approaches into an Model-driven engineering (MDE) development process may save manpower and may make systems more dependable.