Master d’informatique 2006 2007 de l’université Paris VI
sacc
Mini-projets SACC

Le contrôle continu de l’UE SACC sera validé par un mini-projet. Ce mini-projet remplace les travaux dirigés et devra correspondre en gros à la même charge de travail (eq. 2h/semaine à partir de la deuxième semaine).

Quatre types de projet sont proposés :

  1. Projet model-checking
  2. Projet bibliographie
  3. Projet assistant de preuve
  4. Projet programmation

Pour chaque projet un petit rapport devra être rédigé.

IMPORTANT : Le choix du projet doit être effectué au plus tard lors de la 3ème séance de cours. Le projet sera rendu au plus tard à la 7ème séance.

Projets model-checking

Nombre de participants : 2 par groupe

Il s’agira de développer un modèle de système non-trivial (ex. : machine à café réaliste, ascenseur, passage à niveau de train, diner de philosophes, etc.) au sein d’un outil de model-checking.

Nous utiliserons le Concurrency workbench que l’on peut récupérer à cette adresse. On l’associera au Bisimulation game game disponible à cette adresse

Il faudra spécifier les propriétés que l’on veut vérifier sur le modèle en utilisant soit des spécifications sous forme de processus (tests d’équivalence) soit en utilisant des formules de logique temporelle (mu-calcul modal).

Projets bibliographie

Nombre de participants : 1

Il s’agira de lire un article scientifique, éventuellement ses prérequis, et d’en extraire un rapport de type fiche de lecture détaillée. On prendra soin, en particulier, d’illustrer les concepts importants par des exemples originaux (différents de ceux de l’article).

Aspects sémantiques

- Testing equivalence (équivalence basée sur la notion d’observateur, me contacter le papier n’est pas disponible en version électronique)

Variantes de CCS

- Reversible CCS En PDF
- A Language for value-passing CCS En PS
- Synchronous CCS (à venir)

Vérification de CCS

- Modal mu-calcul et CCS (logique temporelle pour la vérification, me contacter le papier n’est pas disponible en version électronique)
- Mobility workbench (au coeur de l’outil de vérification, me contacter le papier n’est pas disponible en version électronique)

Projet assistant de preuve

Nombre de participants : 1 ou 2 en fonction de la taille du projet

Il s’agira d’implémenter dans un assistant de preuve (type Coq ou Isabelle ou autre) certaines définitions du cours et de vérifier formellement certaines propriétés.

- On commencera par les définitions de syntaxe du cours 1.
- On étudiera également les définitions sémantiques du cours 2.

Le rapport sera généré automatiquement via l’autodocumentation (genre coqdoc).

Projet programmation

Nombre de participants : 1 ou 2 en fonction de la taille du projet

Certains concepts vus en cours peuvent être automatisés (ex. calcul des noms libres, calcul des transitions possibles, etc.). Le projet consistera donc en la programmation dans un langage de programmation libre (de préférence fonctionnel type Ocaml mais ce n’est pas obligatoire) d’une ou plusieurs de ces tâches automatisables.

Voici des sujets possibles :
- Interprète de CCS
- Génération automatique de toutes les transitions possibles
- Preuve (arbre d’inférence) pour une transition

Un rapport sera rendu avec le projet.


Retour à la page de l’UE