inria-00466158, version 1
Statistical abstraction and model-checking of large heterogeneous systems
N° RR-7238 (2010)
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.
- a – INRIA
- b – Université de Rennes 1
- 1 :
- CNRS : UMR5104 – Université Joseph Fourier - Grenoble I – Institut National Polytechnique de Grenoble (INPG)
- 2 :
- CNRS : UMR6074 – INRIA – Institut National des Sciences Appliquées (INSA) - Rennes – Université de Rennes 1
- Collaboration : Verimag
- Domaine : Informatique/Modélisation et simulation
- Mots-clés : Statistical Model-Checking – BIP – Abstraction
- Référence interne : RR-7238
- inria-00466158, version 1
- http://hal.inria.fr/inria-00466158
- oai:hal.inria.fr:inria-00466158
- Contributeur :
- Soumis le : Lundi 22 Mars 2010, 18:46:01
- Dernière modification le : Mardi 9 Novembre 2010, 16:40:10
Documents associés
Exporter