Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
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 ...