Spécifications formelles

Ce module a pour objectif de présenter les notions fondamentales de simulation et bisimulation entre systèmes de transitions [1]. Afin d’appliquer ces notions, nous étudions premièrement un calcul de processus dans lequel ces notions sont liées à la substituabilité entre processus. Puis, plus concrètement, nous étudierons un langage de spécification et de programmation `a modules, le langage TLA, pour lequel on retrouve les notions classiques de raffinement de programmes [2], de couple spécification/implantation et de sous-typage, déclinées formellement à partir de la définition de la simulation.

Programme

1. Simulation et bisimulation (2 cours + 2 TD) ;

• Contexte général : systèmes de transitions, sous-typage, raffinement, spécification/implantation
• Simulation et bisimulation forte, propriétés ;
• Simulation et bisimulation faible, propriétés ;
• Algorithmes de calcul de plus grande simulation / bisimulation 

2. Calcul de processus CCS (1 cours + 2 TD + 2TP) ;

• Syntaxe ;
• Sémantique par règles de réduction ;
• Équivalence structurelle, simulation, bisimulation entre processus ;
• Algorithmes de calcul de plus grande simulation / bisimulation

3. Raffinement de programmes séquentiels (1 cours + 2 TP) ;

• Cadre général : programmation / raffinement de modules, implantation en TLA ;
• Sémantique de type jeu des modules ;
• Expression du raffinement entre modules, lien avec la simulation ;
• Différents raffinements classiques, exemples.

[1] J.-F. Monin, Introduction aux méthodes formelles, Hermès, 2000.

[2] J.-R. Abrial, The B-book : Assigning Programs to Meanings, Cambridge University Press, 1996.

[3] T. Hoare, Communicating Sequential Processes, Prentice Hall International, 1985.

[4] R. Milner, Communicating and Mobile Systems : The Pi-Calculus, Cambridge University Press, 1999.