Design Time and Run Time Formal Safety Analysis using Executable Models

Safety-critical systems can be negatively affected by faults such as component failures or environmental disturbances. One or more occurrences of such faults might lead to hazards, that is, potentially disastrous situations or conditions that may cause accidents with economical losses, environmental damage, injuries, or loss of lives. Safety analysis is the process of identifying such hazards as well as their root causes in order to assess a system's overall safety. Traditional safety analysis techniques such as Fault Tree Analysis or Failure Modes and Effects Analysis help to systematically assess system safety by informally dissecting the system's behavior and component interdependencies. However, the increasing complexity of safety-critical systems, in part due to the introduction of more and more software-based components, requires more sophisticated safety analysis techniques to thoroughly analyze system behavior with regard to faults. Additionally, traditional safety analysis techniques are not suited for the analysis of self-organizing systems, an emerging class of often safety-critical systems that change their behavior and structure during operation in a way that cannot be predicted during system development. Self-organization thus necessitates new safety analysis approaches that are at least partially conducted at run time while the system is already in operation. The contribution of this thesis is a systematic design time and run time modeling and analysis approach for safety-critical systems based on formal methods and executable models. Its main achievements are threefold: Firstly, a systematic modeling approach and the executable modeling language S# are introduced. Secondly, a safety analysis technique based on explicit-state model checking and its formal foundations are defined, increasing analysis efficiency and practical usability compared to alternative techniques. Thirdly, a unified model execution and analysis approach is used to simulate and visualize S# models and to systematically conduct design time and run time safety analyses for them with consistent semantics. The contributions are evaluated using different case studies from multiple application domains