Cours du 11 février 8h15-9h15

Amphi 4

Le cours s'est déroulé par une belle matinée. Ciel tout bleu. Froid sec agréable à 8h 15. Amphi bien chauffé.

11 absents du groupe 1
19 absents du groupe 2
7 absents du groupe 3
18 absents du groupe 4



J'ai traité :

• J'ai distribué une petite spec en B. Il s'est agi de faire le diagramme de transition d'états. J'ai fait un automate simple et un automate structuré (un automate de Harel).
• La prochaine fois, je ferai la spec en B événementiel
• le renommage. Illustré par des chaussettes thaïlandaises et des gants français et par un exemple en FSP(LTSA) Client/Serveur
• le produit de processus (avec FSP)
• la sémantique du losange pour le parallèlisme. Illustrations avec exemples en FSP
• processus types et instances de processus types (processus) en FSP
• un exemple de partage de ressources

Ca c'était pour avoir l'essentiel de LTSA pour pouvoir l'utiliser pour les différents exercices de td

Je suis passé alors aux

• Réseaux de Petri, avec un exemple. J'ai fait l'automate (un état est un vecteur de marquage). J'ai bien insisté : avec les RDP, il ne s'agit pas de déplacement de jetons. Un marquage d'une place avec 2 jetons n'est ni plus ni moins que dire que cette place a pour valeur l'entier 2.
• Il n'y a pas forcément conservation du nombre de jetons. Il peut y avoir dans un problème donné, un invariant qui dit par exemple que le marquage de telle place + le marquage de telle autre doit toujours être égal à 5. Mais cela n'est pas une loi générale des RDP !

J'ai distribué un texte complément au cours de Michael Jackson et un texte sur le modèle relationnel avec la notation NIAM. Bien sûr, il y aura des questions du DS sur ces textes.

J'ai à la disposition des étudiants intéressés, un texte rédigé par J.F. Monin et J. Sifakis (Prix Turing) intitulé "Eléments de classification des méthodes formelles". On y retrouve notre programme de Spec1 et celui de Spec2.