Dynamic Verification of SystemC with Statistical Model Checking

Van Chan Ngo 1 Axel Legay 2 Jean Quilbeuf 2
1 ESPRESSO - Synchronous programming for the trusted component-based engineering of embedded systems and mission-critical systems
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
2 ESTASYS - Efficient STAtistical methods in SYstems of systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Résumé : Beaucoup de systèmes embarqués et temps réel ont un comportement probabiliste inhérente (données de capteurs, matériels peu fiables, ...). Dans ce contexte, il est crucialpour évaluer les propriétés du système telles que “ la probabilité’ qu’un matériel particulier ne fonctionne pas”. Ces propriétés peuvent être évaluées en utilisant le probabilistic model checking. Cependant, cette technique échoue sur les modèles représentant les systèmes embarqués et temps réel réalistes en raison de l’espace explosion de l’état. Pour surmonter ce problème, nous proposons un cadre de vérification sur la base Statistical Model Checking. Notre cadre est en mesure d’évaluer les propriétés probabilistes et temporelles sur les grands systèmes modélisés dans SystemC, un langage de modélisation au niveau du système standard. Il est pleinement mis en oeuvre comme une extension du modèle statistique Plasma-lab checker. Nous illustrons notre approche sur une étude de cas du système multi-ascenseur.
Type de document :
Rapport
[Research Report] RR-8644, INRIA Rennes - Bretagne Atlantique, équipe ESTASYS; INRIA. 2014, pp.25
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01089742
Contributeur : Van Chan Ngo <>
Soumis le : lundi 21 septembre 2015 - 14:00:04
Dernière modification le : mercredi 2 août 2017 - 10:06:50
Document(s) archivé(s) le : mardi 29 décembre 2015 - 08:58:24

Fichiers

RR-8644.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01089742, version 3
  • ARXIV : 1412.0885

Citation

Van Chan Ngo, Axel Legay, Jean Quilbeuf. Dynamic Verification of SystemC with Statistical Model Checking. [Research Report] RR-8644, INRIA Rennes - Bretagne Atlantique, équipe ESTASYS; INRIA. 2014, pp.25. 〈hal-01089742v3〉

Partager

Métriques

Consultations de
la notice

545

Téléchargements du document

65