Projet phase 1
Note : toutes les propriétés CTL mentionnées devront être exécutables et vraies dans le réseau de Petri associé.
Prendre connaissance du réseau de Petri proposé
Ce réseau modélise 3 chaînes de production en parallèle. Les places P1, P5 et P9 représente les matériaux de départ (avec un stock fini), les places P8, P7 et P11 les éléments produits par chaque chaîne. Pour produire chaque chaîne utilise un des deux outils proposés ou les deux (places outils1 et outils2). Les outils ne peuvent être utilisés que par une chaîne à la fois.
Donnez les forumles CTL associées à chacune des phrases suivantes et vérifier les propriétés sur le système proposé
- il n’est pas possible d’assembler avec l’outil1 en même temps dans les chaîne 1, 2 et 3
- Les outils lorsqu’ils sont utilisés finissent toujours par être libérés (1 formule par outils)
- l’outil 1 est toujours soit utilisé, soit libre pour 1 usage unique
Est-ce que l’une de ces propriétés est fausse ? Si oui, corrigez le réseau de Petri (le système) pour que la propriété soit vrai.
Lesquelles de ces propriétés sont
- de la sûreté ?
- de la vivacité ?
- de l’accessibilité ?
Projet phase 2
Note : toutes les propriétés CTL mentionnées devront être exécutables et vraies dans le réseau de Petri associé. Parfois les propriétés permettent de détecter des problèmes dans la modélisation et de les corriger, c’est intéressant de le noter dans ce cas.
Note : un fichier xml du réseau modifié sera à rendre sur Moodle
Evolution du système
Ajoutez deux assemblages de pièces
- les pièces en P8 et P7 sont assemblés ensemble avec outils1 et outils3
- les pièces en P7 et P11 sont assemblés ensemble avec outils2 et outils3
Nouvelles propriétés
Donnez la propriété CTL associée à la phrase suivante et vérifiez la sur votre système
- le stock de fin finit toujours par être égal en pièces P17 et P18
Donnez ici en langage naturel et en formules CTL de nouvelles proriétés de votre choix en précisant le type de propriété dont il s’agit
Projet phase 3
Note : un fichier xml du réseau modifié sera à rendre sur Moodle
Il faut complexifier, rendre plus réaliste le système. Vous pouvez, si besoin utiliser les arcs spéciaux vus en cours et les sous-réseaux observateurs pour la vérification. Vous pouvez vous baser sur des ressources externes comme des articles, des site internet, des cours en ligne etc. Merci de préciser vos sources dans ce cas.
- forumler en langage naturel (comme plus haut) le fonctionnement de votre nouveau système et indiquez les modifications apportées en conséquences dans le réseau de Petri.
- formuler en langage naturel et en CTL de nouvelles propriétés et les vérifier
Bonus
Note : un fichier xml du réseau modifié sera à rendre sur Moodle
Il faut complexifier, rendre plus réaliste le système de feux de circulation du tutoriel. Vous pouvez, si besoin utiliser les arcs spéciaux vus en cours et les sous-réseaux observateurs pour la vérification. Vous pouvez vous baser sur des ressources externes comme des articles, des site internet, des cours en ligne etc. Merci de préciser vos sources dans ce cas.
- forumler en langage naturel (comme plus haut) le fonctionnement de votre nouveau système et indiquez les modifications apportées en conséquences dans le réseau de Petri.
- formuler en langage naturel et en CTL de nouvelles propriétés et les vérifier