Mini-projet model-checking

imt

1. Objectif

Voici le sujet de mini-projet à conduire en séance et qui sera évalué par le biais d’une restitution orale.

Vous allez former 3 groupes de 4 étudiants et 2 groupes de 5 étudiants

2. Choix de votre système

Choisissez un système de votre choix à modéliser en réseau de Petri

Tip
 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 par exemple. Vous pouvez aussi choisir de modéliser un système informatique.

  1. Spécifier votre système en français

  2. Spécifier votre système sous la forme d’un réseau de Petri

3. Simuler et vérifier votre système

  1. Simuler votre réseau de Petri pour tester rapidement que le comportement est le bon par rapport à votre spécification et corrigez si nécessaire.

  2. Vérifier le plus de propriétés CTL possible sur votre réseau de Petri afin d’avoir des certitudes sur son bon fonctionnement.

4. Complexifier les choses

Vous pouvez au besoin complexifier le comportement de votre système et imaginer d’autres propriétés à vérifier dessus.

5. Evaluation

Il s’agit d’une restitution orale de votre travail de 15 minutes où tous les membres du groupe devront s’exprimer !

L’oral se découpe en 4 temps :

  1. Présentation avec des diapositives de votre système en français (la version la plus complexe obtenue), puis de sa modélisation en réseau de Petri

  2. Démonstration de la simulation de votre réseau de Petri

  3. Présentation avec des diapositives des propriétés attendues de votre système (dans leur version la plus complexe à nouveau), en expliquant à la fois en français et en logique CTL

  4. Démonstration du model-checker sur les propriétés identifiées

  5. Questions/réponses

Note
 Si certaines de vos propriétés se sont révélées fausses et que le model-checker vous a aidé à détecter et corriger des erreurs dans votre système, il est intéressant de le montrer également.

Prevoyez environ 1h de préparation de l’oral sur le temps de la deuxième séance.

Le restitution durera en tout 1h30 avec les 5 groupes et le temps de changer de groupe.

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)