Cours du 3 mars 2008

de 8h15 à 9h15

J'ai traité :

- RDP (suite) , conflit, parallélisme, synchro, partage de ressource, sémaphore
- RDP(suite), Test à zéro, RDP coloré, RDP interprété, Matrices
- GRAFCET, différences GRAFCET/RDP
- Début de B événementiel : le cours se trouve dans le polycopié Spec1 et ICI, y voir aussi la porte en B classique vs la porte en B événementiel

Ces points sont des questions du DS

Prochain cours :
- fin B événementiel

- vérification de propriétés avec LTSA

- preuve vs model-checking (un exemple ici :

- Exposé au CNRIUT de Brest (2006)

P.S.

Je vous ai préparé une liste et pointeurs vers les prouveurs et model-checkers disponibles dans le monde, ICI