Belloteau Patrice Renou Raphael RAPPORT du projet de MEC ========== Question 1 ========== La taille du systeme global semble normal. Le nombre d'etats initiaux est bon (un seul). Il semble logique que le systeme possede des etats "dead" puisqu'il existe un etat mort accessible par la transition "BOOM" de l'echangeur thermique. Nous avons verifie que pour tous les etats "dead", le composant "HE" est dans l'etat "KO", grace a la commande: wts(dead,*). Le nombre d'etats "deadlock" doit etre egal au nombre d'etats "dead", parce que il ne doit pas y avoir d'etats qui utilisent inevitablement la transistion "BOOM" ; Cela est verifie. Toutes les boucles passent bien par l'etat initial. Le probleme de la validation porte sur le calcul des incontrolables. //pbModifTemp : 0 //pbBOOM : 0 //pbPlusAir : 16 //pbMoinsAir : 8 //pbFermerV1 : 32 //pbFermerV5 : 32 //pbOuvrirV1 : 32 //pbOuvrirV5 : 32 //pbActiverAP : 32 //pbInhiberAP : 32 Le calcul de l'ensemble des etats a partir desquels l'evenement incontrolable est possible sur un composant (src_inconti[composant]) prend en compte tous les etats dont les etats qui seront "dead" pour le calcul sur le systeme global. Les evenements incontrolables de ce composant seront bloques par le composant "HE" dans l'etat "KO". En Effet l'etat "KO" est un etat sans transition qui signifie le blocage definitif du systeme. Donc si les etats manquants sont des etats "dead", il n'y a pas de probleme sur cet evenement incontrolable. Les nouveaux calculs sont : pbModifTemp := src_incont1[2] - src(incontrolable1[2]); pbBOOM := src_incont2[2] - src(incontrolable2[2]); pbPlusAir := (src_incont1[4] - src(incontrolable1[4])) - dead; pbMoinsAir := (src_incont2[4] - src(incontrolable2[4])) - dead; pbFermerV1 := (src_incont1[12] - src(incontrolable1[12])) - dead; pbFermerV5 := (src_incont2[12] - src(incontrolable2[12])) - dead; pbOuvrirV1 := (src_incont3[12] - src(incontrolable3[12])) - dead; pbOuvrirV5 := (src_incont4[12] - src(incontrolable4[12])) - dead; pbActiverAP := (src_incont5[12] - src(incontrolable5[12])) - dead; pbInhiberAP := (src_incont6[12] - src(incontrolable6[12])) - dead; Le calcul de pbModifTemp et pbBOOM n'est pas modifie, car ce sont des incontrolable du composant "HE" qui lui possede la transition "BOOM". Avec ces modifications on obtient : //pbModifTemp : 0 //pbBOOM : 0 //pbPlusAir : 0 //pbMoinsAir : 0 //pbFermerV1 : 0 //pbFermerV5 : 0 //pbOuvrirV1 : 0 //pbOuvrirV5 : 0 //pbActiverAP : 0 //pbInhiberAP : 0 Le modele hno3_v11 nous parait valide. ========== Question 2 ========== Le systeme hno3_v12 simule un operateur qui agit de maniere plus coherente que celui du systeme hno3_v11. L'operateur ne peut pas agir sur la vanne V5 sans inhiber AP. De plus, la reactivation de AP se fait avec une configuration donnee des vannes (V5 fermee, V1 ouverte). Enfin, l'operateur a une marche a suivre pour agir sur les vannes. Cela entraine plus de contraintes sur le systeme global. L'autre difference est une modification dans le systeme de synchronisation: a chaque fois que l'operateur agit, l'indicateur de temperature intervient. Et cela limite les possibilites d'action de l'operateur, etant donne qu'il ne peut "fermerV1", "ouvrirV5" et "iniberAP" que quand "TI" est dans l'etat "TSupSupTc". Ces differences ont des consequences sur la validation: - "fermerV1" n'est pas un incontrolable etant donne la ligne: (fermer .e .e .e .e .e .e .e .e .BIP .e .fermerV1) du systeme de synchronisation. En effet il ne peut y avoir une transition "BIP" dans le composant "TI", que si se composant se trouve dans l'etat "TSupSupTc" ce qui limite les etat du systeme dans lesquels "fermerV1" peu avoir lieu. De meme pour "ouvrirV1", "fermerV5", "ouvrirV5", "iniberAP", "activerAP". - Les "incontrolable1" de l'echangeur thermique ne sont plus incontrolables car la position des vannes influence le changement de temperature. ========== Question 3 ========== Le modele hno3_21 ne parait pas valide car les boucles ne passent pas toutes par l'etat initial. ========== Question 4 ========== Pour repondre a ces question, nous avons execute plusieurs calculs sur chacun des modeles: - tout d'abord: ER := tgt(incontrolable2[2]); ER est l'ensemble des etats du systeme global pour lesquels le composant "HE" est dans l'etat "KO". - ensuite: ERsrc := src(incontrolable2[2]); ERsrc est l'ensemble des etats du systeme global ayant une transition "BOOM" pour le composant "HE". - ERlock := inevitable(*,ER) - ER; ERlock est l'ensemble des etats du systeme global menant inevitablement a l'etat "KO" pour le composant "HE" (non-inclu les etat ou "HE" est deja dans l'etat "KO"). - OPOK := !state[2]="KO" /\ !state[10]="TEgalTc" est l'ensemble des etats ou "HE" est dans l'etat "KO" et "TI" affiche une temperature normale. - OPNOK := !state[2]="KO" /\ !state[5]="manuel" est l'ensemble des etats ou "HE" est dans l'etat "KO" et l'operateur a pris les choses en main. ##################### # modele hno3_v11 :# ##################### //OPOK : 8 //ER : 32 //ERsrc : 32 //ERlock : 0 //OPNOK : 8 a) ER n'est pas impossible car "ER" est non vide. b) C'est possible car: "OPOK" est non vide, c'est a dire, que meme si l'operateur fait correctement son boulot, etant donne qu'il ne connait pas la temperature reel de "HE", "ER" a quand meme lieu. c) TR := trace(initial, *, OPNOK); wts(src(TR),TR); transition_system hno3_v11 < width = 12; list = (Vanne1, EchangeurThermique, CapteurTemperature, ControleurTemperature, AirComprime, Vanne5, EauPrincipale, EauSecondaire, Pompe, IndicateurTemperature, ControleurPannePompe, OperateurV1 )>; e(ouverte.normal.0.TEgalTc.automatique.ouverteAlimentee.0.0.0.TEgalTc.0.0) |- (e.e.e.e.inhiber.e.e.e.e.e.e.inhiberAP) -> e(ouverte.normal.0.TEgalTc.manuel.ouverteAlimentee.0.0.0.TEgalTc.0.0) < property = ( boucle, TR, boucleinitial ) >, ; e(ouverte.normal.0.TEgalTc.manuel.ouverteAlimentee.0.0.0.TEgalTc.0.0) |- (e.e.e.e.isManuel.fermer.e.e.e.e.e.fermerV5) -> e(ouverte.normal.0.TEgalTc.manuel.fermeeAlimentee.0.0.0.TEgalTc.0.0) < property = ( boucle, TR, boucleinitial ) >, ; e(ouverte.normal.0.TEgalTc.manuel.fermeeAlimentee.0.0.0.TEgalTc.0.0) |- (OK.tMonte.e.e.e.KO.e.e.e.e.e.e) -> e(ouverte.chaud.0.TEgalTc.manuel.fermeeAlimentee.0.0.0.TEgalTc.0.0) < property = ( boucle, TR, boucleinitial ) >, ; e(ouverte.chaud.0.TEgalTc.manuel.fermeeAlimentee.0.0.0.TEgalTc.0.0) |- (OK.tMonte.e.e.e.KO.e.e.e.e.e.e) -> e(ouverte.danger.0.TEgalTc.manuel.fermeeAlimentee.0.0.0.TEgalTc.0.0) < property = ( boucle, TR, boucleinitial ) >, ; e(ouverte.danger.0.TEgalTc.manuel.fermeeAlimentee.0.0.0.TEgalTc.0.0) |- (e.BOOM.e.e.e.e.e.e.e.e.e.e) -> e(ouverte.KO.0.TEgalTc.manuel.fermeeAlimentee.0.0.0.TEgalTc.0.0) < property = ( TR ) >, ; d) "ERlock" etant vide, il n'y a pas d'etats qui menent inevitablement a ER. ##################### # modele hno3_v12 :# ##################### //OPOK : 2 //ER : 13 //ERsrc : 13 //ERlock : 0 //OPNOK : 7 a) ER n'est pas impossible car "ER" est non vide. b) possible, car aucune transition menant a ER est une transition ou l'operateur fait correctement son travail. c) TR := trace(initial, *, OPNOK); wts(src(TR),TR); transition_system hno3_v12 < width = 12; list = (Vanne1, EchangeurThermique, CapteurTemperature, ControleurTemperature, AirComprime, Vanne5, EauPrincipale, EauSecondaire, Pompe, IndicateurTemperature, ControleurPannePompe, OperateurV2 )>; e(ouverte.normal.0.TEgalTc.automatique.ouverteAlimentee.0.0.0.TEgalTc.0.0) |- (e.tDescend.e.e.e.OK.e.e.e.e.e.e) -> e(ouverte.froid.0.TEgalTc.automatique.ouverteAlimentee.0.0.0.TEgalTc.0.0) < property = ( boucle, TR, boucleinitial ) >; e(ouverte.froid.0.TEgalTc.automatique.ouverteAlimentee.0.0.0.TEgalTc.0.0) |- (e.tIsFroide.T6.tToInfTc.e.e.e.e.e.afficheInfTc.e.e) -> e(ouverte.froid.0.TInfTc.automatique.ouverteAlimentee.0.0.0.TInfTc.0.0) < property = ( boucle, TR, boucleinitial ) >, ; e(ouverte.froid.0.TInfTc.automatique.ouverteAlimentee.0.0.0.TInfTc.0.0) |- (e.e.e.MoinsAir.fermerV5.fermer.e.e.e.e.e.e) -> e(ouverte.froid.0.TInfTc.automatique.fermeeAlimentee.0.0.0.TInfTc.0.0) < property = ( boucle, TR, boucleinitial ) >, ; e(ouverte.froid.0.TInfTc.automatique.fermeeAlimentee.0.0.0.TInfTc.0.0) |- (OK.tMonte.e.e.e.KO.e.e.e.e.e.e) -> e(ouverte.normal.0.TInfTc.automatique.fermeeAlimentee.0.0.0.TInfTc.0.0) < property = ( boucle, TR, boucleinitial ) >; e(ouverte.normal.0.TInfTc.automatique.fermeeAlimentee.0.0.0.TInfTc.0.0) |- (OK.tMonte.e.e.e.KO.e.e.e.e.e.e) -> e(ouverte.chaud.0.TInfTc.automatique.fermeeAlimentee.0.0.0.TInfTc.0.0) < property = ( boucle, TR, boucleinitial ) >; e(ouverte.chaud.0.TInfTc.automatique.fermeeAlimentee.0.0.0.TInfTc.0.0) |- (OK.tMonte.e.e.e.KO.e.e.e.e.e.e) -> e(ouverte.danger.0.TInfTc.automatique.fermeeAlimentee.0.0.0.TInfTc.0.0) < property = ( boucle, TR, boucleinitial ) >; e(ouverte.danger.0.TInfTc.automatique.fermeeAlimentee.0.0.0.TInfTc.0.0) |- (e.tIsDanger.T6.tToDanger.e.e.e.e.e.afficheDanger.e.e) -> e(ouverte.danger.0.TSupSupTc.automatique.fermeeAlimentee.0.0.0.TSupSupTc.0.0) < property = ( boucle, TR, boucleinitial ) >, ; e(ouverte.danger.0.TSupSupTc.automatique.fermeeAlimentee.0.0.0.TSupSupTc.0.0) |- (e.e.e.e.inhiber.e.e.e.e.BIP.e.inhiberAP) -> e(ouverte.danger.0.TSupSupTc.manuel.fermeeAlimentee.0.0.0.TSupSupTc.0.1) < property = ( boucle, TR, boucleinitial ) >, ; e(ouverte.danger.0.TSupSupTc.manuel.fermeeAlimentee.0.0.0.TSupSupTc.0.1) |- (e.BOOM.e.e.e.e.e.e.e.e.e.e) -> e(ouverte.KO.0.TSupSupTc.manuel.fermeeAlimentee.0.0.0.TSupSupTc.0.1) < property = ( TR ) >, ; d) "ERlock" etant vide, il n'y a pas d'etats qui menent inevitablement a ER. ##################### # modele hno3_v21 :# ##################### //OPOK : 4 //ER : 26 //ERsrc : 26 //ERlock : 0 //OPNOK : 14 a) ER n'est pas impossible car "ER" est non vide. b) possible, car aucune transition menant a ER est une transition ou l'operateur fait correctement son travail. c) TR := trace(initial, *, OPNOK); wts(src(TR),TR); transition_system hno3_v21 < width = 12; list = (Vanne1, EchangeurThermique, CapteurTemperature, ControleurTemperature, AirComprime, Vanne5, EauPrincipale, EauSecondaire, Pompe, IndicateurTemperature, ControleurPannePompe, OperateurV2 )>; e(ouverte.normal.0.TEgalTc.automatique.ouverteAlimentee.0.0.0.TEgalTc.0.0) |- (e.tDescend.e.e.e.OK.e.e.e.e.e.e) -> e(ouverte.froid.0.TEgalTc.automatique.ouverteAlimentee.0.0.0.TEgalTc.0.0) < property = ( boucle, TR, boucleinitial ) >; e(ouverte.froid.0.TEgalTc.automatique.ouverteAlimentee.0.0.0.TEgalTc.0.0) |- (e.tIsFroide.T6.tToInfTc.e.e.e.e.e.afficheInfTc.e.e) -> e(ouverte.froid.0.TInfTc.automatique.ouverteAlimentee.0.0.0.TInfTc.0.0) < property = ( boucle, TR, boucleinitial ) >, ; e(ouverte.froid.0.TInfTc.automatique.ouverteAlimentee.0.0.0.TInfTc.0.0) |- (e.e.e.MoinsAir.fermerV5.fermer.e.e.e.e.e.e) -> e(ouverte.froid.0.TInfTc.automatique.fermeeAlimentee.0.0.0.TInfTc.0.0) < property = ( boucle, TR, boucleinitial ) >, ; e(ouverte.froid.0.TInfTc.automatique.fermeeAlimentee.0.0.0.TInfTc.0.0) |- (OK.tMonte.e.e.e.KO.e.e.e.e.e.e) -> e(ouverte.normal.0.TInfTc.automatique.fermeeAlimentee.0.0.0.TInfTc.0.0) < property = ( boucle, TR, boucleinitial ) >; e(ouverte.normal.0.TInfTc.automatique.fermeeAlimentee.0.0.0.TInfTc.0.0) |- (OK.tMonte.e.e.e.KO.e.e.e.e.e.e) -> e(ouverte.chaud.0.TInfTc.automatique.fermeeAlimentee.0.0.0.TInfTc.0.0) < property = ( boucle, TR, boucleinitial ) >; e(ouverte.chaud.0.TInfTc.automatique.fermeeAlimentee.0.0.0.TInfTc.0.0) |- (OK.tMonte.e.e.e.KO.e.e.e.e.e.e) -> e(ouverte.danger.0.TInfTc.automatique.fermeeAlimentee.0.0.0.TInfTc.0.0) < property = ( boucle, TR, boucleinitial ) >; e(ouverte.danger.0.TInfTc.automatique.fermeeAlimentee.0.0.0.TInfTc.0.0) |- (e.tIsDanger.T6.tToDanger.e.e.e.e.e.afficheDanger.e.e) -> e(ouverte.danger.0.TSupSupTc.automatique.fermeeAlimentee.0.0.0.TSupSupTc.0.0) < property = ( boucle, TR, boucleinitial ) >, ; e(ouverte.danger.0.TSupSupTc.automatique.fermeeAlimentee.0.0.0.TSupSupTc.0.0) |- (e.e.e.e.inhiber.e.e.e.e.BIP.e.inhiberAP) -> e(ouverte.danger.0.TSupSupTc.manuel.fermeeAlimentee.0.0.0.TSupSupTc.0.1) < property = ( boucle, TR, boucleinitial ) >, ; e(ouverte.danger.0.TSupSupTc.manuel.fermeeAlimentee.0.0.0.TSupSupTc.0.1) |- (e.BOOM.e.e.e.e.e.e.e.e.e.e) -> e(ouverte.KO.0.TSupSupTc.manuel.fermeeAlimentee.0.0.0.TSupSupTc.0.1) < property = ( TR ) >, ; d)"ERlock" etant vide, il n'y a pas d'etats qui menent inevitablement a ER. ===================================== question 5: mise au point d'un modele ===================================== La version de depart, que nous appelons hno3_v1 est exactement la version hno3_v12 qui nous a ete fournie. La version hno3_v2 est une version modifie de hno3_v1: - Nous avons modifie le systeme pour que toutes modification de temperature dans "HE" soit repercuter sur "TI" et "TC". Ainsi le probleme de la hausse de temperature non repercutee pouvant provoquer le passage en mode danger de "HE" sans reaction du systeme, est resolu.