Auteur : Rodriguez Sébastien ------------------------- | Vérifications formelles | ------------------------- ------------ | Question 1 | ------------ Oui, le modèle prend en charge tous les composants du système. On obtient : Syst. Trans. | hno3_v11 |Syst. Synchro. |-----------Etats-------------:---------Transitions---------| Vanne1 |* 160:* 1296|hno3_v11 EchangeurThermique |initial 1:boucle 1264|hno3_v12 CapteurTemperature |dead 32:boucleinitial 1264| ControleurTemperature|deadlock 32: | AirComprime |pbModifTemp 0: | Vanne5 |pbBOOM 0: | EauPrincipale |pbPlusAir 16: | EauSecondaire |pbMoinsAir 8: | Pompe |pbFermerV1 32: | IndicateurTemperature|pbFermerV5 32: | ControleurPannePompe |pbOuvrirV1 32: | OperateurV1 |pbOuvrirV5 32: | OperateurV2 |pbActiverAP 32: | hno3_v11 |pbInhiberAP 32: | On remarque que dans le système de synchronisation, la transition "BOOM" peut toujours etre atteinte. D'après le systeme de transition, cette transition doit conduire à un état KO qui n'est pas défini. Je rajoute dans l'échangeur thermique : KO |- e -> KO; Cela permet d'obtenir : Syst. Trans. | hno3_v11 |Syst. Synchro. |-----------Etats-------------:---------Transitions---------| Vanne1 |* 160:* 1544|hno3_v11 EchangeurThermique |initial 1:boucle 1512|hno3_v12 CapteurTemperature |dead 0:boucleinitial 1264| ControleurTemperature|deadlock 0: | AirComprime |pbModifTemp 0: | Vanne5 |pbBOOM 0: | EauPrincipale |pbPlusAir 0: | EauSecondaire |pbMoinsAir 0: | Pompe |pbFermerV1 0: | IndicateurTemperature|pbFermerV5 0: | ControleurPannePompe |pbOuvrirV1 0: | OperateurV1 |pbOuvrirV5 0: | OperateurV2 |pbActiverAP 0: | hno3_v11 |pbInhiberAP 0: | fichier hno3_v11 : version(); //MEC 4 version alpha 3.4dts(hno3_v11); //Current St : hno3_v11 //--- States : // * : 160 //initial : 1 //dead : 0 //deadlock : 0 //pbModifTemp : 0 //pbBOOM : 0 //pbPlusAir : 0 //pbMoinsAir : 0 //pbFermerV1 : 0 //pbFermerV5 : 0 //pbOuvrirV1 : 0 //pbOuvrirV5 : 0 //pbActiverAP : 0 //pbInhiberAP : 0 //--- Transitions : // * : 1544 //boucle : 1512 //boucleinitial : 1264 //stoplog(); // ------------ | Question 2 | ------------ Le modèle hno3_v12 comporte un opérateur plus intelligent : désormais, la fermeture d'une vanne ne peut s'effectuer que lorsque la vanne est déja ouverte. De plus, le modèle hno3_v12 prend en charge la gestion des "BIP" et "NotBIP". Lorsqu'un BIP arrive à l'indicateur de température, l'opérateur doit ouvrir la vanne V5 pour refroidir l'échangeur thermique, et fermer la vanne V1 d'acide nitrique. Le fichier obtenu par le modèle hno3_v12, est le fichier "hno3_v12" suivant : version(); //MEC 4 version alpha 3.4dts(hno3_v12); //Current St : hno3_v12 //--- States : // * : 65 //initial : 1 //dead : 0 //deadlock : 0 //pbModifTemp : 0 //pbBOOM : 0 //pbPlusAir : 0 //pbMoinsAir : 0 //pbFermerV1 : 6 //pbFermerV5 : 2 //pbOuvrirV1 : 5 //pbOuvrirV5 : 15 //pbActiverAP : 4 //pbInhiberAP : 23 //--- Transitions : // * : 275 //boucle : 252 //traceBoucle : 1 //traceBOOM : 0 //boucleinitial : 230 //traceFermerV1 : 13 //traceFermerV5 : 9 //stoplog(); // ------------ | Question 3 | ------------ Le modèle hno3v21 semble valide car le modèle hno3v12 était valide. En effet, on a rajouté la gestion des pannes dans ce modèle. Il faut changer les propriétés incontrôlables des températures. En effet, elles peuvent désormais être controlées par les transitions tIs(...) du capteur de température. Dans ce modèle, la panne de l'arrivée principale d'eau est prise en charge. Cependant, le mauvais fonctionnement de l'arrivée secondaire n'est pas évoqué. Je rajoute donc dans le système de transitions de ES : transition_system EauSecondaire < width = 0 >; 0 |- e -> 0, eau -> 0, panne -> 1 ; 1 |- e -> 1, plusEau -> 1; < initial = { 0 } >. et dans le système de synchronisation, on rajoute la transition panne. De plus, il faut rajouter l'état Chaos atteint par la transition BOOM dans l'échangeur thermique : transition_system EchangeurThermique < width = 0 >; normal |- e -> normal, tIsStable -> normal, tDescend -> froid , tMonte -> chaud ; chaud |- e -> chaud, tIsChaude -> chaud, tDescend -> normal , tMonte -> chaud , tMonte -> danger ; danger |- e -> danger, tIsDanger -> danger, BOOM -> Chaos , tChute -> chaud , tDescend -> danger , tMonte -> danger ; froid |- e -> froid, tIsFroide -> froid, tDescend -> froid , tMonte -> normal ; Chaos |- e -> Chaos; < initial = { normal } >. En ce qui concerne la panne de la pompe, il faut aussi prendre en compte le fait que le contrôleur de pompe peut tomber en panne lui-aussi (cf sources). On est contraint de créer une panne dans le contrôleur de panne. De même, il faut gérer l'abscence de l'opérateur qui correspond à une panne, et la panne éventuelle de l'indicateur de température. On obtient le fichier résultat hno3_v21 : version(); //MEC 4 version alpha 3.4dts(hno3_v21); //Current St : hno3_v21 //--- States : // * : 17488 //initial : 1 //dead : 0 //deadlock : 0 //pbPlusAir : 0 //pbMoinsAir : 0 //pbPanneMP : 0 //pbPanneES : 0 //pbPanneOP : 0 //pbPanneTS : 0 //pbPanneTI : 0 //--- Transitions : // * : 131236 //boucle : 41524 //traceDead : 0 //boucleinitial : 230 //stoplog(); // ------------ | Question 4 | ------------ 1) Pour le modèle hno3_v11, l'évènement redouté ER est possible. En effet, la gestion des pannes n'est pas prise en compte. Ainsi, il est possible que la vanne V1 soit ouverte et que la vanne V5 soit fermée : si l'opérateur ne ferme pas la vanne V1, la quantité d'acide nitrique va faire augmenter la température à l'intérieur de l'échangeur thermique et provoquer une explosion. 2) En ce qui concerne le modèle hno3_v12, il intègre un opérateur plus "intelligent". Cependant, l'évènement redouté ER est possible si l'opérateur fait mal son travail. Comme en 1), la vanne V5 peut être fermée alors que V1 est ouverte. Si la température augmente, et dépasse la température requise, un BIP est émis. Si l'opérateur n'en prend pas compte, et ne ferme pas la vanne V1 en ouvrant la vanne V5, une explosion survient. 3) Dans le modèle hno3_v21, on suppose que seules les pannes sont incontrôlables. Ainsi, l'opérateur est supposé être "raisonnable" donc aucune fausse manoeuvre ne peut arriver. En conséquence, l'évènement redouté ER est inévitable (les pannes mettent le système dans un état puits où le système ne peut plus agir.)