Spécifications formelles

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.