Initiation à la spécification et la vérification

OBJECTIFS :

Présentation de modèles probabilistes et introduction à la vérification de modèles probabilistes avec la logique PCTL.

CONTENU DÉTAILLÉ DE L’ENSEIGNEMENT :

  • Chaines de Markov
  • Files d’attente (M/M/1, M/M/m, M/G/1, etc)
  • Probabilités transitoires et stationnaires
  • Réseaux de files d’attentes
  • Réseaux à forme produit (réseaux de Jackson, réseaux BCMP, etc)
  • Vérification sur les chaines de Markov et MDP avec la logique PCTL