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.
Type de document :
Communication dans un congrès
8. Dagstuhl-Workshop MBEES 2012 - Model-Based Development of Embedded Systems, Feb 2012, Dagstuhl, Germany. 2012
Liste complète des métadonnées

Littérature citée [8 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00665607
Contributeur : Matthias Güdemann <>
Soumis le : vendredi 23 novembre 2012 - 18:14:50
Dernière modification le : mercredi 11 avril 2018 - 01:52:07
Document(s) archivé(s) le : dimanche 24 février 2013 - 02:40:08

Fichier

Gudemann-Lipaczewski-Struck-et...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00665607, version 1

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〉

Partager

Métriques

Consultations de la notice

501

Téléchargements de fichiers

261