Numerical and statistical approaches for model checking of stochastic processes

Résumé : Nous proposons dans cette thèse plusieurs contributions relatives à la vérification quantitative des systèmes. Cette discipline vise à évaluer les propriétés fonctionnelles et les performances d'un système. Une telle vérification requiert deux ingrédients : un modèle formel de représentation d'un système et une logique temporelle pour exprimer la propriété considérée. L'évaluation est alors faite par une méthode statistique ou numérique. La complexité spatiale des méthodes numériques, proportionnelle à la taille de l'espace d'états, les rend impraticables si les systèmes présentent une combinatoire importante. La méthode de comparaison stochastique basée sur les chaînes de Markov censurées réduit la mémoire occupée en restreignant l'analyse à un sous-ensemble des états de la chaîne originale. Dans cette thèse nous fournissons de nouvelles bornes dépendant de l'information disponible relative à la chaîne. Nous introduisons une nouvelle logique temporelle quantitative appelée Hybrid Automata Stochastic Logic (HASL), pour la vérification des processus stochastiques à événements discrets (DESP).HASL emploie les automates linéaires hybrides (LHA) pour sélectionner des préfixes de chemins d'exécution d'un DESP. LHA permet de collecter des informations élaborées durant la génération des chemins, fournissant ainsi à l'utilisateur un moyen d'exprimer des mesures sophistiquées. HASL supporte donc des raisonnements temporels mixés avec une analyse à base de récompenses. Nous avons aussi développé COSMOS, un outil qui implémente la vérification statistique de formules HASL pour des réseaux de Petri stochastiques. Les ateliers flexibles (FMS) ont souvent été modélisés par des réseaux de Petri. Cependant le modélisateur doit avoir une bonne connaissance de ce formalisme. Afin de faciliter cette modélisation nous proposons une méthodologie de modélisation compositionnelle orientée vers les applications qui ne requiert aucune connaissance des réseaux de Petri.
Type de document :
Thèse
Other [cs.OH]. École normale supérieure de Cachan - ENS Cachan, 2012. English. <NNT : 2012DENS0025>


https://tel.archives-ouvertes.fr/tel-00751927
Contributeur : Abes Star <>
Soumis le : mercredi 14 novembre 2012 - 15:12:17
Dernière modification le : vendredi 29 juillet 2016 - 03:44:13

Fichier

Djafri2012.pdf
Version validée par le jury (STAR)

Identifiants

  • HAL Id : tel-00751927, version 1

Citation

Hilal Djafri. Numerical and statistical approaches for model checking of stochastic processes. Other [cs.OH]. École normale supérieure de Cachan - ENS Cachan, 2012. English. <NNT : 2012DENS0025>. <tel-00751927>

Exporter

Partager

Métriques

Consultations de
la notice

456

Téléchargements du document

256