Mini-projet model-checking

imt

1. Objectif

Voici le sujet de mini-projet à conduire en séance et qui sera évalué par une courte restitution orale au professeur et un rendu sur Moodle.

Vous allez former des groupes de 2 étudiants pour ce projet.

2. Choix de votre système

Choisissez un système de votre choix à modéliser en réseau de Petri avec les éléments suivants :

  • Plus le système demande de la concurrence et la synchronisation de plusieurs entités plus il sera intéressant et complexe à modéliser en réseau de Petri.

  • Inspirez-vous des systèmes que vous avez eu l’occasion de rencontrer dans les systèmes industriels ou l’informatique par exemple.

  • Je dois retrouver au moins 3 des 4 structures de bases vues en TD (parallélisme, communications asynchrones, sections crtiques, producteur/consommateur)

3. Déroulé du projet

  1. Chacun spécifie le système imaginé en français

  2. Echanger votre spécification et juger des incohérences, imprécisions, incompréhensions dues à l’utilisation de la langue française.

  3. Améliorer ensemble cette spécification pour arriver au système réellement souhaité.

  4. Modéliser votre système en réseau de Petri

  5. Spécifier les propriétés de sûreté et de vivacité de votre système

  6. Vérifier vos propriétés avec Roméo

  7. Au besoin, complexifier votre système et reprendre à l’étape 3

4. Evaluation

  1. évaluation orale :

    • en milieu de deuxième séance, le professeur passera vous voir pour vous demander de lui restituer votre système en langage naturel et les prorpiétés à vérifier dessus

    • en fin de deuxième séance, le professeur passera une deuxième fois pour lui restituer votre modélisation en réseau de Petri et en formules CTL

  2. rendu sur Moodle:

    • les spécifications textuelles initiales de chacun et la version améliorée commune

    • le fichier xml Roméo (merci d’utiliser des noms de places et de transitions compréhensibles)

    • la liste des propriétés à vérifier avec Roméo ainsi qu’une explication textuelle associée de votre compréhension des formules

5. Bonus

Pour aller plus loin vous pouvez ajouter des éléments avancés dans votre modélisation comme les arcs spéciaux de la deuxième partie du cours, ou bien le temps.

6. Compétences évaluées

  • CG1 Comprendre et analyser, synthétiser un problème et/ou une situation complexe (complexité de votre système)

  • CG4 Critiquer et décider (capacité à mettre en doute votre système et à vérifier des propriétés)

  • CG14 S’engager (participer et s’engager dans les idées)

  • CG9 Communiquer (oral en séance)