Based on the idea and research of Matthias Güdemann, a tool-independent language for formal, model-based system-analysis was initiated. This language is named SAML (System Analysis Modeling Language). It is a well-specified language and transformation of SAML-Models into semantically equivalent models in the input-languages of popular model checkers (like PRISM and NuSMV) is mathematically proven correct.
The idea behind SAML
The core idea behind SAML (System Analysis Modeling Language) is to allow the user to model the system once and verify formal models using multiple model checkers. Thus, it is a formal tool-independent language which allows the expression of both, qualitative (non-deterministic) and quantitative (probabilistic) aspects with an automatic model transformation framework to tool-specific languages for verification engines. SAML is powerful enough to model software components, hardware components, environments and failure modes. For safety critical systems, all those aspects typically have to be considered together as single formal model.
In SAML, a model describes finite state automata that are executed in a synchronous parallel fashion with discrete time steps. The language has been explicitly designed as simple as possible, while being expressible enough for convenient modeling of large systems. Further, to translate SAML to modeling languages for third party model checking tools guaranties broad usage possibilities during the model based safety analysis.
The goal of MBSA is to give guarantees on the possible behavior of real-world systems based on a specified model. These includes, for example, event probabilities such as the probability of which and how many redundant systems have to fail in order for an airplane to crash.
In order to calculate qualitative and/or quantitative statements, a SAML model has to be transformed into a formal model suitable for other verification tools. The transformation of SAML into other formal specification languages is well defined (Güdemann2011), however a SAML model must not be transformed manually. SAML is designed to be transformed or executed for debugging purposes by a dedicated verification tool called: Verification Environment for Critical Systems. Thus, it is advised to use VECS in order to get hands-on experience with SAML.