Dynamic Verification of SystemC with Statistical Model Checking - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2014

Dynamic Verification of SystemC with Statistical Model Checking

Résumé

Many embedded and real-time systems have a inherent probabilistic behaviour (sensors data, unreliable hardware,...). In that context, it is crucial to evaluate system properties such as “the probability that a particular hardware fails”. Such properties can be evaluated by using probabilistic model checking. However, this technique fails on models representing realistic embedded and real-time systems because of the state space explosion. To overcome this problem, we propose a verification framework based on Statistical Model Checking. Our framework is able to evaluate probabilistic and temporal properties on large systems modelled in SystemC, a standard system-level modelling language. It is fully implemented as an extension of the Plasma-lab statistical model checker. We illustrate our approach on a multi-lift system case study.
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.
Fichier principal
Vignette du fichier
RR-8644.pdf (1.11 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01089742 , version 1 (02-12-2014)
hal-01089742 , version 2 (04-12-2014)
hal-01089742 , version 3 (21-09-2015)

Identifiants

Citer

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⟩
512 Consultations
223 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More