Causality Checking of Safety-Critical Software and Systems

The complexity of modern safety-critical systems is steadily increasing due to the amount of functionality that is implemented in those systems.In order to be able to asses the correctness and safety of these systems in a comprehensive manner automated or, at least, computer-aided techniques are needed.Model checking, a formal verification technique, provides an automated algorithmic analysis of system models and is able to check whether a formalized requirement is satisfied by the system. If the requirement is violated the model checker provides error traces, called counterexamples, which serve as witnesses for the requirement violation. While the counterexamples can be used as a debugging aid, they do not provide any obvious insight into which events are causal for the requirement violation. In order to derive the causal events from a set of counterexamples, the events of all error traces need to be manually inspected, which is an error prone and time consuming task.We propose a method complementing model checking that is called causality checking. Causality checking algorithmically computes the causal events for the violation of a requirement that is formalized as a non-reachability property. The notion of causality that we use is based on the actual cause definition by Halpern and Pearl, which in turn is based on the counterfactual argument by Lewis. Causality checking is able to compute the causal events for a property violation and also takes the order in which the events appear into account as a causal factor. Furthermore, causality checking identifies the causal non-occurrence of events. We propose a causality checking algorithm and show how it can be integrated into the state-space exploration algorithms used in qualitative model checking.The hardware of an embedded system may fail due to deterioration and affect the software that is running on this hardware and thereby cause a requirement violation. In industry negative exponentially distributed rates are used in order to specify the occurrence probability of such a hardware failure in a given time frame. In order to support a probabilistic analysis of the system we extend the causality checking approach to be applicable to probabilistic system models. The proposed probabilistic causality checking approach enables us to compute the probabilities of certain combinations of events that cause a property violation. A pure probabilistic causality checking method, as will become clear in this thesis, entails a high performance penalty for the necessary probabilistic counterexample computation. We will show how this bottleneck can be mitigated by a combination of qualitative and probabilistic causality checking.While a full state-space exploration of the case studies that we analyze is possible, we discuss the implications of an incomplete state-space exploration of the analysis model with respect to soundness and completeness of the causality checking result and present strategies that can be applied in order to increase the scalability of the causality checking approach.Furthermore, we discuss how the causality checking method can be integrated into the QuantUM framework, a method that allows for the generation of the analysis models from higher-level architectural description languages such as the unified modeling language (UML) or the systems modeling language (SysML). For the result representation we propose a temporal logic called event order logic which allows for a concise and formal representation of the causal events and the causal orderings. Furthermore, we show how formulas in event order logic, that have been computed by the causality checker, can be represented by fault trees, a method used in industry to reason about causal relationships between property violations and events. The mapping to fault trees facilitates the interpretation of the causality checking results and is a representation that is already known and used in industry.We demonstrate the applicability and usefulness of the causality checking approach on several case studies from industry and academia and discuss how causality checking can be used in an industrial safety engineering process