Title :
A Framework for Qualitative and Quantitative Formal Model-Based Safety Analysis
Author :
Güdemann, Matthias ; Ortmeier, Frank
Author_Institution :
Comput. Syst. in Eng., Otto-von-Guericke Univ. Magdeburg, Magdeburg, Germany
Abstract :
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.
Keywords :
formal specification; safety-critical software; software metrics; SAML; SAML framework; model checking notation; probabilistic analysis; prototypical tool support; qualitative formal model based safety analysis; quantitative formal model; safety analysis modeling language; tool independent framework; Analytical models; Markov processes; Probabilistic logic; Probability distribution; Safety; Semantics; Syntactics; fault tolerance; formal methods; model checking; reliability;
Conference_Titel :
High-Assurance Systems Engineering (HASE), 2010 IEEE 12th International Symposium on
Conference_Location :
San Jose, CA
Print_ISBN :
978-1-4244-9091-2
Electronic_ISBN :
1530-2059
DOI :
10.1109/HASE.2010.24