Formal modelling for concurrent and probabilistic systems
Synopsis.
Le développement d'un système informatique est un processus complexe qui peut très facilement comporter la presence d'erreurs dans la realisation d’un système visé à se comporter selon certains specifications. Ca c'est particulièrement vrai pour les systèmes concurrentes, cet à dire pour cet type de système dont le comportement est le résultat de l'interaction de plusieurs composants qui sont exécutés en parallèle. Dans ce cours on s’interesse à l’etude de certains languages formels pour la modelisation et analyses de systemes concurrents. Dans la premiere partie du cours on va introduire l'algèbre de processus dite CCS, qui permet de representer formellement une classe importante de systèmes, cet a dire la classe des systèmes réactifs. Avec le langage CCS on va aussi introduire les concepts fondamataux d'equivalence entre processus ainsi que la logique temporelle HML qui nous permet d'exprimer des propriétés formelles d'un système et de vérifier si un modèle CCS satisfait un propriété formelle HML. Dans la deuxième partie du cours on introduit la notion de temps et donc on va s'intéresser à la classe des automate temporisé qui nous permet de décrire formellement les systèmes dont le comportement est dépendent du temps (systèmes à temps réel). On va donc s'intéresser à la modélisation des systèmes temps réels (notamment du protocole IEEE 802.11 qui est à la base des réseaux wifi) à travers UPPAAL un outil pour la modélisation avec automate temporisés. Finalement dans la troisième partie du cours on va s'intéresser de la modélisation des systèmes probabilistes. En particulier on va introduire le formalisme de chaines de Markov à temps discrète, on va étudier leur aspects théoriques de base et on va introduire les principes des bases du model checking probabiliste, et en particulier de la logique PCTL.
Contenu.
Notion de systèmes réactif. notion de algèbre de processus. syntaxe et sémantique de l'algèbre CCS. notions d'équivalence: bisimulaiton faible et forte. Logique de Hennesy Millner. Operateurs modales de la logique HML. Satisfaction d'une formule HML contre un systèmes de transitions.
Notion d’ automate temporisée, syntaxe et sémantique. sémantique discrète pour une classe de modèles a états infinie et dense, Graphe de régions: définition et construction. La logique temporelle TCTL. Introduction à l’outil UPPAAL. Analyse d’un protocole Wifi avec UPPAAL.·
Modeles probabilistes. Chains de Markov à temps discrete. Mesures de probabilité sur l’espace de chemins d’un chain de Markov. Comportament au limite. Distribution transient et stationaire. La logique temporelle PCTL. Le modele checking probabiliste. Formules qualitatifs vs quantittatives. Algorithms de verification pour le modele checking PCTL.
Organisation.
Petites classes pour pratiquer les concepts introduits dans le cours et quelques travaux pratiques pour implanter les algorithmes de vérification associés à chacun des formalismes présentés. Utilisation des outils de modélisation/verification UPPAAL et PRISM