Couaillier Nicolas Gentil Olivier Dess Génie Logiciel Janvier 1998 Spécifications et vérifications formelles ----------------------------------------- Question 1 ********** Oui, le modèle hno3_v11 parait valide. Lors de l'évaluation, on obtient 32 états dead et dead-lock et il y a des problèmes sur les évènements incontrolables.. En rajoutant la ligne KO |- e -> KO dans l'automate de l'échangeur thermique, on resoud le problème des évènements incontrolables, mais on retrouve 32 transitions de différence entre l'ensemble des transitions et la boucle. En traçant tous les transitions qui ne sont pas dans la boucle, on s'apperçoit qu'elles mènent dans l´état KO où il est logique de ne plus pouvoir boucler. Soit le résultat de la trace sur les transitions hors de la boucle : e(fermee.danger.0.TInfTc.automatique.ouverteAlimentee.0.0.0.TInfTc.0.0) |- (e.BOOM.e.e.e.e.e.e.e.e.e.e) -> e(fermee.KO.0.TInfTc.automatique.ouverteAlimentee.0.0.0.TInfTc.0.0) < property = ( traceboucle ) >, ; Question 2 ********** La différence entre la version hno3_v11 et hno3_v12 est la suivante : 1) L'automate de l'opérateur n'est plus naif et suit une procédure précise pour gérer le système. C'est à dire : - pour agir sur la vanne V5, il doit d'abord inhiber le controleur pneumatique. - pour agir sur la vanne V1, on considère que l'operateur a déja agit sur V5 et qu'en dernier recours, il ferme V1. 2) Dans la version 12, l'opérateur n'est autorisé à passer en mode manuel (inhiber AP) que lorsque l'indicateur de température émet le BIP. Ceci implique que l'ouverture manuelle de la vanne V5 est régie de la même façon par le BIP.(idem pour la fermeture manuelle de V1). En étudiant le résultat de la commande "wts(*, * - boucle)" qui tous les chemins qui partent de tous les états et qui arrivent dans des états n'appartenant pas a la boucle. Voici un exemple de résultat : e(ouverte.danger.0.TInfTc.automatique.fermeeAlimentee.0.0.0.TInfTc.0.1) |- (e.BOOM.e.e.e.e.e.e.e.e.e.e) -> e(ouverte.KO.0.TInfTc.automatique.fermeeAlimentee.0.0.0.TInfTc.0.1), Ici, l'échangeur thermique est dans l'état "danger" alors que l'indicateur de température est dans l'état "TInfTc", ce qui abérant. Question 3 ********** Les différentes versions ont des évènements incontrolables sur les transitions "tmonte", "tdescend" ... Or, ces évènements sont controlés dans la table de synchronisation. Etant donné qu'un changement de température peut être calculé en réalité, il parait normal de rendre l'évènement contrôlable. Dans les versions précédentes, le capteur de température n'était notifié que par des évènements "tIsXXXX". En fait, une suite d'évènements "tmonte" pouvait conduire à l'état KO sans que le capteur de température ne détecte un changement. Il faut maintenant ajouter des nouvelles synchronisations pour que le capteur de température soit prévenu de tout changement de température. Pour réaliser cela, nous avons modifié l'automate du capteur de température. Il garde en memoire la derniere modification de température, grace a deux états , et les transitions change et stable. Change indique un changement de température. Stable, a l'inverse indique, que la température est stable. De plus nous avons contraint le passage de l'échangeur thermique a l´etat KO, par la transition Ok de la vanne V1. On ne peut avoir BOOM, que si V1 est ouverte. Le modèle V21 est valide car le modèle précedent l´était et que l'ajout de la panne sur l'eau principale ne pose pas de problème de modelisation. Cependant 1) ajout d'une panne sur l'Eau Principale : le système reste valide : pbPanneMP = 0. 2) ajout d'une panne sur l'opérateur (absence) : le système reste valide : pbPanneOP = 0. 3) ajout d'une panne sur le détecteur de panne : le système reste valide : pbPanneFD = 0. 4) ajout d'une panne sur l'indicateur de température : le système reste valide : pbPanneTI = 0. 5) ajout d'une panne sur la pompe : - il faut ajouter en plus une ligne où la pompe et le controleur de pompe tombe en panne - si on rajoute la panne seule, on obtient des états dead et il y a un problème : pbPompeP <> 0. En traçant les états deads, on se rend compte que lorsque le controleur de pompe tombe en panne, il est impossible pour la pompe de tomber en panne . En fait, le problème vient du système de transition du détecteur : il faut rajouter dans l´état 1(état panne du détecteur), une transition "panne -> 1". On considère donc que la transition panne indique que l'élément tombe en panne où est en panne. Dans ce cas, le fait que le controleur de panne tombe en panne avant la pompe ne pose pas de problèmes. Question 4 ********** 1) modèle 11 : l'évènement redouté (ER)est impossible si l'opérateur fait bien son travail (c'est à dire s'il surveille régulièrement TI et qu'il agit en conséquence(ouverture de V5). 2) modèle 12 : l'ER est impossible si l'opérateur fait bien son travail(cf 1) 3) modèle 21_1 (hno3_21_1.*) : - (panne : EauPrincipale): l'ER est impossible si l'opérateur fait bien son travail(cf 1), la panne n'est pas primordiale dans le déclenchement du BOOM. 4) modèle 21_2 (hno3_21_2.*) : - (panne : EauPrincipale + Opérateur) : 5) modèle 21_3 (panne : EauPrincipale + Operateur + Controleur de panne de pompe) : 6) modèle 21_4 (panne : EauPrincipale + Operateur + Controleur de panne de pompe + Indicateur de température) : 7) modèle 21_5 (panne : EauPrincipale + Operateur + Controleur de panne de pompe + Indicateur de température + Pompe ) : Remarque : si nous avions modélisés les pannes sur V1 et V5 : V1 bloquée en position ouverte et V5 bloquée en position fermée, l'évènement redouté est inévitable.