Unifying Probabilistic and Traditional Formal Model Based Analysis

Matthias Güdemann 1 Michael Lipaczewski 2 Simon Struck 2 Frank Ortmeier 2
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
2 CSE
OVGU - Otto-von-Guericke University Magdeburg
Abstract : The increasing complexity of modern software-intensive systems makes their analysis much more difficult. At the same time, more and more of these systems are used in safety-critical environment. Model based safety analysis can help with this problem by giving provably correct and complete results, very often in a fully automatic way. Today, such methods can cope with logical as well as probabilistic questions. However, very often the models used in many model based approaches must be specified in different input languages depending on the chosen verification tool for the desired aspect, which is time consuming and often error-prone. In this paper, we report on our experiences in designing a tool independent specification language (SAML) for model based safety analysis. This allows to use only one model and analyze it with different methods and different verification engines, while guaranteeing the equivalence of the analyzed models. In particular, we discuss challenges and possible solutions to integrate SAML in the development process of real systems.
Document type :
Conference papers
8. Dagstuhl-Workshop MBEES 2012 - Model-Based Development of Embedded Systems, Feb 2012, Dagstuhl, Germany. 2012
Liste complète des métadonnées


https://hal.inria.fr/hal-00665607
Contributor : Matthias Güdemann <>
Submitted on : Friday, November 23, 2012 - 6:14:50 PM
Last modification on : Monday, October 5, 2015 - 4:59:29 PM
Document(s) archivé(s) le : Sunday, February 24, 2013 - 2:40:08 AM

File

Gudemann-Lipaczewski-Struck-et...
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00665607, version 1

Collections

Citation

Matthias Güdemann, Michael Lipaczewski, Simon Struck, Frank Ortmeier. Unifying Probabilistic and Traditional Formal Model Based Analysis. 8. Dagstuhl-Workshop MBEES 2012 - Model-Based Development of Embedded Systems, Feb 2012, Dagstuhl, Germany. 2012. <hal-00665607>

Share

Metrics

Record views

359

Document downloads

219