Causality in Systems
Software controls cars, planes, medical equipment, nuclear power plants and many other safety-critical embedded and cyber-physical systems. The malfunctioning of those systems can harm people physically, threaten the environment or cause significant financial losses. With the increasing complexity of modern safety-critical systems, the need for model based engineering methods that both help in designing such systems and in assessing their safety and correctness is becoming increasingly apparent. Due to the size of the systems, traditional techniques like reviews and testing, on the one hand, and manual fault tree analysis or failure mode and effect analysis, on the other hand, can only be applied to limited parts of the system. The main reason for this limitation lies in the vast amount of time and resources that is consumed by manually executing those techniques. 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 is an established technique for the automated analysis of system properties. If a model of the system and a formalized property are given to the model checker, it automatically checks whether it can find property violations. In case a safety property is violated, the model checker returns a counterexample, which consists of a system execution trace leading to the property violation. Our QuantUM tool allows for automatic translation of system and software architecture models in UML and SysML to the input language of the probabilistic model checker PRISM.
The automatic translation of the UML model to PRISM saves time and resources and prevents errors that where frequently introduced in the manual translation process that was previously used. The remaining challenge is the identification of the causes of the property violation and representing this information in a way that it is interpretable on the level of the UML model. The counterexamples that are computed by the model checker help in retracing the system executions leading to the property violation, but they can only be interpreted at the level of the analysis model. Our tool automatically computes causality relationships based on a complete set of counterexamples and visualizes the computed causal relationships as fault trees. Fault trees are an industrial standard technique to document graphically which combination of events can cause a system hazard.