Contact

Paolo Ballarini paolo.ballarini@centralesupelec.fr

Objectifs du cours

L'objectif du cours est de comprendre et savoir utiliser les méthodes formelles pour l'analyse des modèles stochastiques. En commencent par une aperçue de l'approach du model-checking classique pour les modèles non-probabiliste et en passant par une introduction aux principaux type de modèles stochastiques y compris les chaines de Markov à temps-discret ainsi que celles à temps-continu, les élèves vont en suit apprendre l'extension du model-checking au cadre des modèles stochastiques. Ceci comport l'etudes des principaux algorithms pour la verification des propriétés formellement exprimées à travers des formules d'une logique temporelle probabiliste

Déroulé du cours

14 créneaux d'1h30 (21 HPE).

• CM1 (1h30)
  • Introduction, motivation, contexte
  • Notion de vérification formelle automatique d'un système (model checking)
  • Systèmes probabilistes: motivation, exemples
  • Notion de vérification formelle automatique d'un système probabiliste
  • Modèles non-probabilistes: systèmes de transitions
  • Logiques temporelles pour les modèles non-probabilistes: LTL et CTL
  • Algorithm de model-checking CTL
• CM2 (1h30)
  • Notions de théorie des probabilité: événement, mesure de probabilité, espace de probabilité
  • chaines de Markov temps-discret (DTMC), espace de probabilité sur le trajectoires d'un DTMC
  • atteignabilité probabiliste et atteignabilité probabiliste bornée
  • distribution à l'etat transient d'un DTMC (transient-state distribution)
  • distribution à l'etat stable d'un DTMC (steady-state distribution)
• TD1 (1h30)
  • Exercises sur l'application de l'atteignabilité probabiliste non-bornée et bornée
  • Exercises sur solution à l'état transient d'un modèle DTMC
  • Exercises sur solution à l'état stable d'un modèle DTMC (différentes cas)
• CM3 (1h30)
  • Extension probabiliste de la logique CTL: la logique PCTL
  • Types de formules PCTL
  • Equivalences entre CTL et PCTL
  • Verification de formules PCTL de type NEXT
  • Verification de formules PCTL de type UNTIL borné
  • Verification de formules PCTL de type UNTIL
• TD2 (1h30)
  • Exercises sur la versification des formules PCTL sur des modèles DTMC
  • Equivalence entre formule PCTL qualitative est formule CTL correspondantes
  • Un problème de modélisation DTMC et verification des propriétés
• TP1 (1h30)
  • Installation et prise en main de l'outil de model checking probabiliste PRISM
  • Développement des exemples DTMCs traités pendant les cours et le TD1
  • Développement des propriétés PCTL et verification
  • Mise en ouvre et execution d'un experiences de verification paramétrique avec PRISM
• CM4 (1h30)
  • Modèles DTMCs enrichis avec des rewards
  • Types de propriétés des reward et variables aléatoires correspondants: reward-instantaneous, reward-cumulé
  • Espérance des variables aléatoires des reward
  • Extension de la logique PCTL avec des formules de rewards
  • Exemples de verification des formules PCTL de reward
  • Utiliser les rewards dans PRISM
• CM5 (1h30)
  • chaines de Markov temps-continu (CTMC), espace de probabilité sur le trajectoires d'un CTMC
  • Rate matrix, Infinitesimal generetor matrix, embedded DTMC
  • atteignabilité probabiliste et atteignabilité probabiliste bornée pour le CTMC
  • distribution à l'etat transient d'un CTMC (transient-state distribution)
  • Uniformisation
  • Logique temporelle CSL
  • Verification de propriété qualitative
  • Verification de propriété quantitative
• TD3 (1h30)
  • Exercises sur la versification des formules CSL qualitative sur des modèles CTMC
  • Quelque problèmes des modélisation CTMC: filles d'attentes, machines en pannes, accès mutuellement exclusif
  • Verification des propriétés avec PRISM
• CM6 (1h30)
  • distribution à l'etat stable d'un CTMC (steady-state distribution)
  • Verification des propriétés CSL de steady-state
  • Modèles CTMCs enrichis avec des rewards
  • Espérance des variables aléatoires des reward CTMC
  • Extension de la logique CSL avec des formules de rewards
  • Exemples de verification des formules CSL de reward
  • Utiliser les rewards CSL dans PRISM
• TD4 (1h30)
  • Exercises sur la versification des formules CSL quantitative sur des modèles CTMC
  • Quelque problèmes des modélisation CTMC: filles d'attentes, machines en pannes, accès mutuellement exclusif
  • rajoute de structures de rewards et verification de propriétés de rewards avec PRISM
• CM7 (1h30)
  • Introduction au model-checking statistique
  • Simulation stochastique
  • Estimation de l'nterval de confiance pour une formule d'un logique probabiliste
  • Autre logiques probabilistes: probabilistic-LTL, Hybrid automata specification language
  • Utilisation du simulateur stochastique dans PRISM: avantages et limitations
• TP2 (1h30)
  • Application du model checking statistique sur des modèles CTMCs de grosse tailles avec PRISM
• Projet (hors HPE)
  • Development d'un etude d'analyse de performance complete sur des cas d'etudes réalistes (p.e. analyse des performance de protocoles réseaux de communication, algorithmes distribué, systemes des manufactures, modèles biologiques)
• Examen ecrit (1h30)

EVALUATION

La note finale est calculée par composition entre la note de l'examen écrit et du projet à rendre en forme d'un compte rendu.

OUTILS

• PRISM model checker probabiliste
• Cosmos model checker statistique

BIBLIOGRAPHIE

• Principles of model checking. C. Baier, J-P Katoen
• Modeling and Analysis of Stochastic Systems. V.G. Kulkarni
• Model checking algorithms for CTMCs. C. Baier, B. Haverkort, H. Hermanns, J-P Katoen
• Stochastic model checking. M. Kwiatkowska, G. Norman, and D. Parker.