Statistical Abstraction and Model-Checking of Large Heterogeneous Systems - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2010

Statistical Abstraction and Model-Checking of Large Heterogeneous Systems

Résumé

We propose a new simulation-based technique for verifying applications running within a large heterogeneous system. Our technique starts by performing simulations of the system in order to learn the context in which the application is used. Then, it creates a stochastic abstraction for the application, which takes the context information into account. This smaller model can be verified using efficient techniques such as statistical model checking. We have applied our technique to an industrial case study: the cabin communication system of an airplane. We use the BIP toolset to model and simulate the system. We have conducted experiments to verify the clock synchronization protocol i.e., the application used to synchronize the clocks of all computing devices within the system.
Fichier principal
Vignette du fichier
61170032.pdf (195.99 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00554321 , version 1 (10-01-2011)
inria-00554321 , version 2 (11-08-2014)

Licence

Paternité

Identifiants

Citer

Ananda Basu, Saddek Bensalem, Marius Bozga, Benoît Caillaud, Benoît Delahaye, et al.. Statistical Abstraction and Model-Checking of Large Heterogeneous Systems. Joint 12th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 30th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2010, Amsterdam, Netherlands. pp.32-46, ⟨10.1007/978-3-642-13464-7_4⟩. ⟨inria-00554321v2⟩
1195 Consultations
190 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More