transformateur de courant moyenne tension
Cette me´thodologie de preuve a` e´te´ utilise´e pour la ve´rification de la spe´cification d’un transformateur de courant moyenne tension du re´seau EdF. Ce poste a pour but d’abaisser la tension du courant en vue de sa distribution dans les centres urbains. Durantl’exploitationd’unposte, plusieurstypesde de´fauts peuvent apparaˆıtre(de´faut dephase (PH), homopolaire(H), ou wattme´trique (W)). Pour prote´ger le mate´riel et l’environnement, plusieurs disjoncteurs ont e´te´ place´s sur diffe´rentespartiesduposte.Lorsdel’apparitiond’unde´faut, des capteurs alertent les diffe´rents disjoncteurs, controˆle´s par des controˆleurslocauxappele´s cellules(celluleliaison,cellule arrive´e et cellule de´part.
A. Descriptionformelled’unecellulede´part. Cettecellule a deux activite´s: la phase de confirmation du de´faut, suivie de la phase de traitement du de´faut. La phase de confirmation a pour but de faire disparaˆıtre les de´fauts fugitifs. Pour chacun des types de de´fauts un de´lai est de´clenche´, permettant de tester si ce de´faut est permanent ou non. Ils sont teste´s en se´quence, jusqu’a` ce qu’un d’entre eux soit confirme´ (i.e., pre´sent a` la fin du de´lai correspondant). De plus cette se´quence est interrompue de`s que le de´faut disparaˆıt, ou quand un des de´fauts pre´alablement examine´s apparaˆıt. La phase de traitement commence de`s que le de´faut a e´te´ confirme´. On alterne alors entre une ouverture du disjoncteur durant un de´lai variable et sa fermeture afin de ve´rifier si le de´faut n’a pas disparu. On ouvre le disjoncteur durant un de´lai donne´, on le referme alors. Si le de´faut est toujours pre´sent, on re´pe`te cette ope´ration pendant un certain nombre de cycles. Si le de´faut persiste a` la fin du dernier cycle, le disjoncteur est de´finitivement ouvert et son traitement est pris en charge par un intervenant exte´rieur. La spe´cification de cette cellule (et des deux autres) a e´te ´ re´alise´e en utilisant SIGNALGT [MRS95b].
B. Ve´rification de la cellule de´part. On rappelle brie`vementlebutdelaphasedeconfirmationspe´cifie´ en SIGNAL. Le processus confirmation est active´ lorsque le de´faut apparaˆıt (i.e., e´mission de l’e´ve´nement first_Defect). Le processus e´met l’e´ve´nement de sortie Def_Conf lorsque le de´faut est confirme´ et le signal boole´en Defect, donnant l’e´tat de cette cellule. Ce dernier est vrai quand un de´faut exte´rieur est de´tecte´ (re´ception de Ext_Defect), ouquandun de´fautae´te´ confirme´ (Def_Conf),autrement il est faux lorsque le de´faut n’est pas pre´sent. On veut donc analyser les proprie´te´s suivantes:
(1) La phase de confirmation et la phase de traitement ne sont jamais en cours aux meˆmes instants Cette proprie´te´ peut eˆtre e´tablie, en prouvant que l’ensemble des e´tats correspondant a` la situation ou` la phase de traitement et la phase de confirmation sont actives en meˆme temps, n’est pas accessible depuis les e´tats initiaux du syste`me dynamique polynomial. C’est ainsi, que l’on conside`re les deux intervalles I_Treat et I_PH, encode´s par des boole´ens qui sont vrais quand le syste`me est en phase de traitement, respectivement en phase de confirmation. Apre`s la traduction du programme SIGNAL en syste`me dynamique polynomial, on calcule l’ensemble des e´tats conf_and_treat , ou` I_Treat=1 et I_PH=1. La me´thode consiste alors a` ve´rifier que l’ensemble des e´tats conf_and_treat n’est pas accessible depuis les e´tats initiaux du syste`me. L’accessibilite´ de cet ensemble d’e´tats peut eˆtre ve´rifie´e en utilisant la fonction reachable(prop) qui rend vrai si les e´tats ve´rifiant la proprie´te´ sont accessibles depuis les e´tats initiaux et faux sinon. Dans notre cas le re´sultat est faux.
(2) Quand un de´faut apparaˆıt, on aura ne´cessairement:
(a) La confirmation du de´faut,
(b) ou la disparitiondu de´faut,
(c) ou l’apparitiond’un de´faut exte´rieur.
ces trois possibilite´s ont e´te´ spe´cifie´es en SIGNAL par un unique boole´en DEFECT qui est pre´sent quand l’une des trois possibilite´s est pre´sente 2 . Cette proprie´te´ peut eˆtre prouve´e en ve´rifiant l’attractivite´ de l’ensemble des e´tatsF, ou` DEFECT est pre´sent, a` partir de l’ensembleE, le de´faut apparaˆıt (i.e., il y a une occurrence de l’e´ve´nement First_Defect). En appliquant la fonction attractivity, de´crite par la de´finition 4, on peut prouver queFest attractif vis a` vis deE(i.e., chaque fois qu’un de´faut apparaˆıt, toutes les trajectoires du syste`me ame`nent dans des e´tats ou` DEFECT est pre´sent.
transformateur de courant moyenne tension