Fault-Aware Modeling and Specification for Efficient Formal Safety Analysis

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. Ad- ditionally, we present conceptual changes to D CCA that improve efficiency and usability. We evaluate our work using our safety analysis tool S# ("safety sharp").
published 27.09.2016 09:00 Critical Systems: Formal Methods and Automated Verification

Publisher: Springer



For questions regarding the publication, please contact!