A Framework for Qualitative and Quantitative Formal Model-Based Safety Analysis

In model-based safety analysis both qualitative aspects i.e. what must go wrong for a system failure) and quantitative aspects (i.e. how probable is a system failure) are very important. For both aspects methods and tools are available. However, until now for each aspect new and independent models must be built for analysis. This paper proposes the SAML framework as a formal foundation for both qualitative and quantitative formal model-based safety analysis. The main advantage of SAML is the combination of qualitative and quantitative formal semantics which allows different analyses on the same model. This increases the confidence in the analysis results, simplifies modeling and is less error-prone. The SAML framework is tool-independent. As proof-of-concept, we present sound transformation of the formalism into two state of the art model-checking notations. Prototypical tool support for the sound transformation of SAML into PRISM and MRMC for probabilistic analysis as well as different variants of the SMV model checker for qualitative analysis is currently being developed.