Paper
Contents
1. Mod lisation Mod le du fonctionnement nominal Le fonctionnement nominal du syst me des deux r servoirs consiste en une succession de phases de conjonction et de disjonction suite des commandes d ouverture et de fermeture des lectrovannes Le fonctionnement des deux r servoirs est identique en termes d tats et de succession d tats En effet les deux r servoirs poss dent la m me loi de commande et les deux lectrovannes poss dent les m mes modes de d faillance Une fois le mod le du r servoir 1 et de sa commande tabli il suffit de le dupliquer en adaptant tout simplement les seuils de commande et les param tres de d faillances et de r paration ceux du r servoir 2 dV1 f t lt 0 J SO V12 Vimax VI lt Vimin dv1 g t gt 0 0 figure 2 Mod le du fonctionnement nominal du r servoir 1 La figure 2 illustre le mod le de fonctionnement nominal du r servoir 1 La place V1 dec repr sente la phase de disjonction le volume d cro t tandis que la place V1_cr repr sente la phase de conjonction pendant laquelle le volume croit La place EV1 OK mod lise le bon fonctionnement de l lectrovanne 1 Les transitions t11 et t12 repr sentent respectivement la commande de fermeture de l lectrovanne 1 quand le volume d passe Vimax et la commande d ouverture de la m me lectrovanne quand le volume devient inf rieur V1min Mod le de d faillance et de r paration de l lectrovanne 1 C2. crite pr c demment au cas d tude 1 Etats normaux Ce sont les places ray es dans le mod le du syst me complet 2 Etat cible On s int resse au d bordement du r servoir 1 L tat cible sera donc l tat partiel redout E_red1 place gris e dans le RdP 3 Raisonnement arri re partir de l tat cible Cette tape donne la liste des sc narios menant l tat partiel redout La seule transition en aval de la place E_red1 est la transition t13 Un jeton est alors produit dans la place V1_cr Cette derni re repr sentant un tat de fonctionnement normal le raisonnement arri re s arr te On obtient donc le sc nario qui repr sente l accessibilit de l tat partiel redout E_red1 partir du marquage de la place V1_cr qu on appelle tat conditionneur en tirant une fois la transition t13 4 Raisonnement avant partir de la place V1 cr Le but de cette tape est de mettre en vidence les bifurcations entre le fonctionnement normal et les sc narios redout s La place V1_cr repr sente un tat conditionneur partir duquel on pourrait voluer soit vers l tat redout en question marquage de E_red1 par le tir de la transition t13 soit vers d autres fonctionnements Cela se traduit par le conflit entre les trois transitions en aval de la place V1_cr t13 t11 ett14 Cette tape donne trois fonctionnements possibles selon que l une ou l autre des transitions est tir e 0 l
3. syst me Le principe de notre m thode est d enrichir progressivement le contexte dans lequel s est produit l v nement conduisant l tat redout en tudiant les conflits de comportements ayant un lien de causalit avec l occurrence de l v nement redout Partant d une connaissance tr s partielle des conditions d occurrence de cet v nement par exemple le d clenchement d une alarme suite au franchissement d un seuil de s curit on s int resse aux comportements qui permettent d viter le chemin critique et qui correspondent des bifurcations repr sent es par des conflits de transitions L tude des conditions de tirs de ces transitions de bifurcation nous informe de mani re plus compl te sur les conditions d occurrence de l v nement redout Pour garantir la non occurrence de l v nement redout et donc une bifurcation du chemin critique certaines conditions sont n cessaires par exemple la disponibilit d une ressource de reconfiguration ou la pr sence du syst me dans un tat de fonctionnement bien d termin La non satisfaction de ces conditions nous conduit in vitablement vers l tat redout On a enrichi par cons quent nos connaissances sur l v nement redout en faisant intervenir d autres conditions la non disponibilit d une ressource par exemple L tude des comportements qui sont en conflit avec ceux en conflit avec le comportement critique et qui favorisent par
4. de d faillances Elle est bas e sur une mod lisation hybride du syst me et une g n ration automatique d arbres de d faillances temporis es Cette approche impose une discr tisation syst matique du temps et des variables continues ce qui entra ne une explosion combinatoire des tats Notre approche est galement bas e sur un mod lisation hybride du syst me Le fait que cette mod lisation soit fond e sur les r seaux de Petri permet la mise en vidence des sc narios menant aux tats redout s sans discr tisation du temps Chaque sc nario est g n r sous la forme d un graphe orient En inversant les fl ches de ces graphes et en consid rant que les transitions sont de conjonctions on obtient des descriptions proches de celle des arbres de d faillances En effet chaque n ud est un tat partiel comme c est le cas dans l arbre de d faillances de la figure 10 Les transitions du graphe la fois jouent le r le des portes ET des arbres de d faillances et celui des rep res des changements d tats dans les arbres temporis s Conclusion La m thode que nous avons pr sent e est bas e sur mod lisation pr alable d un syst me m catronique sous la forme d un r seau de Petri et d un ensemble d quations diff rentielles Cette mod lisation hybride pr sente l avantage de s parer clairement les aspects discrets et continus Ceci nous permet une analyse logique fond e sur la logique Lin aire 6 de
5. def3 It 3 R sultats L tat redout ne sera atteint que par le franchissement de t13 Comme nous l avons d j dit cause des seuils associ s aux transitions t11 t14 et t13 la transition t13 n est franchie que si t11 et t14 ne sont pas sensibilis es Cela veut dire que les sc narios redout s seront compos s d une part de sc narios comprenant des transitions en conflit avec t11 et t14 et d autres part du sc nario de franchissement de t13 Ce dernier sc nario a t d fini par la premi re it ration de la m thode Le sc nario emp chant le tir de t11 est issu de la deuxi me it ration et les deux sc narios emp chants le tir de t14 sont issus de la troisi me it ration D taillons ce dernier point Lors du raisonnement avant partir des tats conditionneurs nous avons vu qu il y avait deux cas pour lesquels la transition t14 n tait pas franchie cause du conflit autour de la place EV3_OK Il s agit soit du franchissement de def3 l lectrovanne 3 est d finitivement hors d usage soit du franchissement de t24 vidange de secours du r servoir 2 impliquant un jeton dans V2 cr Ces deux cas tant exclusifs nous aurons donc deux sc narios redout s Ces deux sc narios comprendront galement le sc nario obtenu lors de la deuxi me it ration raisonnement avant qui franchit la transition def1 Ces sc narios d finissent des relations d ordre entre les franchissements des transitions et peuvent
6. donc tre repr sent s par les deux r seaux de Petri de la figure 8 Ces r seaux de Petri sont des graphes d v nements c est dire qu ils ne comportent aucun conflit La partie not e lt 2 sur la figure 8 des deux sc narios correspond au r sultat de la deuxi me it ration et la partie It 3 correspond aux deux cas trouv s lors de la troisi me it ration La place reliant def1 t13 exprime le fait que pour ne pas franchir t11 il faut franchir def1 avant t13 De m me la place reliant def3 t13 exprime le fait que t14 ne doit pas tre franchie Par contre aucune relation d ordre n existe entre le tir des transitions def1 et def3 pour le cas a et def 1 et t24 pour le cas b Un sc nario correspond donc un ensemble de s quences de tirs de transitions Par exemple le sc nario a correspond aux s quences def1 def3 t13 et def3 def1 t13 La sym trie du fonctionnement des deux r servoirs qui se traduit par une sym trie dans le mod le RdP permet d tendre les r sultats obtenus au r servoir 2 EV3_BO F EV3_OK e EV3_oc2 It 3 V2 cr E red It 1 Vicr EVI_OK It 2 EVI_OK EVI_OK It 2 EVI_OK p O Ra lt E a Premier sc nario redout b Deuxi me sc nario redout figure 8 Les deux sc narios redout s sous forme de 2 RdP Au13 ESREL 2002 European Conference Comparaison avec les arbres de d faillances La description du sc nario que nous venons de donner se
7. pr sente sous la forme d un arbre dont les n uds sont les v nements et les arcs les tats partiels La m thode la plus utilis e dans les tudes de S ret de Fonctionnement pour l identification des situations redout s est la m thode des arbres de d faillances Elle donne une repr sentation des causes de d faillances et de leurs combinaisons conduisant une situation redout e Nous allons dans cette section comparer l arbre que nous avons obtenu avec les arbres de d faillances en nous appuyant sur le syst me de r gulation du volume de deux r servoirs Arbre de d faillance classique Il ne fait intervenir que les tats d faillants ou en bon fonctionnement des composants n cessaires l occurrence d une situation redout e L arbre relatif au d bordement du r servoir 1 est pr sent sur la figure suivante figure 9 Arbre de d faillance du d bordement du r servoir 1 Il exprime le fait qu il est suffisant que les deux lectrovannes 1 et 3 soient d faillantes EV1_ HS et EV3_HS pour que le r servoir 1 d borde c est la situation redout e not e E_red1 En fait cet arbre est incorrect car l lectrovanne 3 peut ne pas tre disponible sans tre pour autant hors service Nous avons affaire un syst me dynamique Arbre de d faillances avec prise en compte des tats Avec une connaissance des tats de l lectrovanne 3 il est possible d utiliser la notion d arbres de d faillances et
8. rs alliant m canique hydraulique et lectronique ainsi qu un calculateur Ces syst mes sont hybrides la dynamique continue tant associ e la partie nerg tique et la dynamique discr te tant li e la commande num rique et l existence d v nements discrets d faillances d passement de seuils Ce papier s int resse la s curit des syst mes m catroniques Pour cela il est important de caract riser les sc narios redout s au plus t t dans la phase de conception La raret de ces sc narios redout s rend inefficaces les m thodes bas es seulement sur la simulation 1 Pour aider les concepteurs prendre en compte les contraintes de s curit les sc narios redout s doivent tre directement d duits d un mod le du syst me Une analyse qualitative et quantitative de ces sc narios est n cessaires pour choisir les architectures les plus s res Comme le syst me est hybride nous avons choisi une mod lisation associant r seau de Petri et quations diff rentielles 2 Le mod le r seau de Petri d crit le fonctionnement nominal les d faillances et les m canismes de reconfiguration Nous proposons une m thode bas e sur l analyse qualitative du mod le RdP permettant de d duire les sc narios redout s en particulier en d terminant la suite d actions et d tats conduisant l tat redout Une comparaison des r sultats obtenus avec les m thodes classiques de SdF arbres de d
9. Une m thode pour obtenir des sc narios critiques dans les syst mes m catroniques Sarhane KHALFAOUI et Edwige GUILHEM PSA Peugeot Citro n Direction des Syst mes d Information 18 rue des Fauvelles F 92256 La Garenne Colombes cedex Summary Hamid DEMMOU et Robert VALETTE LAAS CNRS 7 avenue du Colonel Roche F 31077 Toulouse cedex This paper deals with safety in design of mechatronic systems For this purpose it is important to characterize feared behaviors which are critical in the early design stage In order to help designers taking into account safety constraints the feared behaviors have to be directly derived from a system model A qualitative and quantitative analysis of these behaviors are necessary to select good architectures The qualitative analysis points out all the behaviors leading to states in which the motorist and the passengers safety is no longer guaranteed We are proposing a method based on a qualitative analysis of a Petri net model of the system It allows to derive feared scenarios by determining the sequences of actions and state changes leading to the feared state Finally we present a comparison between Fault trees and the results obtained by our approach Introduction La part croissante de l lectronique dans le secteur automobile bien qu ayant consid rablement am lior et diversifi les services rendus par le v hicule a complexifi la conception des syst mes m catroniques s
10. a figure suivante Il regroupe les mod les de fonctionnement nominal des deux r servoirs les mod les de d faillance et de r paration des lectrovannes 1 et 2 les mod les d utilisation de l lectrovanne de secours ainsi que les mod les d occurrence des v nements redout s d bordement des r servoirs 1 ou 2 On d clare qu il y a d bordement d un des deux r servoirs par exemple le r servoir 1 quand le volume dans ce dernier d passe V s V4 tant sup rieur Vimax et V4 Dans ce cas on tire la transition t13 et on marque la place E_red1 EV1_BO V1 gt Vis 3 EV3_HS EV3_oc1 EV3_oc2 t23 V2 gt Vis EV2_BO figure 5 Mod le RdP du cas d tude u13 ESREL 2002 European Conference M thode de recherche de sc narios critiques Principe de la m thode Le but de cette m thode est de mettre en vidence les suites d actions et d tats qui conduisent aux tats redout s et d analyser plus pr cis ment ce qui fait que le syst me quitte le fonctionnement normal pour aller vers l tat redout La m thode que nous proposons est bas e sur une analyse qualitative partir d un mod le R seau de Petri Ce mod le repr sente le fonctionnement nominal du syst me ainsi que son comportement en pr sence de d faillances Il s agit donc d extraire et de rendre explicite les sc narios redout s partir d un mod le agr geant un ensemble de connaissances sur le fonctionnement du
11. cons quent l occurrence de l v nement redout nous informe plus pr cis ment sur le contexte dans lequel a eu lieu l v nement redout C est pourquoi notre d marche se poursuit r cursivement selon le m me principe et pas pas en analysant chaque tat partiel intervenant dans un sc nario redout comme un tat redout et en se posant la question de savoir comment on peut y arriver Nous avons labor une m thode g n rale bas e sur 4 tapes qui a pour but de d terminer les conditions de marquages d un ensemble de places donn qu on appelle tat cible Cela consiste d terminer de mani re syst matique et formelle comment marquer et d marquer cet ensemble de places Cette m thode est compos e de 4 tapes 1 D termination des tats normaux qualitativement ou quantitativement 2 D termination des tats cibles tats partiels redout s ou tats tudier 3 Raisonnement arri re partir de l tat cible peut tre un tat redout ou n importe quel autre tat partiel du mod le RdP 4 Raisonnement avant partir des tats conditionneurs mettre en vidence les ramifications bifurcation entre fonctionnement normal et sc narios redout s La premi re tape consiste d terminer les places dont le marquage repr sente un tat de fonctionnement normal Ces places nominales seront utilis es comme crit re d arr t du raisonnement arri re Cette tape peut tre r alis e d
12. d croissant Calculateur Pompel hp Pompe2 figure 1 Cas d tude La loi de contr le du calculateur pour chaque r servoir est telle que lorsque le volume d passe la limite sup rieure de commande Vimax pendant la phase de conjonction alors le calculateur commande la fermeture de l lectrovanne Lorsque le volume devient inf rieur V limite inf rieure de commande durant la phase de disjonction alors le calculateur commande l lectrovanne de s ouvrir et on change par cons quent de phase de fonctionnement Ce syst me doit assurer l approvisionnement des utilisateurs tout en vitant le d bordement de l un des r servoirs Une troisi me lectrovanne de secours est pr vue pour cet effet Elle est partag e entre les deux r servoirs et assure leur vidange quand ils d bordent Elle ne peut tre utilis e que par un seul r servoir la fois Quand le volume dans l un des r servoirs d passe la limite sup rieure de s curit Vi alors le calculateur commande l ouverture de cette lectrovanne du c t du r servoir qui risque de d border et ce jusqu ce que le volume devient inf rieur Vinin Pour simplifier nous supposons que seules les lectrovannes peuvent subir des d faillances Les lectrovannes 1 et 2 pr vues pour l alimentation des r servoirs peuvent tre bloqu es en ouverture En cas de d faillance de l lectrovanne 3 de secours celle ci est mise hors service
13. e deux mani res soit en utilisant une connaissance a priori des tats de bon fonctionnement du Au13 ESREL 2002 European Conference syst me soit en effectuant une simulation de Monte Carlo du mod le sur une courte fen tre temporelle pour d terminer la probabilit de marquage des places du r seau Celles qui auront une probabilit de marquage non n gligeable seront assimil es des places normales La deuxi me tape d termine l tat cible tudier Cet tat cible peut tre soit un tat partiel redout soit un autre tat partiel ayant un lien de causalit direct ou indirect avec cet tat redout par exemple une place qui repr sente la disponibilit d une ressource pour assurer un fonctionnement d grad vitant l occurrence de l v nement redout La troisi me tape g n re l ensemble des chemins qui m nent vers l tat partiel redout On effectue un raisonnement sur le mod le RdP invers c est pour cette raison qu on l appelle tape de raisonnement arri re Dans ce r seau invers on prend comme marquage initial le seul tat redout et l on cherche de fa on exhaustive tous les sc narios 3 minimaux aucun franchissement de transition non n cessaire n est effectu e permettant de consommer le marquage initial et aboutissant un marquage final uniquement form de places associ es au fonctionnement normal Au cours de cette tape on est en g n ral amen enrichir le mar
14. e mod le est le suivant EV1_OK repi def1 EV1_BO figure 3 D faillance et r paration de l lectrovanne 1 Il repr sente le fait que l lectrovanne reste bloqu e en ouverture apr s le tir de def1 et qu elle peut reprendre un comportement normal apr s r paration tir de rep1 Mod le d utilisation de l lectrovanne de secours Cette lectrovanne peut tre utilis e de mani re identique par les deux r servoirs 1 et 2 Quand le volume dans le r servoir 1 d passe la limite sup rieure de s curit V1 et si l lectrovanne de secours est disponible la place EV3_ OK est marqu e alors t14 devient franchissable et on commence la proc dure de vidange du r servoir 1 via l lectrovanne 3 en marquant la place EV3_oc1 L lectrovanne n est pas disponible pour une autre utilisation que celle en cours place EV3_OK vide Cette phase dure le temps que met le volume pour atteindre le seuil bas Vimin Ensuite on lib re l lectrovanne 3 on marque de nouveau EV3_ OK et on recommence une phase de conjonction on remet un jeton dans la place V1_cr en tirant la transition t15 Vi_cr t14 V1 gt Vir VI lt Vimin figure 4 Utilisation de l lectrovanne de secours L lectrovanne peut subir une d faillance tir de la transition def3 Dans ce cas la place EV3 HS est marqu e et l lectrovanne est mise hors service Mod le de syst me complet Le mod le du syst me de r gulation est le RdP de l
15. e sc nario redout trouv dans l tape pr c dente partir du marquage de V1_cr tirer une fois la transition t13 pour marquer E_red1 le tir de t11 partir du marquage initial un jeton dans chacune des places V1_cr et EV1 OK conduisant au marquage des places V1_dec et EV1_OK Ce sc nario repr sente la fermeture de l lectrovanne EV1 quand elle mest pas bloqu e en ouverture et quand le volume dans le r servoir 1 d passe la limite de contr le sup rieure V gt Vmax le tir de la transition t14 partir du marquage de V1_cr et de EV3_OK Cela conduit au marquage de la place EV3_oc1 Ce sc nario correspond au d but de la proc dure de vidange de secours du r servoir 1 quand l lectrovanne 3 appel e EV3 est disponible Suite l application de notre m thode l tat partiel redout d bordement du r servoir 1 correspondant au marquage de la place E red1 on obtient les r sultats suivants L occurrence de l v nement redout tir de t13 et ou marquage de E_red1 est provoqu par le non franchissement des transitions t11 et t14 qui sont en conflit structurel avec t13 Ceci nous am ne par cons quent l tude des conditions de sensibilisation de ces transitions savoir comment obtenir un marquage suffisant pour pouvoir franchir ces transitions comment sont marqu es les places EV1_ OK et EV3 OK en m me temps que la place V1_cr Nous prenons en compte lors de cette analyse des con
16. faillances est pr sent e la fin de l article Cas d tude Pr sentation Le cas d tude est bas sur un syst me de r gulation du volume de deux r servoirs cf figure 1 Il est constitu d un calculateur de deux pompes de trois lectrovannes tout ou rien de deux capteurs de volume et des deux r servoirs r gul s R servoir 1 R servoir 2 et d un troisi me r servoir de vidange Les deux r servoirs r gul s alimentent des utilisateurs selon un besoin pr d fini fonction du temps Le volume dans chaque r servoir 1 ou 2 doit rester dans un intervalle donn Vimin Vimax Le contr le s op re l aide du calculateur qui d cide selon la valeur du volume d livr e par le capteur d approvisionner ou non le u13 ESREL 2002 European Conference r servoir en question en en alimentant ou non l lectrovanne concern e Pour chaque r servoir on distingue donc deux phases de fonctionnement selon que l lectrovanne alimentant ce r servoir est ouverte ou ferm e Une phase de conjonction lorsque l lectrovanne est ouverte Le volume dans le r servoir est croissant durant cette phase et cela quelle que soit la valeur du d bit de sortie vers l utilisateur le d bit d alimentation de l lectrovanne est bien sup rieur par hypoth se au d bit de sortie Une phase de disjonction lorsque l lectrovanne est ferm e Le volume dans le r servoir est par cons quent
17. flits les valeurs des seuils des variables continues associ s aux transitions Par exemple pour pouvoir franchir t13 il faut qu il y ait au moins un jeton dans chacune des places Vi_cr et EV1 OK et aussi que la condition V12 gt Vima Soit v rifi e Afin de mieux analyser les conflits entre les transitions t13 t11 et t14 nous allons r it rer la m thode de recherche de sc narios pour analyser les conditions de tirs des transitions t11 et t14 Deuxi me it ration Commen ons tout d abord par l tude des conditions de franchissement de t11 cette transition est associ le seuil V12 gt Vima Cette condition est toujours vraie lorsque t13 est franchissable puisque le seuil de t13 est V12 gt Vis et on a Vis gt Vimax Donc si les places EV1 OK et V1_cr sont marqu es t11 sera toujours franchie avant t13 vitant ainsi le d bordement Il est donc n cessaire d analyser pr cis ment le ou les sc narios amenant ce marquage Pour que l approche soit exactement r cursive nous allons rajouter au mod le RdP du cas d tude une place virtuelle cf figure reliant par l interm diaire d une transition les places qui nous int ressent V1_cr et EV1_ OK Cette place appel Etat cible virtuel 1 repr sente un tat virtuel par rapport au syst me r el et n est autre qu un artifice pour pouvoir appliquer notre Au13 ESREL 2002 European Conference m thode partir de cet tat En effet chercher les sc nari
18. ieur Vmin 4 Raisonnement _ avant partir des tats conditionneurs On a trois tats conditionneurs V1_ dec V2 cr et EV3 OK Cela donne les ramifications suivantes e A partir de V2 cr soit le tir de t23 et le marquage de la place E_red2 d bordement du r servoir 2 soit le tir de t21 en supposant que la place EV2 OK est aussi marqu e et le marquage de V2 dec et de EV2 OK Ce sc nario correspond la fermeture de l lectrovanne 2 quand le volume dans le r servoir 2 d passe Vmax e A partir de V1 dec l unique volution est celle correspondant louverture de l lectrovanne 1 quand le volume franchit le seuil Vimin tir de t12 On retrouve la situation de conflit que nous sommes en train d tudier entre t11 t13 et t14 e A partir de EV3 OK un sc nario correspond au tir de la transition def3 d faillance de l lectrovanne 3 de secours Un autre sc nario possible en conflit avec le pr c dent est le tir de t12 et de t14 Le troisi me en conflit avec les deux pr c dents consiste tirer t24 La transition t14 est sensibilis e si les deux places V1_cr et EV3_OK sont marqu es Les possibilit s pour qu il n y ait pas de jetons dans la place EV3_OK sont soit le tir de def3 d faillance de l lectrovanne 3 soit le tir de t24 sans le tir de t25 vidange du r servoir 2 par l lectrovanne 3 Pour pouvoir tirer t24 il faut qu il ait un jeton dans chacune des places EV3 OK et V2 _cr
19. les outils associ s outil SOFIA de Sofreten 4 pour g n rer un arbre de d faillances ne se restreignant pas uniquement aux tats de bon ou mauvais fonctionnement Dans l exemple des deux r servoirs il existe alors un deuxi me sc nario qui m ne la situation redout e correspondant la d faillance de l lectrovanne 1 et l utilisation de l lectrovanne 3 pour vider le r servoir 2 cf figure 10 figure 10 Arbre de d faillance avec prise en compte des tats de l lectrovanne 3 Au13 ESREL 2002 European Conference Discussion L arbre de d faillances de la figure 10 ne fait r f rence qu des tats de composants et n explicite pas les changements d tats On trouve ainsi les deux situations critiques lectrovannes 1 et 3 hors service ou lectrovanne 1 et 2 hors service et lectrovanne 3 occup e vidanger le r servoir 2 sans pour autant savoir quelle est la suite de changements d tats qui m ne d un tat de bon fonctionnement l une des deux situations redout es En cons quence les sc narios qui m nent ces situations redout s ne peuvent pas tre d duits de cet arbre et comme le syst me est dynamique la connaissance des probabilit s des tats partiels de chaque composant ne suffit pas pour d duire la probabilit des situations redout s La m thode des graphes de flux dynamiques 5 a t introduite pour prendre en compte les volutions temporelles dans les arbres
20. os produisant un jeton dans cette place c est exactement rechercher les sc narios amenant la pr sence simultan e d un jeton dans V1_cr et d un jeton dans EV1_OK Vi_cr EV1_OK t_virt 1 Etat cible virtuel 1 figure 6 Etat cible 1 La m thode de recherche de sc narios donne les r sultats suivants 1 Etats normaux Ils sont repr sent s par le marquage des m mes places ray es l exception de EV1_ OK et de V1_cr En effet comme on se propose d tudier comment marquer ces places il faut les soustraire de la liste des tats normaux pour pousser le raisonnement arri re plus loin 2 Etat cible On s int resse au marquage de la place Etat cible virtuel 1 3 Raisonnement arri re partir de l tat cible Le premier pas de cette tape nous ram ne dans l tat correspondant au marquages des places V1_cr et EV1_OK Les transitions en aval de V1_cr sont t12 et t25 Le tir de t12 produit une jeton dans V1_ dec qui repr sente un tat normal Le tir de t15 sera analys lors de la troisi me it ration En aval de V1 dec les transitions rep1 et def1 sont franchies et cela nous ram ne de nouveau dans cette place On obtient le sc nario repr sentant la boucle d occurrence d une d faillance de l lectrovanne et de sa r paration tir des transitions def1 et rep1 L tat conditionneur est alors le marquage de la place EV1_OK 4 Raisonnement avant partir de l tat conditionneur On retrou
21. quage initial ajouter des jetons dans certaines places Cela se fera chaque fois que pour consommer un jeton dans une place non associ e un fonctionnement normal il faut franchir une transition non sensibilis e par un marquage accessible partir du marquage initial non enrichi Les jetons ajout s lors du processus d enrichissement du marquage correspondant des tats partiels qui sont des cons quences logiques des sc narios redout s et qui seront donc n cessairement observ s lors de l volution du syst me vers l tat redout En inversant les sc narios obtenus lors de cette tape nous aurons les suites d actions possibles menant d un tat normal l tat redout Cet tat normal est nomm tat conditionneur La derni re tape de la m thode consiste construire un raisonnement partir du mod le RdP initial en partant de chaque tat conditionneur d termin l tape pr c dente C est l tape de raisonnement avant Cela a pour objectif de localiser les bifurcations entre le comportement redout et le fonctionnement normal du syst me ainsi que les conditions de marquage de certaines places du r seau impliqu es dans ces bifurcations Afin de mieux comprendre cette m thode de recherche de sc narios nous allons la mettre en uvre en s appuyant sur le mod le du syst me de r gulation des r servoirs Application au cas d tude Premi re it ration Appliquons maintenant la m thode d
22. ret de fonctionnement des syst mes m catroniques du monde automobile Th se de Doctorat N 3076 Universit Paul Sabatier Toulouse 2 R Champagnat P Esteban P Pingaud R Valette Modeling and simulation of a hybrid system through Pr Tr PN DAE model ADPM 98 3 International Conference on Automation of Mixed Processes 19 20 March 1998 Reims France p 131 137 3 S Khalfaoui E Guilhem H Demmou N Rivieres Extraction de sc narios critiques partir dun mod le RdP l aide de la logique Lin aire MSR 2001 Mod lisation des syst mes r actifs 17 19 Octobre 2001 Toulouse France p 409 424 Au13 ESREL 2002 European Conference 4 Manuel d utilisation de l outil Sofia de la soci te Sofreten disponible partir de la page web http www sofreten fr Aide 20Simfia index htm 5 Chris J GARRET Sergio B Guarro George E APOSTOLAKIS The Dynamic Flowgraph Methodology for Assessing the Dependability of Embedded Software Systems IEEE Transactions On Systems Man and Cybernetics Vol 25 No 5 May 1995 6 J Y Girard Linear Logic Theoretical Computer Science 50 1987 p 1 102 7 B Pradin Ch zalviel R Valette L A K nzle Scenario duration characterization of t timed Petri nets using linear logic IEEE PNPM 99 8th International Workshop on Petri Nets and Performance Models Zaragoza Spain September 6 10 1999 p 208 217
23. s causalit s r sultant des changements d tats Gr ce cette analyse il est possible partir dun tat redout de remonter les cha nes de causalit et de mettre ainsi en vidence tous les sc narios possibles conduisant une situation critique Chaque sc nario est donn sous la forme d un ordre partiel entre les v nements n cessaires l apparition de l tat redout contrairement aux arbres de d faillances qui donnent un ensemble de combinaisons d tats partiels n cessaire la r alisation de la situation critique Il faut souligner le fait que l approche que nous avons d velopp e partir de la logique Lin aire 3 7 et n implique pas une num ration brutale et globale de tous les tats accessibles du syst me Au contraire elle permet de se focaliser sur le voisinage de l tat redout en faisant une num ration locale d tats partiels Autrement dit nous ne consid rons que les tats des composants directement impliqu s dans l apparition de l tat redout Le travail se poursuit par une meilleure formalisation des algorithmes de recherche des sc narios redout s en vue de leur automatisation A plus long terme nous envisageons de proposer une m thode d analyse quantitative utilisant ventuellement la simulation de Monte Carlo s appuyant sur la connaissance des sc narios redout s R f rences 1 Gilles Moncelet Application des r seaux de Petri l valuation de la s
24. ve le franchissement de defi ou ou exclusif celui de t11 Troisi me it ration Etudions maintenant les conditions de tir de t14 De m me que pour t11 le seuil associ est tel que si les places en amont de t14 sont marqu es elle sera franchie avant t13 et bloquera l volution redout On rajoute l tat cible virtuel de la figure 7 Vi_cr EV3_OK t virt 1 Etat cible virtuel 2 figure 7 Etat cible 2 La m thode de recherche de sc narios donne les r sultats suivants 1 Etats normaux places ray es du r seau l exception de EV3_OK et de V1_cr 2 Nouvel tat cible C est le marquage de la place Etat cible virtuel 2 3 Raisonnement arri re partir de l tat cible Le premier pas de cette tape nous ram ne dans l tat correspondant au marquage des places V1 cr et EV3_ OK A partir de V1_cr on franchit t12 et on marque V1_dec On peut marquer la place EV3_OK de deux fa ons diff rentes l issue des deux sc narios suivants Le tir de t15 puis de t14 dans le RdP invers et le marquage des places EV3_OK et V1_cr 0 Le tir de t25 suivi du tir de t24 et le marquage des places EV1 OK et V2 cr Le premier sc nario repr sente la vidange du r servoir 1 en utilisant l lectrovanne 3 avec succ s Le deuxi me sc nario illustre l utilisation de l lectrovanne 3 pour vider le r servoir 2 puis la lib ration de cette ressource la fin de la vidange quand le volume devient inf r
Download Pdf Manuals
Related Search
Paper paperless post paper source papercut paper paper.io 2 paper mart paper trading paperstream paperless paperport paper shredder paper towels paper cutter paper sizes paper airplane paper texture paper mache paper republic papercut login paperrater paperstream capture paper-pak paperwork paperless post login paperless employee