Fault-aware modeling and specification for efficient formal safety analysis

Abstract

Deductive Cause Consequence Analysis (Dcca) is a model checking-based safety analysis technique that determines all combinations of faults potentially causing a hazard. This paper introduces a new fault modeling and specification approach for safety-critical systems based on the concept of fault activations that decreases explicit-state model checking and safety analysis times by up to three orders of magnitude. We augment Kripke structures and LTL with fault activations and show how standard model checkers can be used for analysis. Additionally, we present conceptual changes to Dcca that improve efficiency and usability. We evaluate our work using our safety analysis tool S# (“safety sharp”).