1 Uppaal
Uppaal est disponible en version Windows, Unix et Linux à l'adresse:
http://www.uppaal.com/
Insérez dans votre fichier .bashrc la ligne suivante :
alias uppaal='/usr/local/insa/uppaal/uppaal'
Effectuez la commande source ~/.bashrc
Appel direct au model-checker : /usr/local/insa/uppaal/bin-Linux/verifyta fic.xta fic.q
Récupérez
l'ensemble des sources pour cette seconde partie
via l'archive suivante.
2 Prise en main d'Uppaal: Ex du Bit Alterné
Placez vous dans le répertoire ABP.
Le modèle du bit alterné est : ab.xta.
Vous trouverez quelques propriétés via le fichier : ab.q
L'appel à Uppaaal se fait via la commande uppaal ab.xta
- Simulez le modèle du protocole,
- Vérifiez les exemples de propriétés fournies.
3 John et Frédéric
John va au travail soit en voiture (entre 30 et 40 minutes), ou en bus (au moins 60 minutes). Frédéric part travailler en voiture (entre 20 et 30 minutes), ou en covoiturage (entre 40 et 50 minutes). Aujourd'hui john quitte la maison entre 7H10 et 7H20, et Frédéric arrive au travail entre 8H00 et 8H10. On sait aussi que John arrive au travail entre 10 et 20 minutes après que Frédéric quitte sa maison.
Placez vous dans le répertoire John_Fred.
Vous trouverez dans le fichier dechter.xta un "squelette" de modélisation.
Vous trouverez aussi quelques propriétés via le fichier dechter.q
-
Complétez le début de modélisation fourni dans l'archive
pour obtenir un modèle du comportement de John et Fred
de "tous les jours".
- Ajoutez les contraintes temporelles du jour spécifique. Vous avez le droit d'ajouter de nouvelles horloges. Vous procèderez contrainte par contrainte et vous vous assurerez par simulation que le résultat obtenu correspond bien à ce que vous attendiez
-
Est-il possible que John et Fred arrivent à leur travail respectifs en respectant les contraintes temporelles ? Pour répondre à cette question, vous vérifierez la formule suivante permettant de s'assurer que john et Fred peuvent arriver à l'heure ( E<> John.travail_IT and Frederic.travail_IT )
- Est-il possible que John et Fred respectent ces contraintes temporelles avec John prenant le bus et Frédéric utilisant le covoiturage ? En vous inspirant de la question précédente, vous "instrumenterez" les codes de John et de Fred pour mémoriser le moyen de transport employé et vous "affinerez" la formule
précédente pour qu'elle prenne en compte les moyens de transports utilisés
- En vous inspirant de cette première modélisation, proposez une nouvelle modélisation n'utilisant aucune horloge globale (uniquement des horloges locales). Pour ce faire, en reprenant le principe de la modélisation retenu en RDP, vous définirez deux nouveaux composants permettant
respectivement de modéliser une horloge associée aux
données temporelles absolues et une horloge associée aux données relatives du problème.
Question annexe : ne serait-il pas possible de se passer du composant décrivant l'horloge globale ?
4 Modélisation d'une machine à café
On se propose de modéliser le fonctionnement d'une machine à café, garantie conforme à la norme AFNOR MC007, qui indique la nécessité pour les machines à café à usage privé de se mettre en veille en cas de réservoir vide. La machine peut délivrer du café ou du thé suivant le type de capsule et de tasse insérées dans les logements prévus à cet effet. Un bouton poussoir permet de sélectionner thé ou café et déclenche le fonctionnement approprié de la machine en même temps. La délivrance d'un café prend 20 secondes et réclame 10cl d'eau, et celle d'un thé prend 40 secondes et réclame 20cl d'eau, quantités qui prennent en compte l'évaporation causée par le chaufage. Un réservoir de 2 litres permet d'alimenter manuellement la machine en eau. La machine ne peut être utilisée par 2 personnes en même temps, le bouton poussoir étant inhibé pendant tout le temps de service d'un utilisateur. La machine se met d'elle même en veille si elle reste inutilisée plus de 5 minutes, auquel cas elle a besoin d'un temps de chauffe de 90s avant de pouvoir fonctionner à nouveau. Ce préchauffage est déclenché lorsque le nouvel utilisateur presse le bouton poussoir, et occasionne une perte d'eau par évaporation de 5 cl. Le fonctionnement de la machine est matérialisé par un voyant lumineux qui change de couleur suivant qu'elle est : en veille, en manque d'eau, prète à fonctionner, ou en service.
- Modéliser cette machine sous forme d'automates communiquants
- Vérifier la conformité de la machine à la norme AFNOR MC007
";
?>