Home

Allocation sûre dans les systèmes aéronautiques : Modélisation

1. 48 D marche pour la mod lisation ee deu 49 Solutions respectant les contraintes 52 Probl me des N Reines o cc a 2 4e s mm RR REG REO X E RUE OE ERS 53 Exemple de solution du probl me des V Reines 54 Contrainte de connexion 42 e Rm on ng og ds E s SOROR hn n 56 t eng relation reflexive LL as ol eh ew Ee Oe ewe ew eS 56 na Pent Pe WE o sieer e Rw EON GE 57 Illustration de la relation Set Allocation 58 xi 4 8 Exemple de probl me 4 59 4 9 Outil pour la recherche et la visualisation d allocations 62 4 10 Description du mod le GOM MON cosa t e ad Pe OAS est mob 63 4 11 Architecture pour le COM MON lt lt lt cad gos QUE a eee ES PEER a Oa 63 4 12 Allocation propos e par SatZoo 65 4 13 Ensemble des solutions optimales 66 4 14 Une allocation minimale propos e par l outil SatZoo 67 4 15 D marche propos dans ce chapitre 68 5 1 Mod le fonctionnel du COMMON 71 5 2 Nouveau comportement de Interrup 72 5 3 Les solutions n invalidant pas les exigences de s ret 76 5 4 Technique d obtention
2. ma spoiler2 dem AltBrake Y elevatorR NPdisty _Rudderb Flepsir Srorsir spoilers _clevatori aileronir noteng crrhya cBPhyd cEN ya YBrRyd YBNPhya ua FIG 7 13 Observateurs associ s aux situations redout es Nous utilisons la technique de g n ration des sc narios afin de v rifier les exigences associ es au syst me hydraulique Pour chaque observateur nous g n rons les s quences associ es et v rifions qu il n existe pas de s quences de taille plus petite que ce qui est stipul par l exigence de s ret de fonctionnement qui cor respond cette situation redout e Puis nous utilisons ARALIA pour effectuer le calcul de probabilit et v rifions que les probabilit s calcul es sont acceptables Pour cette premi re version du mod le hydraulique nous nous sommes rapidement rendu compte que le syst me ne respectait pas les exigences de s curit En effet il existe des pannes simples qui m nent la perte des lignes jaune et verte et des pannes doubles qui m nent la perte totale d hydraulique Un sc nario qui m ne la perte des lignes jaune et verte est AltBrake fail leakage rsvy update rsvy update PTU update rsvg update rvg update PTU update Ce sc nario ne comprend qu une seule d faillance celle du consommateur de la ligne jaune nomm AltBrake puis des v nements update qui repr sentent des reconfigurations du sy
3. les connexions entre ses composants l ind pendance entre les composants les diff rents choix possibles pour orienter des allocations Dans un premier temps ces informations vont permettre la valuation des constantes du syst me respectivement f cnz idpt coloc et set_ alloc Un exemple d informations extraire de l exemple du COM MON est donn par la figure suivante les informations extraire et permettant de construire le syst me de contraintes sont d crites dans le cadre gris bf cnx COM Equals 1 ff_cnx_Equals_Interrup 1 7 cnx S2 MOM 1 Y o 5 e ES rz w Re v l FIG 4 10 Description du mod le COM MON tant donn que les ressources de calcul poss dent les m mes caract ristiques nous pouvons consi d rer que toutes les fonctions du COM MON peuvent tre allou es sur l ensemble des ressources mises disposition L architecture mat rielle que nous allons utiliser est la m me que celle pr sent e dans le chapitre pr c dent savoir trois ressources de calcul Ry Sy et Sc et deux ressources de communi cation Bus et Bus gt FIG 4 11 Architecture pour le COM MON Les directives d allocation associ es l architecture voir section 4 4 apportent de nouvelles infor mations Pour rappel nous souhaitons que Les couples S1 COM S2 MON et Interrup Equals soient allou s sur une m me res
4. Il serait galement possible d acc l rer les analyses de l impact sur la s ret de fonctionnement des allocations de fonction sur les modules IMA et les r seaux partag s comme l ADCN Les techniques de g n ration automatique de l allocation devraient aider les concepteurs de sys t mes et les concepteurs de la plateforme avionique converger plus rapidement vers de solutions d architecture d allocation 8 3 2 Encore plus loin Les techniques de g n ration base de contraintes ont t appliqu es dans cette th se en se fo calisant sur le respect des exigences de s ret de fonctionnement Or d autres familles d exigences peuvent tre trait es de la m me fa on Dans le cadre du projet CARLIT des contraintes li es aux exigences de performance temps r el respect des ch ances des traitements de communications de compatibilit lectromagn tique taux de perturbation des messages mis sur le r seau ont galement t d velopp es Une perspective de notre travail serait le d veloppement d un outil d aide la conception de sys t mes avioniques qui permettrait de trouver les contraintes provenant des diff rents points de vue que l on peut associer sur un syst me Une derni re perspective concerne l allocation de syst mes dans un espace en trois dimensions d crivant un avion De nouveaux types d exigences peuvent tre identifi s pour aider au choix d une allocation spatiale
5. prenant une probabilit d clatement de pneu de 1079 les probabilit s de la perte de deux lignes et de trois lignes deviennent acceptables Ceci est possible sous l hypoth se que la qualit du pneu est fortement sup rieure la qualit des pneus classiques Cette approche a t consid r e pour autoriser le vol du Concorde apr s l accident de Gonesse Il est galement possible de revenir sur l allocation des composants AltaRica sur le mod le g om trique Comme nous l avons dit pr c demment nous avons choisi d tre pessimiste en consid rant que la perte d un tuyau entra ne la perte de tous les composants qui y sont reli s Il est possible de diminuer la cons quence des pertes des canalisations Par exemple nous avons consid r que l endommagement de la canalisation reliant le r servoir et la pompe jaune entra ne la perte de la pompe mais galement du r servoir et de l autre pompe On pourrait consid rer que seule la pompe aliment e par cette canalisation est perdue et que le r servoir et l autre pompe continuent fournir de la puissance hydraulique Dans ce cas l impact des trajectoires serait bien moindre que celui que nous avons calcul dans le tableau pr c dent En dernier recours il est possible d ajouter des blindages de fa on prot ger un quipement ou une canalisation contre des d bris de pneu ou de moteur Comme cette solution ajoute du poids l a ronef elle est consid r
6. 1 node Source 2 flow 3 bool ont 4 state 5 6 event 7 Fall Losas 8 trans 9 Se osea gt S false 10 assert 11 8 12 init 13 S true 14 edon 2 Les r servoirs Un r servoir est affect chaque ligne de distribution Le comportement sou hait pour ce composant est qu en pr sence d une fuite sur la ligne hydraulique qu il alimente le r servoir doit se vider progressivement Ces diff rentes tapes consid r es sont repr sent es par la figure 7 6 a O O O a Full b c Medium Empty FIG 7 6 Les diff rents tats d un r servoir Afin de mod liser correctement le vidage progressif du r servoir l v nement update est ajout Il permet en pr sence d une fuite dans le syst me qui est signal e par le fait que l entr e O rev est fausse de modifier en deux tapes la variable d tat du composant S passe de la valeur full medium puis empty pour visualiser l volution du contenu du r servoir Nous consid rons que le r servoir fournit du fluide la sortie 0 nom est vraie tant qu il n est pas vide la variable d tat S est diff rentede la valeur empty De plus tout moment une d faillance fail_Loss peut provoquer le vidage instantann du r servoir Le graphe repr sentant un tel comportement peut tre le suivant fail_Loss Fic 7 7 Automate du comportement d un r servoir Le code AltaRica correspondant a
7. Wd FlapsL spoiler 9 elevatorR Je NPdisty spoiler4 1 Flaps Pdistb 9 FlapsLR P StatsLR spoilers elevatorLR _sileroniR Fic 7 12 Mod lisation du syst me Hydraulique avec OCAS 111 CHAPITRE 7 SYSTEME HYDRAULIQUE D UN AVION DE TYPE A320 7 3 2 Validation du mod le Pour faciliter les analyses sur ce mod le nous ajoutons des composants suppl mentaires pour Vobservation des situations redout es Ces composant observateurs permettent lors de l volution du syst me d indiquer tout moment si oui ou non l tat du syst me correspond la situation redout e Dans notre cas nous souhaitons observer la perte totale de puissance hydraulique Pour exprimer ce comportement en AltaRica nous cr ons un composant poss dant autant d entr es qu il y a de lignes hydrauliques surveiller et la valeur de ses entr es est repr sent e par un bool en exprimant la pr sence ou non d alimentation Ce composant doit signaler la perte totale il poss de donc un flux de sortie exprimant par un bool en si oui ou non le syst me se trouve dans cette situation Le composant observateur n est pas sujet aux d faillances ne poss de donc pas de variable d tat ni d v nements Le code complet des observateurs est le suivant node Obs_Total_Loss al 2 flow 3 iil 2 log 8 mm 2 4 TARADO O 5 Le S WOOL g am 3 6 DIED O OO CNN asser
8. dom F et e Y si 8 Is oji o in1 est d fini alors 0 I s ARR 5 Vs dom S I dom F a s I o S En pratique une connexion peut tre assimil e 4 un renommage des variables d entr e par les variables de sortie La synchronisation d automates Les transitions dans les automates de mode sont asynchrones i e par d faut deux transitions ne peuvent tre d clench es simultan ment Seule l op ration de synchronisation BR94 permet de tirer plusieurs transitions simultan ment L ensemble des v nements synchronis s est ainsi regroup au sein d un m me vecteur de synchronisation Ce nouveau vecteur de synchronisation introduit donc des connexions synchrones entre les noeuds synchronis s et est d fini dans la rubrique sync du noeud p re 22 2 2 MODELISATION ET VERIFICATION DE LA SECURITE DES SYSTEMES AERONAUTIQUES Avant de voir la d finition formelle d un vecteur de synchronisation pour un automate de mode nous allons tout d abord rappeler la notion de composition de jeux de valuations Soit S C V ensemble fini de variables de automate V V et V des jeux de valuation des variables On dit que V et V sont incompatibles par rapport V si il existe une variable v S telle que V v V v et V v sont distinctes La composition des deux valuations V et Y par rapport V not e Y oy V est la valuation d finie par v si V v 4 V
9. lt Flux entrant par le port I1 Flux sortant par le port O2 lt Flux entrant par le port I2 Activation de I2 vers O1 A2 Fic 7 10 R le du PTU Le comportement souhait pour ce composant est d crit comme suit 109 CHAPITRE 7 SYSTEME HYDRAULIQUE D UN AVION DE TYPE A320 lorsque les deux lignes d livrent de la puissance hydraulique ou lorsqu aucune des deux lignes ne d livre de la puissance hydraulique alors le PTU ne doit pas tre activ Dans ce cas une fuite d un consommateur d une ligne n a pas d influence sur le niveau de fluide de l autre ligne Lorsque la ligne 2 ne d livre pas de puissance hydraulique et que la ligne 1 en d livre alors le PTU doit tre activ Dans ce cas la puissance hydraulique de la ligne 1 alimente les consommateurs de la ligne 2 Dans ce cas une fuite sur un consommateur de la ligne 2 influe sur le niveau de fluide de la ligne 1 Le comportement doit tre similaire lorsque la ligne 1 ne d livre pas de puissance hydraulique et que la ligne 2 en d livre Tant qu il n y a pas d activation le PTU ne doit transf rer aucune puissance hydraulique En pr sence d un dysfonctionnement le PTU ne fournit plus de puissance hydraulique d une ligne l autre mais la propagation d une ligne l autre de la baisse de niveau de fluide li e la fuite d un des consommateurs n est pas arr t e Pour mod liser ce comportement en
10. I rev I rev rev Fic 7 8 Automate du comportement d une pompe Le code AltaRica correspondant au comportement d une pompe peut s crire de la fagon suivante 1 node pump 2 flow 3 AS bolo 8 a B 4 D mon O OO TGS 5 reir 5 sim B 6 lol E sm 2 7 DOC E Gta E 8 state 9 SEE DO O 10 event 11 12 init 13 S true 14 trans 15 S true fail Loss gt S false 16 assert 17 O nom I nom and S and A 18 I rev O rev 19 edon 4 Les vannes de priorit ont pour objectif de couper la puissance hydraulique d livr e aux lignes de distribution non prioritaires Nous utilisons le m me noeud AltaRica que lors de la mod lisation d une pompe en consid rant que la vanne est ouverte lorsque le signal d activation A est vrai et qu elle est ferm e sinon 108 7 3 MODELISATION DE L ARCHITECTURE FONCTIONNELLE DU SYSTEME HYDRAULIQUE 5 Les consommateurs sont de deux types prioritaires et non prioritaires Les consommateurs prioritaires ont comme leurs noms l indiquent une priorit sur l alimentation par rapport aux non prioritaires Ils ont tous le m me comportement savoir consommer de la puissance hydrau lique subir une d faillance de type fuite v nement fail_leakage et dans ce cas envoyer une information de fuite sortie Ifev est vraie S false S true I rev S fail_
11. Sc nario de perte des lignes Jaune et Verte tape 2 La figure 7 16 montre l effet sur le r servoir de la ligne jaune de la fuite du consommateur AltBrake Apr s un second v nement rsvy update le r servoir est vide et les consommateurs de la ligne jaune ne sont plus aliment s en puissance hydraulique 114 7 3 MODELISATION DE L ARCHITECTURE FONCTIONNELLE DU SYSTEME HYDRAULIQUE engl le NPdistg ng B ESV DP d Eps jg PYg 4 e 2 E LandingGear 1e 1e 5 9 SlatsFlaps maa eng2 o gt E elecl FlapsL Y spoilerz o gt LJ PYy elevatorR Fic 7 16 Sc nario de perte des lignes Jaune et Verte tape La figure 7 17 montre l effet de la reconfiguration du PTU comme la ligne jaune n est plus aliment e alors que la ligne verte l est Apr s l v nement PTU update le PTU alimente la ligne jaune avec la puissance hydraulique provenant de la ligne verte et les consommateurs de la ligne jaune ne sont nouveau aliment s en puissance hydraulique engl _ rsvi DP k I H H C E 1e E E Al SlatsFlaps YamDampe naa ny4 FlapsE Pdistg _Ruddery Riiie stabilizery 2 spoiler T Stabiliz e gt rsvEDPy EDPy elevato Pdisty _spoilera_ NPdisty E E aileror spoiler m g 3 ll P Dye E Fic 7 17 Sc nario de perte des lignes Jaune et Vert
12. count 1 12 default i Count d 13 Suivant le degr N de s v rit associ la FC nous cherchons v rifier que tous les sc narios qui m nent la FC sont d un ordre sup rieur N Par exemple l exigence qui nous int resse est class e MAJ ce qui correspond au niveau 2 de s v rit Nous allons donc chercher v rifier qu il n existe que des combinaisons d au moins 2 d faillances l mentaires qui m nent la situation redout e consid r e Cela peut se traduire en logique Temporelle Lin aire de cette fa on F Sg X SR gt F failure count gt 2 o signifie que la propri t sera vraie dans un tat futur F pour finally failure failure failure failure failure failure time FC FC FCAXFC Pour v rifier si une telle formule est valide pour le mod le consid r nous utilisons le model checker SMV de Cadence Labs McM98 Ce model checker permet de prouver que le mod le de propagation satisfait bien cette formule Tant que la formule n est pas v rifi e le model checker fournit un contre exemple L analyse de ce contre exemple permet d extraire le sc nario et donc d identifier la s quence de d faillances qui invalide le mod le Par cons quent dans un premier temps nous v rifions la premi re partie de la formule pour faire appara tre un premier sc nario violant l exigence La premi re formule v rifier est donc AF SR XSR 73 CHAPITRE 5
13. les variables X X j i le num ro de ligne et j le num ro de colonne le domaine D 0 1 les contraintes TL 1 Une seule reine par ligne Vi 1 hk Ag 1 j 1 n 2 Une seule reine par colonne Vj 1 n 1 i l 3 Deux reines ne doivent pas se retrouver sur une m me diagonale Vi j k l 1 n Xij Xi lt 1 avec i kl j La r solution de ce CSP lorsque n vaut 8 c d dans le cas d un chiquier de 8 lignes donne 92 affectations possibles et diff rentes dont voici un exemple X11 X25 X38 X46 X53 X67 X72 X84 Cette solution est repr sent e par la figure 4 3 53 CHAPITRE 4 RESOLUTION DE CONTRAINTES D ALLOCATION Fic 4 3 Exemple de solution du probl me des W Reines 4 2 Les variables du probl me d allocation La mod lisation du probl me d allocation passe par une premi re tape d identification des diff rentes variables Les variables utilis es par la mod lisation sont les suivantes Les ensembles Afin de manipuler les diff rents composants nous les avons regroup s en deux ensembles Fonction F et Ressource R Les constantes Diff rentes relations peuvent s appliquer sur des fonctions f cnz correspond la relation de connexion entre les fonctions d finies dans la section 3 1 Pour rappel si f _cnx fi fo 1 alors f est connect fa coloc permet de pr ciser que deux fonctions doivent se r
14. 14 2 2 3 Pr sentation d taill e du langage choisi AltaRica Data Flow 19 2 2 4 Analyses et outils disponibles pour le langage AltaRica 24 II M thode propos e 29 3 Mod lisation et Analyse de l allocation 31 3 1 D finitions pr liminaires o os e scd ossee e du dE xm oho m OX E ER RE ho 32 3 2 Mod lisation de l architecture fonctionnelle 33 3 3 Mod lisation de l architecture mat rielle 38 3 3 1 Architecture mat rielle informatique 38 S202 Architecture Spatiale 22k ae d o GOR ee ek ee fe du 42 3 4 Mod lisation de l allocation 44 34 1 Application COMIMON o ke Pe 8 YR REOR de EO 46 DS Bl Li a A dm men UE de C 49 4 R solution de contraintes d allocation 51 4 1 Mod lisation et approche par contraintes 52 4 2 Les variables du probl me d allocation 54 4 3 Le domaine des variables utilis es 55 4 Los GODIFSIDIES s 4 5 3 sde m E ek w QUEG OE XR PUE EUR 55 4 5 Transformation du mod le CSP en syst me d quations lin aires 59 4 5 1 Des relations vers des variables bool ennes 59 4 5 2 Des variables bool ennes vers des in quations lin aires 60 4 6 R solution du syst me de contraintes 2 22 62 4
15. A D S Ft dom 5 0 I tel que eB mr eL PUS Bel 6 est obtenu en remontant les transitions 6 de chaque automate Aj au niveau de A Soit s dom S une valuation des variables d tat de Aj Soient i dom F une valuation des entr es de Aj Soient t dom S et e tel que t 6 S Ii e alors 51 5 Sry 11 in e 81 e Si 1 gt ti Si l 3 Sn Les assertions sont d finies de la m me mani re par 0 81 Sn 1 54n Ss 4 se On Sn tn I h In AltaRica est un langage hi rarchique Un noeud interm diaire est un noeud pouvant contenir d autres noeuds ces noeuds sont d finis dans la clause sub L organisation compl te d un syst me est orchestr e autour d un noeud principal appel Main le nom de ce noeud est une restriction impos e par l outil OCAS Finalement la mod lisation d un syst me complet est repr sent e par un unique noeud AltaRica Main compos de diff rents noeuds repr sentant les l ments du syst me 21 CHAPITRE 2 TECHNIQUES POUR LA MODELISATION ET LA VERIFICATION La connexion des interfaces d automates de mode synchronisme La connexion de composants i e d automates de modes consiste relier les composants par leurs interfaces pour leur permettre d changer des informations Elle consiste donc contraindre certaines variables d entr e d un composant tre gales une s
16. Alarm intemp Out true ClAlarmComp fail error C RadioAltimeter fail lost gt RadioAltimeter fail error Ces trois sc narios n apportent pas de nouveaux l ments l ensemble idpt puisqu il sont tous constitu s d une seule d faillance Par l analyse des diff rents sc narios menant des situations que nous souhaitons viter ou en s assurant qu il existe au moins deux d faillances mat rielles y menant nous avons construit l ensemble idpt identifiant l ensemble des fonctions placer sur des ressources mat rielles ind pendantes En effet en placant chaque fonction de chaque couple de d faillances constituant l ensemble idpt sur des ressources mat rielles nous garantissons que l allocation des fonctions sur les ressources n engendre pas de panne unique nous menant aux situations redout es 6 6 G n ration des contraintes d allocation Les hypoth ses d ind pendance consid rer pour notre SdT sont donc les suivantes idpt ClAlarmComp Navigation 1 idpt ClAlarmComp Radar 1 idpt ClAlarmComp TFTAPanel 1 idpt ClAlarmComp VerAccComp 1 idpt Navigation Roll1 idpt Navigation Rol12 il 2 15 idpt_Rolli_Roll2 1 Le syst me bas sur les contraintes d allocations est construit partir des hypoth ses d ind pendance et de l ensemble des contraintes d finies dans le chapitre 4 4 Chaque contrainte d finie doit tre appliqu e notre syst me pour obtenir le
17. Partant d une description des architectures fonctionnelles et mat rielles les mod les AltaRica de ces architectures sont r alis s L analyse du mod le fonctionnel fournit des r sultats dont on extrait les directives d ind pen dances Les directives s ajoutent aux contraintes d riv es de la description des architectures fonction nelles et mat rielles La r solution de ces contraintes produit une allocation des fonctions sur l architecture mat rielle 75 CHAPITRE 5 METHODE INTEGREE DE RECHERCHE D ALLOCATION Les solutions propos es par le solveur de contraintes pr servent les exigences de s ret Ces nouvelles contraintes permettent donc de r duire l espace des solutions possibles un espace de solutions respectant les exigences de s ret cf figure 5 3 Solutions respectant les exigences Sdf Solutions possibles Fic 5 3 Les solutions n invalidant pas les exigences de s ret La nouvelle allocation obtenue par r solution du syst me de contraintes peut tre ais ment ajou t e au mod le AltaRica pour effectuer de nouvelles analyses En effet comme vu dans le chapitre 3 la relation d allocation peut tre mod lis e en AltaRica par l ajout d un vecteur de synchro nisation Ce vecteur exprime une d faillance commune repr sentant la d faillance de tous les composants li s par la relation d allocation Ce nouveau mod le AltaRica est dit global car il
18. Dans l tat actuel de la r solution de notre syst me SatZoo nous propose une solution et donc une allocation possible pour notre syst me La repr sentation faite par SatZoo de la solution est la suivante MODEL alloc Navigation R1 alloc Rolli 1 R2 alloc CommandeVol R3 alloc Roll2 R3 alloc ClAlarmComp R3 alloc ConsRollComp R3 alloc Radar R3 alloc RadioAltimeter R3 alloc TFTAPanel R3 alloc VerAccComp R3 u cnx R1 R2 u cnx R1 R3 u cnx R2 R3 used R1 used R2 used R3 Le r sultat pr sent ci dessus peut tre interpr t comme suit les variables de la forme al1oc Fonction Ressource dont la valeur de v rit est vraie indiquent que Fonction est allou e la Ressource Par exemple les fonctions CommandeVol et Ro112 sont allou es la ressource R3 les variables used Ressource dont la valeur de v rit est vraie indiquent que la ressource est utilis e Dans le cas pr c dent les trois ressources sont utilis es les variables u_cnx_Ressourcei_Ressource2 dont la valeur de v rit est fausse elle sont pr c d es du signe indiquent que la connexion entre deux ressources n est pas utilis e Par exemple la variable u cnx R1 R2 signifie que la connexion entre les ressources R1 et R2 n est pas utilis e et par cons quent nous pouvons en d duire qu il n est pas n cessaire d avoir une liaison entre ces deux ressources les variables u_cnx_Ressource1_Ressource2 dont la v
19. L outil TINA BV06 quant lui manipule des r seaux de Petri sur lesquels il v rifie des propri t s exprim es par des formules LTL CTL et TCTL Yam95 UPPAAL PLOO est un langage de mod lisation mais aussi un outil permettant de v rifier sur des mod les de type automates temporis s des propri t s d invariants et d atteignabilit par l exploration de l espace d tat symbolique du syst me repr sent par des contraintes Bien entendu nous n envisageons pas de v rifier toutes les exigences par le biais du model checking En effet les exigences relatives au placement des quipements dans un avion comme Les quipements doivent tre distants d au moins L m tres ou Les quipements lectriques doivent se trouver au dessus des quipements hydrauliques seront v rifi es l aide de techniques propres aux outils de mod lisation g om trique 2 2 Mod lisation et v rification de la s curit des syst mes a ronau tiques Apr s avoir introduit dans la section pr c dente les concepts g n riques de la mod lisation et de la v rification des syst mes nous les instancions avec les techniques utiles dans le domaine de la s curit des syst mes embarqu s a ronautiques Nous commen ons par d finir le type d exigences que l on souhaite v rifier avant de d duire le type de mod les que l on doit manipuler Nous pr sentons dans ce cadre les types de mod les utilis s jusqu alors po
20. METHODE INTEGREE DE RECHERCHE D ALLOCATION Une fois que le premier sc nario contre exemple cex1 est identifi nous cherchons identifier de nouveaux sc narios invalidant eux aussi l exigence Pour cela nous ajoutons la formule pr c dente le sc nario identifi et obtenons ainsi une nouvelle formule a v rifier AF SR XSR V Si la formule n est pas v rifi e alors le model checker fournit 4 nouveau un sc nario contre exemple cex2 diff rent de cex De la m me mani re que pr c demment ce nouveau sc nario est utilis pour construire une nouvelle formule afin d identifier s ils existent de nouveaux sc narios contre exemples AF SR XSR V V cex2 Nous r it rons cette technique jusqu a obtenir la v rification de la formule AF Sr XSR V cex1 V V Ainsi de mani re r cursive nous utilisons la g n ration de contre exemples pour obtenir les dif f rents sc narios invalidant l exigence Donc lorsque l ensemble des contre exemples a t identifi la formule suivante est v rifi e F Sg XSR gt V Maintenant que nous avons identifi l ensemble des sc narios qui ne respectent pas l exigence nous allons extraire parmi ces sc narios les diff rentes fonctions rendre ind pendantes Le fait d imposer une ind pendance entre fonctions va nous permettre de garantir qu un sc nario compos de 2 fonctions ind pendantes est un sc nario
21. aires Nous avons jusque l d crit notre probl me d allocation par un ensemble de variables et des contraintes reliant ces variables entre elles Les diff rentes allocations acceptables sont repr sent es par les diff rentes combinaisons de valeurs des variables qui sont compatibles avec les contraintes L affectation des valeurs aux diff rentes variables est possible en faisant appel un outil de r solu tion de contraintes Une fois notre probl me mod lis sous la forme d un CSP l tape suivante consiste traduire les constituants du mod le en l ments de base formant notre syst me d quations lin aires Ce mod le a t transform moyennant l ajout de variables bool ennes appropri es en mod le de programmation lin aire bool en 4 5 1 Des relations vers des variables bool ennes Comme pr cis dans la section pr c dente l outil SATZOO ES03 GT04 qui permet de r soudre notre CSP prend comme variables d entr es des variables bool ennes Or comme pr sent dans la premi re section les variables utilis es pour la mod lisation sont des relations La transformation en variables bool ennes consiste lister toutes les variables lorsqu une relation est vraie La relation f cnx permettant d exprimer la connexion entre deux fonctions peut se transformer en un ensemble de variables bool ennes exprimant les diff rentes connexions Cette transformation permet aussi de construire l ensemble Vy
22. association de diff rentes fonctions sur une m me ressource Cette relation doit illustrer que lorsqu une d faillance survient sur une ressource alors toutes les fonctions allou es doivent aussi subir cette m me d faillance Nous pouvons ainsi observer la r action de notre syst me face la d faillance d une ressource permettant l ex cution du syst me Cette relation introduit une nouvelle notion la d faillance de cause commune ou de mode commun Lorsque plusieurs composants d pendent d l ments communs par exemple plusieurs com posants peuvent d pendre d une m me source lectrique et qu une d faillance intervient sur un de ces l ments tous les l ments communs vont subir cette m me d faillance Par exemple si nous prenons l exemple d l ments connect s une m me source lectrique une d faillance qui entra ne la perte de cette source est aussi une d faillance qui entra ne un dysfonctionnement des l ments connect s sous r serve de consid rer ces l ments comme des entit s ind pendantes lors de la mod lisation Nous utilisons la synchronisation d v nements pr sent e dans la section 2 2 3 afin de mod liser l allocation La synchronisation relie les d faillances de l architectures mat rielle avec les d faillances de l architecture fonctionnelle Cet op rateur du langage AltaRica ajoute un v nement suppl mentaire qui permet de simplifier l ex cution de tous les v nem
23. e des fonctions Fx1_fail_error Cet l ment regroupe donc l architecture fonctionnelle dans un m me composant un l ment de ce type est appel quipement Une repr sentation possible de la mod lisation souhait e est donn e par la figure suivante Ress_alloc_fail_error Mod le global Architecture _ __ Architecture fonctionnelle mat rielle Le code AltaRica du syst me ainsi que des composants est le suivant 1 node Main 2 event 3 Ress_alloc_fail_error 4 sub 5 alse 2 lat 6 Ress ress 7 sync 8 lt ess aT AMIE Cr or faES NEC TI OT 9 edon 1 node Archi_Fxl 2 event 3 Exile dL 4 sub 5 EXE 6 INdL 2 3 OMC 7 sync 8 sal il i doses o EN ESI steal TRO gt 9 lt il gt 10 SEINE gt 11 edon 1 node fonct 1 node ress 2 Peed 2 3 edon 3 edon En ce qui concerne les d faillances fail_lost la technique est exactement la m me 45 CHAPITRE 3 MOD LISATION ET ANALYSE DE L ALLOCATION 3 4 1 Application au COM MON Voyons pr sent comment v rifier une allocation propos e pour l architecture fonctionnelle de l exemple du COM MON fig 5 1 L allocation que nous allons v rifier suit les directives suivantes Comme les composants de la voie COM S et COM poss dent une forte d pendance ils s
24. espace en trois dimensions avec IRIS Air00 ou CATIA DAS85 la repr sentation des comportements possibles d un syst me l aide de formalismes d di s les automates contraintes utilis s par le langage AltaRica APGR0OO dans lesquels les contraintes r gissent le franchissement des transitions INous reviendrons de mani re plus d taill e sur les types de mod les correspondant nos besoins de mod lisation en section 2 2 2 10 2 1 INTRODUCTION A LA MODELISATION ET A LA VERIFICATION DE SYSTEMES les automates temporis s utilis s notamment par le langage UPPAAL PLOO les r seaux de Petri Pet81 permettant de mani re tr s simple de mod liser les interactions entre composants du type provider fournissant une donn e un service aupr s d un receiver en attente de cette fourniture pour son tour accomplir sa fonction Pour chacun de ces types de mod les des attributs sp cifiques sont d finis et caract risent le syst me mod liser pour les mod les AADL un ensemble de composants avec identificateurs attributs et services sp cifiques doivent tre identifi s ainsi que les relations existantes entre ces composants pour les mod les en trois dimensions chacun des composants du syst me mod liser doit tre repr sent en trois dimensions ainsi que chacune des connexions entre composants pour les automates contraintes il s agit de caract riser l
25. l aide d arbres de d faillance L arbre de d faillance est une repr sentation graphique de la formule logique exprimant la relation de causalit entre l occurrence de d faillances des composants d un syst me et la situation redout e Les analyses associ es aux arbres de d faillances permettent de v rifier la tenue des exigences qualitatives et quantitatives Les taux de d faillances des composants deviennent alors des exigences quantitatives garantir par les fournisseurs d quipements SSA Cette analyse consiste d montrer que l architecture mat rielle finale du syst me est bien en accord avec les objectifs fix s Il s agit de v rifier la coh rence entre les taux de d faillance atteindre et ceux pr sent s par les composants mat riels du syst me Contrairement une PSSA qui propose une m thode d valuation d une architecture relativement des exigences la SSA v rifie qu une architecture mise en place est conforme aux objectifs Les taux de d faillance prendre en compte pour la construction et l analyse des arbres de d faillances sont ceux fournis par les diff rents fournisseurs Les arbres sont mis jour avec ces nouveaux taux de d faillance et sont r valu s afin de quantifier les situations redout es d finies au niveau avion et de s assurer que les taux obtenus sont bien conformes ceux identifi s dans la FHA CCA L objectif de cette analyse est d identifier les d faillances dites de m
26. la contrainte sur les connexions peut s crire en logique de fa on suivante Vf f F Vr r R alloc f r alloc f r f enz f gt u_cnx r r 4 3 Les directives d allocations Elles concernent les choix pr d finis par le concepteur du syst me 1 Set allocation t doit tre allou e sur une ressource poss dant certaines caract ris tiques Suivant l importance de la fonction il est interdit de l allouer des ressources qui ne pos s deraient pas des caract ristiques suffisantes pour une ex cution id ale En effet certaines fonctions critiques comme le pilotage automatique n cessitent des ressources garantissant un certain niveau de s curit Il est indispensable lors de la conception de syst me de bien respecter les caract ristiques n cessaires aux fonctions pour un bon fonctionnement afin de garantir les performances et les exigences Afin de faciliter les diff rents choix offerts aux concepteurs la contrainte Set allocation permet de sp cifier les ressources n cessaires pour chaque fonction Elle permet ainsi de r duire les possibilit s d allocation et aussi de garantir quelques exigences comme la performance et la s curit Par exemple prenons une architecture fonctionnelle compos e de quatre fonctions fi fo fa fa connect es entre elles et pour permettre l allocation l architecture mat rielle propos e est compos e de trois ressources r1 ro r3 ayant des caract
27. pendamment des fonctions avec lesquelles elle interagit au sein de la chaine Chaque fonction est ainsi d crite par sa t che et par les types de donn es qu elle utilise La fonction connait ses types d entr e mais ne sait de quelles fonctions ou de quels capteurs ils proviennent Dans l tude de cas nous nous sommes tout particuli rement int ress s au mode fonctionnel auto matique du SdT SdT Automatique ce mode correspond un pilotage automatique de l avion les ordres de pilotage sont directement adress s aux commandes de vol CDVE Dans le mode Automatique le syst me SdT calcule en permanence des ordres de pilotage en profondeur qu il envoie directement aux commandes de vol permettant ainsi le contr le de l avion dans le plan vertical En parall le le syst me SdT surveille en permanence la coh rence et le bon fonctionnement des ressources et des t ches et produit en cas d anomalie une alarme de d gagement Cette alarme est suivie d une manoeuvre de d gagement qui permet de positionner rapidement l avion une altitude suffisante afin d viter le relief et permettre ainsi au pilote la reprise du contr le de l appareil Cette manoeuvre est bas e sur le calcul d un angle de tangage Pitch c f figure 6 2 suffisant afin d viter tout relief Avant que l alarme ne d clenche ce d gagement le syst me SdT calcule un angle de roulis appliquer afin de stabiliser l avion l horizontale c f angle Ro
28. s peuvent uti CTL liser les expressions suivantes pour exprimer une propri t sur les tats successifs d un syst me imm diatement apr s un jour toujours jusqu Y A CTL Computational Tree Logic EH82 permet de consid rer plusieurs volutions possibles partir d un tat donn du syst me plus t t que d avoir une vue lin aire du syst me consid r Ainsi depuis un tat du syst me on peut exprimer une propri t du type le syst me ne doit jamais par quelque volution du comportement du syst me possible tre dans un tat de panne non signal ucalcul le 86 est la logique pr sentant le plus grand pouvoir d expressivit En effet elle dispose des op rateurs v plus grand point fixe et u plus petit point fixe La notion de point fixe s applique des ensembles d tats Par exemple on utilise le plus petit point fixe pour calculer un ensemble d tats accessibles depuis un tat donn Le point fixe est atteint lorsque depuis le dernier ensemble d tats calcul aucun nouvel tat n est accessible Le plus grand point fixe peut tre utilis pour identifier un ensemble d tats ne menant pas un tat bloquant Les op rateurs de point fixe peuvent tre utilis s afin d exprimer les op rateurs Toujours un jour etc des logiques CTL et LTL L expression de la propri t P portant sur un tat du mod le doit quant elle tre bas e uniquemen
29. tous les v nements de cette s quence repr sentent la d faillance d une fonction fx Ci fx fail fx2 fail fp fail L allocation des fonctions fx1 fag sur les ressources R introduit des d faillances de mode commun vu dans la section 1 2 Cela revient remplacer la d faillance de la fonction fx par la d faillance de la ressource laquelle elle est allou e not e alloc fx Nous obtenons ainsi une nouvelle s quence minimale C incluant uniquement des d faillances des ressources de l architecture mat rielle C alloc f x1 fail alloc f 3 fail alloc fxg fail S il existe des fonctions qui sont allou es sur une m me ressource alors la d faillance de cette ressource va tre repr sent e qu une seule fois dans le sc nario C Dans ce cas la taille de C devient strictement inf rieure celle de C ce qui peut entra ner l invalidation de l exigence associ e FC Suivant la classification de FC le nombre minimal d v nements N composant les sc narios accep tables est donn dans par la table suivante FC CAT HAZ MAJ MIN S v rit N 3 2 1 Ainsi l aide de cette classification nous pouvons examiner l effet de l allocation sur chaque sc nario minimal de k v nements C fx fail fxo fail fxr fail e k lt N Ce sc nario est inadmissible car il ne respecte pas l objectif de safety e k N Ce sc nario est admissible mais
30. utilisation du langage AltaRica r side dans la possibilit d enrichir la description des diff rents composants pour se rapprocher du comportement attendu des fonctions sur une architecture mat rielle Voyons maintenant comment appliquer ces r gles pour mod liser l exemple du COM MON Comme pr sent dans la figure 3 2 ce syst me est compos de quatre composants Parmi ces quatre composants deux sont identiques du point de vue de leur comportement car ils effectuent tout deux une t che de calcul identique partir de leur entr e Ce composant de calcul poss de donc une entr e et une sortie pour faire transiter une donn e apr s un calcul sur cette derni re Comme pour la plupart des fonctions de calcul nous souhaitons lui associer un certain comportement face aux d faillances Ce comportement peut tre sch matis par l automate suivant correct fail_lost fail_error 7 fail_lost FIG 3 3 Comportements possibles des fonctions Cet automate d crit le comportement des fonctions en pr sence de d faillances L apparition d une d faillance fail_error ou fail_lost am ne un changement d tat de la fonction impact e En effet la fonction impact e n est plus dans son tat nominal qui correspond son bon fonctionnement mais dans un tat d crivant le dysfonctionnement Ainsi les deux autres tats de cet automate d crivent les deux tats de dysfonctionnement 1 L tat error repr sente un dy
31. 0 12 4 8 e 8 0 182 3 6 e 7 GBNPhyd 0 40 1 8 e 7 0 226 5 8 e 7 T 4 4 2 d44 4 4 Phyd 0 0 5 1 1111 0 151 3 2 e 7 NPhyd 0 1 1 0 e 8 0 140 2 7 e 7 Afin de faciliter la comparaison le tableau pr c dent reprend dans les 3 premi res colonnes les r sultats obtenus avant l introduction des d faillances de mode commun les trois derni res colonnes donnent les nouveaux r sultats Les probabilit s ont t calcul es en gardant les m mes taux de d faillances que pr c demment pour les d faillances des composants Pour les d faillances de mode commun nous tenons compte du nombre de trajectoires repr sent es par une d faillance La probabilit d une d faillance de mode com mun est gale au rapport du nombre de trajectoires repr sent es par cette d faillance et du nombre total de trajectoires consid r es multipli par la probabilit d clatement d un pneu Dans le ta bleau pr c dent nous avons pris une probabilit d clatement de pneu gale 1074 Nous avons consi d r que 1024 trajectoires avaient t calcul es par IRIS en faisant varier theta de 15 15 avec un incr ment 0 de 2 et en faisant varier kappa de 53 179 avec un incr ment Kine de 2 Par cons quent on obtient un taux de d faillance de 10 1024 x 107 soit 0 979 pour l v nement fail tyre burst W4 Theta minus15 9 Kappa 127
32. 135 qui regroupe 10 trajectoires Nous n observons pas de d gradation importante des r sultats aussi bien qualitatifs que quantita tifs pour les observateurs li s la perte d une seule ligne hydraulique En revanche en ce qui concerne la perte de deux lignes les r sultats ne sont pas acceptables En effet il existe dix v nements simples qui conduisent la perte des lignes jaune et verte cf les lignes du tableau pr c dent qui correspondent aux observateurs GYPhyd et GYNPhyd ce qui viole l exigence de stiret de fonctionnement indiquant qu une panne simple ne doit pas conduire la perte de deux lignes hydrauliques De plus les probabi lit s associ es sont sup rieures au taux de d faillance requis nous obtenons des probabilit s de l ordre de 3 8 x 107 alors que le taux requis est de 107 Observons un sc nario possible conduisant la perte des lignes jaunes et vertes Par exemple l v nement fail tyre burst W4 Theta minusi5 9 Kappa 127 135 d clenche les v ne ments Pdistg fail lost qui conduit la perte de la ligne verte prioritaire et rsvy fail lost qui conduit la perte de puissance sur la ligne hydraulique jaune On pourrait esp rer que le PTU puisse alimenter la ligne jaune partir de la ligne verte et permettre ainsi que la ligne jaune ne soit pas perdue Mais l v nement global pr c dent d clenche galement l v nement FlapsR fail leakage qui conduit au vidage progressif du r servoir vert et
33. 4 Cette figure illustre comment les diff rentes fonctions du syst me partagent le m me r seau de communication IMA Integrated Modular Architecture 86 6 3 MODELISATION DU SYSTEME Haut Parleur Base Donn e Terrain Navigation Altim tre FIG 6 4 Architecture mat rielle du Suivi de Terrain Calculateur 1 Commande L utilisation d une telle architecture permet le partage de certaines ressources par plusieurs appli cations et ainsi minimise le nombre de ressources n cessaire au bon fonctionnement de l avion Les int r ts d une telle architecture sont discut s dans BLED99 Les fonctions du syst me se partagent les diff rents calculateurs connect s ce r seau ce qui va engendrer de difficult s nouvelles lors de la conception de l architecture En effet il n est pas toujours ais de trouver les choix d allocation de fonc tions sur les calculateurs qui vont garantir le bon d roulement de la mission en cas de d faillance d un ou plusieurs calculateurs La technologie MA et le partage des ressources qu elle introduit engendrent de nouvelles d faillances de mode commun prendre en compte lors des analyses 6 3 Mod lisation du syst me 6 3 1 Mod le fonctionnel Le syst me SdT est compos de capteurs qui produisent un ensemble de donn es Ces donn es sont ensuite envoy es des fonctions afin de calculer un ordre n cessaire aux commandes de vol Ces
34. 6 1 Trop d allocations possibles 2 4 444 406 4 6 RR RR 65 ata ocho et 4 Oh ho ee Ree LP 67 vil 5 M thode int gr e de recherche d allocation 5 1 Identifier les hypoth ses d ind pendance 5 1 1 Identification par analyse de sc narios 5 1 2 Identification des hypoth ses d ind pendance par model checking 5 2 De l hypoth se d ind pendance vers la contrainte de s gr gation 5 3 Adaptation de l architecture mat rielle 54 Bian bbb Oe 5 en bons D EUR ee be ROAD be pop III Mise en application de la m thode propos e 6 Le Syst me de Suivi de Terrain SDT d un avion de chasse 6 1 Description du syst me de Suivi de Terrain 6 2 Description du syst me ec reas isis desa do dieu 6 2 1 Architecture fonctionnelle 6 2 2 Architecture mat rielle 6 3 du syst me one 6 oo E gens au ok a mire 6 3 1 Mod le fonctionnel gt aa cs esas trenar ae A os 6 3 2 Mod le d architecture mat rielle 4 4 4 4 4 44 4 4 u 4 4 4 4 4 4 RR 6 4 Exigences de s ret de fonctionnement du SDT 6 5 Identification des ind pendances 6 6 G n ration des contraintes d allocation
35. ADAPTATION DE L ARCHITECTURE MATERIELLE Construction Directives Description des Contraintes Architecture Division des ressources R solution du syst me Identification des ressources conflit Allocation possible Allocation Fic 5 6 D marche pour la recherche d allocation incr mentale Comme d crit pr c demment un conflit existe sur une ressource si au moins deux fonctions in d pendantes y sont allou es et par cons quent cette ressource viole syst matiquement l exigence sur l ind pendance de ces fonctions La premi re modification de l architecture mat rielle n cessaire pour pallier la violation de cette exigence consiste remplacer ladite ressource par un sous ensemble de ressources poss dant les m mes caract ristiques Cette technique appel e division permet de modifier simplement une architecture existante par l ajout de ressource Lorsqu une ressource est divis e nous consid rons que toutes ses connexions doivent tre report es sur les diff rentes ressources produites Une fois toutes les divisions n cessaires effectu es il suffit de relancer les analyses pour obtenir une allocation un exemple est propos dans la figure 5 7 gt fi et fo sont ind pendants Fic 5 7 Technique de division d une ressource en conflit 79 CHAPITRE 5 METHODE INTEGREE DE RECHERCHE D ALLOCATION 5 4 Bilan Dans ce chapitre nous proposons
36. ARALIA en consid rant que toutes les d faillances repr sent es par un v nement fail loss ont un taux de d faillance de 1074 par heure de vol et toutes les d faillances repr sent es par un v nement fail leakage ont un taux de d faillance de 107 par heure de vol Ces r sultats sont satisfaisants car aucune panne simple ne conduit la perte de deux ou trois lignes hydrauliques Aucune panne double ne m ne la perte totale d hydraulique prioritaire En revanche il existe une panne double qui conduit la perte totale de l hydraulique non prioritaire En effet lorsque les moteurs sont d faillants engi fail loss et eng2 fail loss alors les pompes moteurs EDPg et EDPy et les pompes lectriques EMPy et EMPb ne sont pas aliment es et par cons quent les lignes jaune et verte sont perdues Seule une pompe de la ligne bleue est aliment e par la Ram Air Turbine mais dans ce cas la valve de priorit PVb est ferm e et seuls les consommateurs prioritaires de la ligne bleue sont aliment s On peut supposer que ceci est acceptable puisque ces consommateurs sont consid r s comme non prioritaires Il faudrait donc consid rer que la perte des trois hydrauliques non prioritaires est class e Hazardous et donc il serait acceptable qu une panne double m ne cette situation S il n est pas possible de changer la s v rit de cette situation alors l analyse montre qu il est imp ratif de modifier la logique de coupure de la vanne de prio
37. AltaRica nous utilisons de nouvelles variables d tats P12 nom P12 rev P21 nom et P21 rev qui d terminent l activation du PTU P12 nom est la variable d tat correspondant l activation du transfert de puissance hydraulique de la ligne 1 vers la ligne 2 En cas d activation A1 true and A2 false cette variable est mise jour pour permettre le changement de mode P12 nom true si I1 nom true Cette mise jour est effectu e par l v nement update Le code AltaRica de la transition de ce comportement est donc trans S true update gt P12 nom not A2 and A1 and Ii nom De m me la variable P12 rev est la variable d tat correspondant l activation de la propa gation des fuites de la ligne 2 vers la ligne 1 En cas d activation A1 true and A2 false cette variable est mise jour pour permettre le changement de mode P12 rev true si 02 rev true sens normal nom lt sens inverse rev Fic 7 11 Comportement du PTU en cas d activation 1 Comme pr sent dans la figure 7 10 les valeurs des flux sortants du P TU sont fonctions de l activation effectu e et par cons quent ils sont fonctions des variables d tat de ce composant En appliquant ces choix pour chaque variable d tat et pour les deux sens de propagation le code AltaRica suivant formalise le comportement du P TU 1 node PTU 2 flow 3 icone 1 2 private 4 Tel boolean 5 JL 3L 39
38. Commen ons par rappeler la d finition d un automate de mode D finition 2 1 Rau02 Formellement un automate de D S F FO dom YE 0 0 1 avec D est un domaine fini mode M est un 9 uplet M Notons V l ensemble fini de variables partitionn en trois classes S et F Ces sous ensembles de V sont d nomm s respectivement variables d tat de flux d entr e et de flux de sortie dom V gt 2 telle que Vv V dom v 5 0 associe une variable son domaine Y est un ensemble fini d v nements 6 est une fonction partielle appel e transition dom S x dom F x E gt dom S dom S x dom F est la garde de la transition Cette fonction calcule la prochaine valuation des variables d tat consid r es en fonction des valeurs courantes des va riables d tat des variables de flux d entr e et de l occurrence de l v nement provo quant le changement d tat est une fonction totale appel e assertion dom S x gt dom F Elle calcule la valeur des variables de sorties en fonction des valeurs des variables d tat et de flux d entr e I dom S est une fonction partielle qui d crit les conditions initiales L automate de mode correspondant l exemple illustr par la figure 2 5 est le suivant _ pout D true false S Status dom Status F true false X fail_error true l fail error false o t
39. DE TERRAIN 4229125439999 OR du 6 2 DESCRIPTION DU SYSTEME coo sa 40 eese db ae da UU ROS WR re dent et 6 2 1 Architecture fonctionnelle 4 4 4 54 o sa asus REA 6 2 2 Architecture mat rielle 4 4 4 4 4 4 4 d dU 9 9 0 3 MOD LISATION DU SYSTEME 2 2 us a e Longe Be du A we vos 6 3 1 Mod le fonctionnel 2 0 4 556 o Rev y m x rene 3 3 ae 6 3 2 Mod le d architecture mat rielle 6 4 EXIGENCES DE SURETE DE FONCTIONNEMENT DU SDT 6 5 IDENTIFICATION DES INDEPENDANCES s e w ao Loan D 3 AT A da La 8 9o X 6 6 G N RATION DES CONTRAINTES D ALLOCATION 6 7 RECHERCHE ET VISUALISATION D ALLOCATION gt o a oo sa taaa eee 6 7 1 Recherche d une allocation 6 72 Visualisation de l allocati B iu nu uo ac a BE oem a RO mate DR BIDEN C d age ga Ba BED EAU ad E a 34 84 85 85 86 87 87 91 91 92 94 96 96 96 99 83 CHAPITRE 6 LE SYSTEME DE SUIVI DE TERRAIN SDT D UN AVION DE CHASSE A la diff rence de l exemple trait dans le chapitre pr c dent il ne s agit pas d un syst me de type informatique Malgr cela nous montrons que l approche de mod lisation et de v rification de Vallocation est applicable 6 1 Description du syst me de Suivi de Terrain Le principe
40. Flux de sens normal 0 nom lt Flux de sens inverse 0 inv Fic 7 4 Mod lisation des informations circulant dans le syst me en AltaRica Le code AltaRica permettant de mod liser ce type d information circulant entre les composants est le suivant 1 node compo 2 flow 3 pinom OL s 4 2 lol 2 sum 5 6 edon Lorsque les informations caract risant les connexions entre les composants sont identifi es et mod lis es il reste mod liser les diff rents composants eux m mes 1 Les sources d nergie les moteurs Engl Eng2 les alimentations lectriques Elecl Elec2 Ces sources permettent d alimenter en lectricit ou en puissance m canique les diff rents pompes du syst me hydraulique Leur r le consiste donc produire de l nergie dans ce cas la sortie O est vraie lorsque qu ils ne sont pas en pr sence d une d faillance et de ne rien produire dans le cas contraire la sortie est fausse dans ce cas Le comportement souhait en pr sence de la d faillance fail Loss est que l tat interne S du composant change emp chant ainsi la production d nergie Ce comportement peut tre repr sent par l automate suivant fail Loss Fic 7 5 Automate du comportement d un r servoir La transcription en AltaRica d un tel comportement peut s exprimer de la fagon suivante 106 7 3 MODELISATION DE L ARCHITECTURE FONCTIONNELLE DU SYSTEME HYDRAULIQUE
41. Item Requirements Safety Objectives Analyses Required Development of System Architecture System Architecture Allocation of Item Requirements Requirements to Items System Implementation Separation amp Verification Physical System Certification Safety Assessment Process System Development Process Fic 1 1 Cycle de d veloppement selon l ARP 4754 1 8 Limites du processus actuel Le processus actuel repose en grande partie sur la d finition et l analyse d arbres de d faillances La d finition des arbres de d faillances associ s un syst me est habituellement tablie par des experts de mani re manuelle La premi re tape de d finition des arbres de d faillances repr sente un travail tr s long En effet ce travail n cessite l analyse de tous les documents de description du syst me de type fonctionnel pour la FHA fonctionnel et architectural pour la PSSA et fonctionnel architectural et composants mat riels pour la SSA Un premier ensemble de limites associ es cette approche est a d finition de l arbre de d faillance est longue il n est pas ais de tenir compte des modifications apport es dans la d finition du syst me c est l ensemble de l arbre de d faillance qui doit tre examin pour d terminer ce qui doit tre modifi la repr sentation sous forme d arbre est assez loign e des diagrammes habituellement u
42. Jp 8 10 edon Fic 3 15 Les ressources de calcul simples Les composants AltaRica des 2 autres groupes G2 G3 sont mod lis s de la m me fagon ils ont un code semblable mis part leur nombre de connexions entrantes Pour tout composant ayant n connexions on construit le noeud AltaRica correspondant Pour cela il suffit d ajouter au composant g n rique les entr es et d exprimer la valeur de sortie en fonction de l tat interne de ress et des valeurs de ses entr es En effet le comportement du composant que nous souhaitons appliquer et qu en cas d une donn e erron e sur l une de ses entr es cette derni re doit tre propag e en sortie et nous supposons galement que ce composant doit obtenir une valeur de toutes ses entr es pour produire une donn e Vie 1 n I in correct error lost out correct error lost case r S correct and I1 erroneous or or In erroneous erroneous 41 CHAPITRE 3 MOD LISATION ET ANALYSE DE L ALLOCATION r S correct and Ii lost or or In lost lost r S correct and li correct and and In correct correct else r S 3 3 2 Architecture spatiale Il est aussi possible d appliquer notre principe de mod lisation et de v rification sur d autres types de syst mes Par exemple en ce qui concerne le probl me d allocation des diff rents quipements dans un avion il est possible de fair
43. Mapping Manager 01 mapATAZ4 ATA27 ATA29 i Left IR Maps Right OCAS List of Components x HYU ATAZ3 DT EUPg Left ATA24 branch1095 1 SL impacted HYD_ATA29 D1 EDPg2f ATA24 branch1096 15L GCU1 to 1DG1 impacted HYD_ATA29_D1 EDPy fa ATA24 branchl 102 25L GCU2 to IDG2 impacted HYD ATA29 D1 distb fail ATA24 branch1 103 25L GCU2 to IDG2 impacted ATA24 branchi 104 25L GCU2 te IDG2 impacted ATA24 branch1 105 25L GCU2 to IDG2 impacted ATA24 branch4 3G impacted ATA24 branch474 1G impacted ATA24 branch476 2G impacted ATA24 branch982 2P TRU APU to MPC impacte List of Components Right RUDDER_ATA27_D2 P2 ATA24 branch383 2P T RU APU te MPC impacte ATA24 branch384 2P TRU APU te MPC impacte ATA27 Rudder THS Control Cable impacted ATA27 Rudderbranch680 1SFC Rudder Servo Ct ATA27 Rudder IRUDDER ATA27 02 51 IRUDDER ATA27 02 5 branch687 1MFC Rudder Servo Ctl mapping operation buttons ATA27 Rudderbranch633 2MF9 Rudder Servo Ctl ATA27 Rudder branch 24 2MF9 Rudder Servo Ctl ATA27 Rudder branch726 2MF9 Rudder Servo Ctl ATA27 Rudder branch 37 25F9 Rudder Servo Ct ATA27 Rudder branch738 2SF Rudder Servo Ct B ATA27 Rudder branch739 2MF Rudder Servo Ctl E lOCAS RUDDER ATA27 D2 SVy fail ATA27 Rudderfbranch795 2MF Rudder Servo CtlE OCAS RUDDER _ATA27_D2P3 fail Ic ATA2S b hp d3 impacted T g
44. OCAS Elle est repr sent e par la figure suivante newSpeed Radar TerrainInFo Verdc Comp Cl larmComp ConsRollComp new Alt FIG 6 6 Mod le AltaRica du SdT Une des particularit s du mod le global du SdT est qu il poss de une boucle d interd pendance entre valeurs emp chant l initialisation des valeurs Cette boucle est facilement identifiable sur le mod le car la sortie du composant CommandeVo1 est branch e sur les entr es des capteurs Navigation et RadioAltimeter Ceci a pour effet de cr er dans le mod le des d finitions circulaires qu il faut viter pour cr er un mod le conforme la syntaxe AltaRica Data Flow Pour cela nous ajoutons un d lai dans le comportement associ la fonction CommandeVol La sortie Out n est pas modifi e instantan ment 90 6 4 EXIGENCES DE SURETE DE FONCTIONNEMENT DU SDT en fonction des nouvelles valeurs de ses entr es Elle n est modifi e qu apr s le tirage d un v nement interne update qui modifie une variable d tat pre_Out 1 node Function_3in 2 flow 3 sa 4 2 sa 5 In3 FailureType in 6 Out FailureType out state 8 pre_Out FailureType 9 event 10 update 11 init 12 AC O e ci 13 trans 14 Ini correct or In3 correct 15 and not pre_0ut erroneous update gt pre_0ut erroneous 16 al am
45. S leak and P21_rev init S true P12_rev false P12_nom false P21_rev false P21_nom false don A1 A1 A2 A1 and and and and A2 and I2 nom Dieu 02 rev Apr s cette modification nous obtenons les r sultats suivants Observateur simple double triple proba T 4 4 4 Pdistb 12 0 1 4 8 e 4 NPdistb 13 1 0 5 8 e 4 Pdisty 1 222 159 1 0 e 4 NPdisty 13 23 0 4 0 e 4 Pdistg 1 232 141 1 0 e 4 NPdistg 3 218 135 3 0 e 4 T 4 4 4 YBPhyd 0 12 2663 4 8 e 8 YBNPhyd 0 170 286 2 4 e 7 GYPhyd 0 201 195 1 1 e 7 GYNPhyd o 243 179 2 3 e 7 GBPhyd 0 12 2783 4 8 e 8 GBNPhyd o 40 2834 1 8 e 7 T 4 4 4 Phyd o o 3146 5 1 e 11 NPhyd o 1 2411 1 0 e 8 La premi re colonne du tableau pr c dent indique le nom de l observateur 117 CHAPITRE 7 SYSTEME HYDRAULIQUE D UN AVION DE TYPE A320 la seconde colonne donne le nombre de pannes simples qui conduisent la situation redout e observ e la troisi me colonne donne le nombre de pannes doubles la quatri me donne le nombre de pannes triples et la derni re colonne indique la probabilit d occurrence de cette situation Les probabilit s sont calcul es l aide de l outil
46. alable soit en parcourant progressivement l espace d tat ceci permet ne pas parcourir les tats qui ne sont pas pertinents pour une propri t soit en se fondant sur une repr sentation symbolique de l espace d tat ceci permet de parcourir et valuer en une seule tape un ensemble d tats atteints Dans ce dernier cas la repr sentation interne des tats accessibles et le parcours de ces derniers pour la v rification peuvent tre r alis s l aide de BDD Bry86 Une alternative consiste repr senter l espace d tats comme une formule bool enne puis utiliser des techniques de Binary Decision Diagram 12 2 2 MODELISATION ET VERIFICATION DE LA SECURITE DES SYSTEMES AERONAUTIQUES satisfaction de contraintes bool ennes pour v rifier les propri t s En pratique les outils de v rification automatique de propri t s sont sp cifiques a un type de mod le ou un langage de mod lisation particulier et un type de propri t s exprim es au moyen d une logique et de pr dicats donn s Parmi les outils de ModelChecking existants nous citerons tout d abord MEC5 Vin03 ABC94 permettant de v rifier des propri t s exprim es par des formules de p calcul EL86 sur des mod les AltaRica Ensuite les outil de la famille SMV Carnegie Mellon SMV Cadence Labs SMV et NuSMV CCGROO v rifient sur des mod les du type structure de Kripke McM98 des propri t s exprim es avec des formules CTL ou LTL
47. analyse CCA En premier lieu l av nement des architectures avioniques modulaires int gr es sur les avions civils r cents Boeing B77 Airbus A380 et A400M conduit partager des ressources de calcul et de communication entre plusieurs fonctions Ce partage est une source de d faillances de mode commun En effet la d faillance d un calculateur va entra ner la d faillance des diff rentes fonctions qui l utilisent En second lieu le d veloppement des avions tend s organiser autour de maquettes num riques d avion qui rendent possible l tude de l installation des quipements d s les phases amont du d veloppement des syst mes Et comme nous l avons d j vu dans la section pr c dente l installation des quipements au sein de l avion est une autre source de d faillances de mode commun Plus g n ralement durant plusieurs phases du d veloppement des syst mes les ing nieurs doivent proposer des allocations allocation des fonctions sur les quipements allocation de ces quipements sur des emplacement de l avion Il faut que l analyse CCA s assure que ces allocations soient s res c est dire qu elles n invalident pas les exigences de s curit du syst me tudi 1 4 Objectifs de la th se et d marche Nos discussions avec les ing nieurs en charge des analyses CCA ont abouti au constat suivant un premier souhait qu ils expriment serait de disposer de techniques permettant d valuer faci lement l
48. aux besoins de la fonction Commande de vol Une derni re information importante pour construire le syst me est le type des ressources mises disposition pour l allocation Le nombre de ressources n a pas vraiment d importance car comme nous le verrons plus tard un crit re d optimisation du syst me de contrainte consistant choisir la solution proposant le minimum de ressources ou bien proposant le minimum de connexion utiliser est mis en oeuvre Pour notre syst me sachant que l exigence permettant d viter la situation d un D gagement erron impose la s gr gation ind pendance de trois fonctions il est donc n cessaire d allouer le SdT sur au moins trois ressources mat rielles que nous nommerons R1 R2 R3 Ainsi le fichier de description permettant de construire le syst me de contrainte est enrichi par les informations suivantes Hypothese independance idpt ClAlarmComp Navigation 1 idpt ClAlarmComp Radar 1 idpt ClAlarmComp TFTAPanel 1 idpt ClAlarmComp VerAccComp 1 idpt_Navigation_Rolli idpt_Navigation_Rol12 15 15 idpt_Rolli_Roll2 1 Jf Directives d allocation alloc_CommandeVol_R3 1 Ress Ri R2 R3 95 CHAPITRE 6 LE SYSTEME DE SUIVI DE TERRAIN SDT D UN AVION DE CHASSE 6 7 Recherche et visualisation d allocation 6 7 1 Recherche d une allocation La recherche d une allocation est rendue automatique par la cr ation d une application En eff
49. compos de 2 d faillances distinctes Ainsi en rendant ind pendantes les diff rentes fonctions intervenant dans les contre exemples cex nous garantissons qu il faut au moins 2 d faillances pour atteindre la situation redout e gt F failure count gt 2 2 Appliquons pr sent cette technique d identification des ind pendances sur l exemple COM MON Pour identifier le premier couple de d faillances rendre ind pendant il faut v rifier la formule explicitant que le syst me ne peut pas rencontrer la situation redout e tudi e transitum ec oni 2 assert F Interrup Out error amp X Interrup Out error Pour forcer le syst me se reconfigurer nous ajoutons une hypoth se exprimant que l v nement update doit tre tir apr s chaque d faillance Cette propri t est exprim e en logique temporelle 1 Updates follow failure 2 assert G failure gt X event update 3 4 assume Updates_follow_failure Sous cette hypoth se les traces d x cution qui nous int ressent deviennent de la forme failure failure failure failure failure failure 4 4 update update update update update update Lors de la v rification de cette formule le model checker nous informe que le mod le ne satisfait pas cette propri t et nous le d montre en nous proposant le contre exemple suivant 74 5 2 DE L HYPOTHESE D INDEPENDANCE VERS LA CONTRAINTE DE
50. composants Cette d composition est assez naturelle car un syst me remplit une ou plusieurs fonctions en utilisant un ensemble de sous syst mes qui interagissent Par exemple dans un syst me hydraulique d avion la puissance fournie repose sur un ensemble de composants qui sont des tuyaux des pompes des vannes qui interagissent entre eux Il est donc n cessaire de mod liser en premier lieu chacun des composants constituant le syst me en prenant en compte ses caract ristiques relatives ce que l on souhaite v rifier Une fois le comportement interne des composants mod lis il est ensuite n cessaire de mod liser les interactions existantes entre ces composants Bien entendu les crit res que l on prend en compte pour cette mod lisation d pendent du type de v rification que l on souhaite faire par la suite Des langages d expression de mod les ont t d finis sp cifiquement aux diff rents crit res observer Nous en num rons quelques uns pour donner un aper u de la diversit du monde de la mod lisation des syst mes la repr sentation de l architecture d un syst me avec les langages de mod lisation UML EC97 et AADL FGH06 sous forme d un ensemble de composants interagissant Le syst me sera d crit essentiellement du point de vue de sa structure les caract ristiques intra composant ainsi que les caract ristiques inter composants les interactions la repr sentation d un syst me dans l
51. d une architecture mat rielle dans la recherche d une allocation s re Description Description mat rielle fonctionnelle eee Directives Contraintes Allocation Fic 4 15 D marche propos dans ce chapitre 68 L CHAPITRE 5 M THODE INT GR E DE RECHERCHE D ALLOCATION Ans cette partie nous proposons une technique qui partant du mod le d architecture fonctionnelle et d un mod le d architecture mat rielle doit permettre de trouver une relation d allocation Cette d marche consiste dans un premier temps extraire du mod le fonctionnel les hypoth ses n cessaires pour valider nos exigences puis transformer ces hypoth ses en contraintes pour orienter la recherche de la relation d allocation La r solution du syst me de contraintes permet de fournir aux concepteurs une premi re allocation ou lorsqu il n y a pas de solution elle permet d identifier les ressources pouvant poser probl me SOMMAIRE 5 1 IDENTIFIER LES HYPOTH SES D IND PENDANCE 5 1 1 Identification par analyse de sc narios 5 1 2 Identification des hypoth ses d ind pendance model checking 5 2 DE L HYPOTHESE D IND PENDANCE VERS LA CONTRAINTE DE SEGREGATION 5 3 ADAPTATION DE L ARCHITECTURE MATERIELLE 5 4 BILAN 70 70 71 75 77 80 69 CHAPITRE 5 METHODE INTEGREE DE RECHERCHE D ALLOCATION 5 1 Identifier les hypoth ses d ind pend
52. d une allocation 76 5 5 Notion de conflit sur une ressource 78 5 6 D marche pour la recherche d allocation incr mentale 79 5 7 Technique de division d une ressource en conflit 79 6 1 Tlustration du Suivi de Terrain 205i d le a ee due Yos dau 84 6 2 Mouvements possibles de l avion 85 6 3 Architecture fonctionnelle du Suivi de Terrain 86 6 4 Architecture mat rielle du Suivi de Terrain 87 6 5 Abstraction de la valeur d une donn e 88 D M dl AltaRica du dl iu 6 Lun d un da da Rien a Re E XCEC Gow 90 6 7 Observateurs associ s aux situations redout es 92 6 8 AllocViewer pour la visualisation des r sultats 98 6 9 Autres solutions possibles du syst me 99 7 1 Syst me Hydraulique del A320 102 7 2 Architecture du syst me Hydraulique 104 7 3 Mod lisation des informations circulant dans le syst me 106 7 4 Mod lisation des informations circulant dans le syst me en AltaRica 106 7 5 Automate du comportement d un r servoir 106 7 6 Les diff rents tats d un r servoir 107 7 7 Automate du comportem
53. dans la clause init dans notre exemple une variable bool enne suffit pour repr senter la pr sence ou l absence d une d faillance Il poss de galement un nombre fini de variables de flux flow permettant de repr senter les connexions possibles in out entre les composants Le type de ces variables repr sente le niveau d abstraction des valeurs chang es dans l exemple nous consid rons que le composant fournit en sa sortie out une valeur d notant son tat interne Plusieurs v nements event sont n cessaires pour mod liser les d faillances ou les reconfigu rations qui provoquent les changements d tats d crits dans les transitions dans l exemple le composant est sujet une d faillance fail error Les transitions trans repr sentent les aspects temporels des modes de fonctionnement et de dysfonctionnement Les gardes de ces transitions repr sentent la cause des v nements La partie droite de la transition permet l affectation consid rer lorsque la transition est tir e dans notre exemple la transition a pour effet le changement de la valeur de la variable d tat La partie assertion d un composant assert regroupe les relations de d pendance entre l tat du composant et la valeur de ses flux permettant ainsi de restreindre et de supprimer les compor tements impossibles ou inutiles dans l exemple nous souhaitons limiter la valeur de la variable de sortie la variable d tat L tat init
54. de deux valeurs erron es similaires En effet dans le cas de deux donn es erron es identiques ce composant ne peut pas faire la diff rence avec un cas de deux donn es correctes et identiques Dans ce cas il consid re bien que les valeurs sont identiques mais il est incapable d valuer le c t erron des donn es Le code AltaRica impl mentant un tel composant est le suivant 39 CHAPITRE 3 MOD LISATION ET ANALYSE DE L ALLOCATION 1 node equals 2 flow 3 4 4f Oe cit ES 5 qmm correct error 6 assert EI ADO 8 Ii I2 true 9 ELSE False 10 JE Fic 3 5 Le composant Equals 11 edon 2 Le composant Interrup quant lui permet comme son nom l indique d interrompre le flux de donn es fournit par COM Cette interruption est activ e par le signal la variable bool enne pro venant de Equals lorsque les valeurs des donn es produisent par COM et MON sont diff rentes Le code AltaRica mettant en ceuvre ce composant est le suivant 1 node interrup 2 flow 3 0 ou Correct error loss 4 ital e stia correct LOS co ey 5 ILA 6 assert 8 I2 false lost 9 else 1 10 PE Fic 3 6 Le composant Interrup 11 edon Voyons maintenant un exemple d analyse v rifiant que le mod le AltaRica global du syst me poss de bien le comportement souhait Afin de tester notre mod
55. de s ret de fonctionnement car elle est simple mettre en oeuvre et elle permet d valuer sur le m me mod le la tenue des exigences qualitatives et quantitatives La simulation La simulation est une autre technique permettant de parcourir les diff rents tats d un syst me Cette technique a pour principal int r t d exploiter directement la dynamique du syst me En effet partant de sa configuration initiale la simulation permet de d clencher les d faillances possibles et ainsi d observer la r action du syst me permise par sa dynamique reconfiguration propagation etc partir de cette technique une g n ration exhaustive de l ensemble des d faillances menant une situation redout e est possible En effet en simulant automatiquement des s quences de d faillance il est possible d observer si oui ou non le syst me atteint une situation redout e De plus tant donn qu un jeu de d faillances est d fini par l ordre d apparition de ses d faillances cette m thode permet d obtenir l ensemble des coupes menant la situation que l on souhaite observer Pour la suite on ne parlera plus de coupes mais de s quences car ces derni res conservent la propri t d ordre d occurrences des d faillances De plus pour des raisons pratiques la g n ration de s quences est born e par une longueur maximale ordre afin d viter l explosion combinatoire La limite principale de cette m thode r si
56. de vol de tous les appareils Airbus est tr s inf rieur au milliard d heures de vol Il faut donc fixer des exigences plus facilement v rifiables avec des taux de d faillance de l ordre d une fois toutes les 10 000 heures de vol ce qui repr sente tout de m me presque trois ann es d utilisation pour un avion qui fonctionne en moyenne 10 heures par jour C est pour cette raison qu il n est pas souhaitable qu une panne simple conduise une situation catastrophique dont le taux de d faillance est de l ordre de 107 par heure de vol Dans la suite de ce document nous consid rons une famille d exigences qualitatives qui corres pondent la fa on dont sont construits les syst mes a ronautiques Une combinaison de moins de pannes ne doit pas conduire une situation redout e class e Sev avec N 3 si Sev N 2 si Sev HAZ ou MAJ et N 1 si Sev MIN PSSA L objectif de cette analyse est de d montrer que la liste des conditions de panne issue de la FHA est compl te et d identifier de nouvelles exigences de s curit C est lors de cette analyse que l on identifie des strat gies de protection mettre en place afin de tenir les objectifs Une PSSA doit donc identifier les pannes et leurs combinaisons contribuant aux situations redout es explicit es par la FHA Les choix tablis par les concepteurs de l architecture du syst me sont ainsi v rifi s par des analyses de s curit r alis es g n ralement
57. donc s appliquer sur toutes les fonctions correspondantes aux d faillances Ainsi il faut d finir les ind pendantes suivantes idp COM MON 1 idp COM 82 1 idp S1 MON 1 idp S1 82 1 Identification de contraintes de co localisation En compl ment de cette analyse sur l ind pendance on remarque que S1 et COM de m me pour S2 et MON poss dent les m mes ind pendances Si nous supposons que COM et 51 sont allou s sur la m me ressource Ress alors nous pouvons remplacer les d faillances de COM et de 51 par la d faillance commune Ress alloc Ress_ alloc fail alloc COM fail alloc S1 fail Avec cette hypoth se il n apparait pas de nouveaux sc narios d ordre inf rieur 2 qui m nent notre FC Nous pouvons donc conclure que l allocation de 51 et de COM sur une m me ressource n invalide pas l exigence car si on remplace la d faillance de S1 et celle COM par une d faillance commune repr sentant la perte de la dite ressource alors il faut encore une d faillance pour atteindre la Cette remarque nous permet ainsi d ajouter notre syst me de nouvelles contraintes sur la co localisation respective de COM et 51 et de MON et 52 Ces contraintes enrichissent notre syst me avec coloc COM S1 1 coloc MON S2 1 5 1 2 Identification des hypoth ses d ind pendance par model checking La deuxi me technique possible pour identifier les taches qui doivent tre
58. e comme peu satisfaisante 7 6 Bilan L application que nous avons pr sent e dans ce chapitre nous a permis de montrer que les principes de mod lisation et d analyse de l allocation d une architecture fonctionnelle sur une architecture ma t rielle sont galement valables pour tudier l allocation spatiale d quipements install s dans l avion La collaboration avec les partenaires industriels et les laboratoires ayant travaill dans le projet ISAAC a permis de s assurer que l approche propos e avait un int r t industriel assez court terme L int r t du d veloppement de l outil MAPPINGMANAGER a t de convaincre les partenaires de la faisabilit de l approche L outil a aussi permis de tester rapidement les formats d entr e et de sortie n goci s au sein d ISAAC Depuis la fin du projet ISAAC en janvier 2007 les principes de l outil MAPPINGMANAGER ont t int gr s dans des outils industriels sous la forme de macros Excel par Alenia cet outil est utilis sur des d veloppements r els et comme plug ins dans l outil CATIA par Airbus cet outil est en cours de d veloppement et n a pas encore t d ploy industriellement Nous aurions souhait illustrer les techniques de recherche d allocation base de contraintes sur ce type d exemple Les mod lisations g om triques fournies par les partenaires d ISAAC nous semblent trop d taill es pour appliquer l approche que nous proposons Il serait bien enten
59. es de ce syst me sources fonctions Equals Obs 81 correct COM erroneous false lost S2 correct MON correct L analyse des valeurs observ es d montre bien que notre syst me poss de le comportement attendu En effet nous remarquons que le composant Equals signale la diff rence des donn es la valeur de sa variable de sortie vaut false et le composant Interrup interrompt bien le transfert de la donn e provenant de COM puisque la valeur observ e par Obs est lost valeur qui d note l absence de donn e Une limite possible ce comportement est atteinte lorsque des donn es erron es arrivent sur les 2 entr es du composant Equals il n est plus capable de d tecter que la valeur est erron e On suppose que les valeurs sont erron es de fa on coh rente c d qu elles ont la m me valeur Le comportement de ce composant est donc limit identifier une diff rence parmi ses entr es peu importe leurs valeurs sources fonctions Equals Obs 81 erroneous COM erroneous true erroneous 52 erroneous MON erroneous Par cons quent la limite du COM MON est qu il ne tol re pas le double erron En effet comme vu dans le tableau pr c dent ce m canisme ne peut emp cher la propagation d une donn e erron e lorsque les deux sources COM et MON fournissent une donn e erron e Une autre limite semblable du comportement de ce composant est
60. est la production de donn es erron es pendant au moins deux instants cons cutifs Nous utilisons l op rateur X Next de la Logique Temporelle Lin aire Pnu77 o X signifie que la propri t est vraie dans l tat suivant pour mod liser cette nouvelle situation redout e La formule Sr XSRr exprime que l tat courant correspond une situation redout e Sr Interrup 0ut error et que l tat suivant correspond aussi une situation redout e Par cons quent cette formule nous permet d identifier tous les tats o le syst me reste dans une situation redout e pendant 2 instants cons cutifs Comme nous ne nous int ressons qu aux combinaisons de pannes menant 4 la situation redout e une solution consiste ajouter un compteur de pannes afin de dissocier les v nements repr sentant les d faillances des autres v nements comme l v nement update Pour cela nous ajoutons au mod le SMV le composant failure count qui permet comme son nom l indique de compter les d faillances 1 module failure count failure 2 failure is true whenever the current event is a failure 3 INPUT failure boolean 4 count counts the failure up to 3 5 Comms OW 2 1 6 init count 0 7 the failure counter is incremented whenever 8 a failure is the current event and the maximal 9 number of failures 3 as not been reached 10 next count case 11 failure amp count 3
61. il faut absolument conserver sa taille lors de l allocation Il faut par cons quent que toutes les fonctions fx soient ind pendantes foi fx idp f 1 1 e k gt N Ce sc nario est admissible et on peut diminuer sa taille lors de l allocation Pour diminuer la taille du sc nario de fa on acceptable il suffit d avoir l ind pendance de N fonctions parmi les k fonctions pr sentes dans le sc nario 70 5 1 IDENTIFIER LES HYPOTHESES D IND PENDANCE Prenons pr sent l exemple du COM MON pr sent dans le chapitre 3 1 afin d illustrer comment identifier les ind pendances entre les fonctions n cessaires Partant de l analyse du mod le fonctionnel du COM MON nous allons tudier les diff rents sc narios menant une situation redout e FC exprimant que la sortie du COM MON est erron e Cette FC est class e MAJ donc les sc narios doivent contenir au moins 2 d faillances sortie OD em FIG 5 1 Mod le fonctionnel du COM MON Les diff rents sc narios menant FC sont les suivants COM fail error amp MON fail error COM fail error S2 fail error S1i fail error MON fail error Sil fail error amp S2 fail error Tous les sc narios poss dent 2 v nements et comme l indice de s v rit associ l exigence est aussi de 2 l allocation ne peut introduire aucun partage de ressource entre ces fonctions Les ind pendances doivent
62. ind pendantes consiste utiliser un model checker afin de trouver toutes les combinaisons de pannes qui m nent la situa tion redout e La technique mise en place utilise la traduction d AltaRica dans le langage SMV et l utilisation du model checker associ 71 CHAPITRE 5 METHODE INTEGREE DE RECHERCHE D ALLOCATION Cette m thode est utile pour traiter des mod les dynamiques Pour l illustrer nous transformons l exemple de l architecture COM MON cf figure 5 1 Prenons l exemple d une situation redout e correspondant la production d une valeur incorrecte en sortie du COM MON Cette valeur est produite par le composant nterrup et est caract ris e par la variable Out de ce composant Pour rendre l exemple plus int ressant nous ajoutons des d faillances ce composant qui pour l instant n en poss dait aucune Son comportement actuel permet en cas d in galit entre la valeur produite par COM et celle produite par MON d interrompre la liaison Or lorsque l alarme est d sactiv e la liaison est r tablie Ce comportement n est pas conforme au comportement r el d une architecture COM MON car la liaison reste interrompue quoiqu il arrive Pour am liorer cela nous proposons de modifier le comportement du noeud Interrup en ajoutant les deux v nements suivants 1 Un v nement update est n cessaire pour ouvrir l interrupteur en cas d alarme 2 tout moment l interrupteur peut su
63. le il faut le compl ter par deux sources 51 52 qui vont fournir aux fonctions COM et MON les donn es n cessaires Nous allons dans cet exemple v rifier que le couple de composants Equals Interrup permet lors d une d faillance sur la fonction COM ou MON de ne pas propager une donn e erron e Pour v rifier cette propri t un observateur Obs est ajout en sortie de Interrup pour contr ler la donn e fournie par ce composant Le mod le d exemple tester devient alors le suivant a Con D gt C Fic 3 7 Exemple utilis pour l analyse du COM MON Lors de la premi re ex cution de notre mod le les diff rentes valeurs en sortie de nos composants sont report es dans le tableau suivant sources fonctions Equals Obs 81 correct COM correct true correct so correct MON correct L analyse des valeurs du tableau montre que lorsque le syst me fonctionne la donn e qui est 36 3 2 MODELISATION DE L ARCHITECTURE FONCTIONNELLE observ e par le composant Obs est bien correcte Voyons maintenant la r action du syst me face une d faillance fail_error sur le composant COM fail_error FIG 3 8 Injection d une d faillance sur COM Cette d faillance a comme effet le changement de valeur de la donn e calcul e par COM Cette valeur modifi e va avoir une influence sur les composants qui manipulent cette donn e Regardons les valeurs observ
64. obtenons idpt ClAlarmComp 111 ou idpt ClAlarmComp Roll2 ou idpt Rolli Ro112 D gagement erron Cette situation redout e correspond la production d un ordre erron d une alarme et d un roulis erron L alarme de d gagement qui d coule de cette situation peut conduire la perte de l appareil Les diff rentes d faillances qui nous m nent cette situation sont les suivantes Number of minimal cuts 1 Erroneous_deg 0ut true C Navigation fail error Rolli fail_error amp Roll2 fail error Le seul sc nario qui m ne un d gagement dangereux est la combinaison de 3 d faillances Afin d viter qu une seule d faillance mat rielle n engendre cette situation il faut rendre au moins deux d faillances ind pendantes parmi les trois De plus il est possible d assurer un niveau de s ret suppl mentaire en consid rant simplement que chaque d faillance du sc nario doit tre ind pendante des autres Ce nouveau choix nous garantit qu au moins trois d faillances mat rielles distinctes sont n cessaires pour rencontrer ce d gagement dangereux Les nouvelles hypoth ses ind pendances d riv es sont donc les suivantes 93 CHAPITRE 6 LE SYSTEME DE SUIVI DE TERRAIN SDT D UN AVION DE CHASSE idpt Navigation Ro111 idpt Navigation Ro112 idpt Ro111 Ro112 3 Alarme intempestive Les r sultats obtenus sont Number of minimal cuts 3
65. occurrence inf rieur 107 par heure de vol pour cette situation La perte partielle de la puissance hydraulique correspond la perte d au moins deux lignes parmi les trois possibles En effet en cas de perte d au moins deux lignes les diff rentes fonctions importantes doivent tre aliment es par la derni re ligne disponible Nous devons donc nous assurer que les diff rentes logiques de reconfiguration permettent en cas de perte de plusieurs lignes de garantir l alimentation en puissance des l ments critiques de l avion Cette exigence est qualifi e MAJ car elle n entraine pas la perte de l avion mais assure le fonctionnement minimal n cessaire la protection de l appareil et donc de ses passagers L exigence qualitative que nous associons cette exigence est qu il ne faut pas qu une panne simple nous m ne cette situation Et l exigence quantitative fixe un taux d occurrence inf rieur 107 par heure de vol pour cette situation La perte d une simple ligne hydraulique n est pas une situation critique mais tant donn qu elle implique une partie de la source en puissance de l avion nous souhaitons maitriser les diff rents sc narios de pannes ind pendamment du nombre de d faillances menant la perte 104 7 3 MODELISATION DE L ARCHITECTURE FONCTIONNELLE DU SYSTEME HYDRAULIQUE dune ligne hydraulique Cette situation est donc consid r e comme MIN Nous n associons pas d exigence
66. par cons quent la perte de puissance de la ligne verte ce qui aboutit la perte des deux lignes Les r sultats ne sont pas satisfaisants non plus pour la perte totale de l hydraulique prioritaire cf la ligne du tableau pr cedent qui correspond l observateur Phyd puisque 151 combinaisons de deux pannes conduisent cette situation alors qu il n y en avait aucune avant l allocation De plus les probabilit s pour l hydraulique prioritaire comme non prioritaire sont inacceptables puisque qu elles sont tr s nettement sup rieures 107 cf les lignes du tableau pr cedent qui correspondent aux observateurs Phyd et NPhyd Pour corriger cette situation il est possible de modifier plusieurs aspects En premier lieu il est possible de modifier l emplacement des quipements ou le routage des canalisations pour qu ils ne soient plus impact s simultan ment par une trajectoire Par exemple dans l exemple pr c dent il faut loigner la ligne de distribution verte de la canalisation reliant le r servoir jaune aux pompes Ceci est possible en faisant passer les canalisations de la ligne verte par l arri re de l aile et les canalisations de la ligne jaune par l avant Lorsqu il n est pas possible d loigner les quipements il est possible de jouer sur les probabilit s des nouveaux v nements pour que les exigences quantitatives soient tenues Par exemple en 129 CHAPITRE 7 SYSTEME HYDRAULIQUE D UN AVION DE TYPE A320
67. possible pour le COM MON La mod lisation AltaRica correspondant cette allocation est repr sent e par l ajout des synchro nisations correspondantes dans le noeud englobant la fois l architecture mat rielle et l architecture fonctionnelle Le code AltaRica permettant la v rification de cette allocation est le suivant 1 node Main 2 sub 3 Syl s Se S SO CE 4 5 6 Sere ys y mG EC Sl Isis Ss ese 8 event 9 sr Gish il OE 10 assert 11 12 sync 13 lt SCralllo ci fai dos SC login Pas dos str 14 lt O IO SAS Za MONT 22 15 C EER AO SE q lose gt 16 ds edon Les nouvelles analyses effectu es sur ce mod le permettent d illustrer qu aucune panne unique ne m ne la situation du double erron En effet parmi les sc narios minimaux menant la situation redout e d une propagation par l interrupteur d une donn e erron e l allocation ne rajoute que 6 sc narios et aucun n est l ordre 1 COM fail error SM alloc fail error S1 fail error amp SM alloc fail error Equals fail error amp SC alloc fail error MO0N fail error SC alloc fail error 92 fail error amp SC alloc fail error 8C alloc
68. pour 10 7 l quipage blessures fatales ou s v res d un petit nombre de passagers Major R duction significative des marges de s curit ou des MAJ fonctions augmentation importante de la charge de travail 1079 pour l quipage inconfort pour les passagers blessures possibles Minor R duction l g re des marges de s curit ou des fonctions MIN augmentation de la charge de travail pour l quipage 107 inconfort pour les passagers TAB 1 1 Classification des d faillances dans la FHA La FHA d cline les situations redout es pour chaque phase de vol et d termine les diff rentes exigences respecter afin de limiter les effets des d faillances qui sont consid r es A chaque situation redout e est alors associ un objectif quantitatif relatif sa classification cf TAB 1 1 Cette exigence 1 2 PROCESSUS DE DEVELOPPEMENT DES SYSTEMES AERONAUTIQUES CRITIQUES quantitative est compl t e dans certains cas par un objectif qualitatif tel que Une panne simple ne doit pas conduire une situation redout e class e Catastrophique L objectif qualititatif est utile pour faciliter la v rification de la tenue des exigences quantitatives En effet la probabilit associ e l occurrence d une d faillance peut tre inf rieure une fois par milliard d heures de vol Or il n est pas possible de v rifier qu un quipement respecte effectivement ce type d exigences En effet le cumul des heures
69. pour une t che d utiliser une ressource mat rielle afin de pouvoir s ex cuter En effet la mod lisation de l architecture fonctionnelle correspond la mise en relation de l ensemble des fonctions n cessaires au syst me avec l ensemble des ressources mises disposition Chacune des fonctions mod lis es a un r le important pour le syst me global il faut donc s assurer que lors de l allocation aucune fonction ne se retrouve orpheline c d qu il n existe aucune fonction non allou e Vf E F 3r R alloc f r 1 4 1 2 Une fonction ne doit tre allou e qu une seule ressource Parmi les choix de mod lisation il a t d cid que toutes les fonctions taient uniques faut comprendre par unique le fait que chaque fonction est d di e une t che bien sp cifique Nous consid rons par exemple que la redondance d une fonction technique fr quemment utilis e pour la tol rance aux fautes engendre 2 fonctions diff rentes mais poss dant exacte ment le m me comportement fonctionnel Ces choix de mod lisation permettent de n avoir qu une seule ressource utiliser pour chaque fonction Vf Vri ro R alloc f alloc f r2 ra 4 2 Boolean satisfiability problem 55 CHAPITRE 4 RESOLUTION DE CONTRAINTES D ALLOCATION Les contraintes de connexions Deux fonctions connect es doivent le rester une fois allou es Cette contrainte stipule que l
70. re d optimisation afin de classer les solutions possibles Ce crit re va permettre de choisir parmi l ensemble des solutions possibles celles qui semblent les plus int ressantes Durant notre tude nous avons consid r un premier crit re d optimisation apportant un int r t certain pour le concepteur La solution optimale que nous allons consid rer est une solution utilisant le minimum de ressources Pour parvenir cette solution optimale nous allons pr senter le crit re d optimisation utilis Les crit res d optimisation Un crit re d optimisation correspond un aspect global du syst me qui est exprim en fonction de certaines variables Rappelons que la r solution du syst me de contraintes correspond la valuation des variables Le crit re consiste maximiser ou minimiser la valeur d un indicateur construit partir de ces variables pour ainsi diminuer l ensemble des solutions acceptables cf figure 4 5 65 CHAPITRE 4 RESOLUTION DE CONTRAINTES D ALLOCATION Solutions respectant les exigences Sdf Solutions optimales Fic 4 13 Ensemble des solutions optimales Solutions possibles L ajout d un crit re un syst me de contraintes s effectue en pla ant la d finition du crit re en d but du syst me pour respecter le formalisme de l outil SATZOO Par exemple si nous souhaitons minimiser le nombre des variables v1 v2 v3 qui sont vraies il suffit d crire la d finition
71. ressource intervient lorsqu au moins deux fonctions ind pendantes sont allou s une m me ressource 1M thode sp cifi e mais non impl ment e 77 CHAPITRE 5 METHODE INTEGREE DE RECHERCHE D ALLOCATION A h fi et fo sont ind pendants alloc A E T N rigs o FIG 5 5 Notion de conflit sur une ressource Cette nouvelle variable permet d tablir pour chaque ressource r R si plusieurs fonctions ind pendantes lui sont allou es Ainsi conflit r est d finie de la mani re suivante conflit R 0 1 con flit r 1 au moins 2 fonctions ind pendantes sont allou es r Finalement cette variable permet d identifier les ressources posant des difficult s pour l allocation Elle permet donc d aider un architecte cibler la partie de l architecture mat rielle modifier La probl matique de l identification des conflits est pr sent e dans l article PBR03 Minimiser le nombre de conflits Un crit re d optimisation permet de r duire le nombre de so lutions propos es pour ne calculer que la meilleure relativement ce crit re Le crit re d optimisation utilis dans nos travaux nombre de connexions peut tre remplac par le nombre de conflits En minimisant le nombre de conflits la solution propos e correspond la solution poss dant le moins de conflits de ressources Ainsi la solution obtenue repr sente l architecture la plus simple modifier en terme d ajout
72. ristiques diff rentes Afin d orienter les possibilit s d allocations les directives suivantes sont propos es la fonction f ne peut s ex cuter que sur une ressource de type et la fonction f3 quant elle ne doit tre allou e que sur une ressource ayant les m mes caract ristiques que ra et Pour mod liser ces directives il faut d finir set alloc fi ri et set alloc f2 ro r3 Ces directives peuvent tre repr sent es par la figure suivante 57 CHAPITRE 4 RESOLUTION DE CONTRAINTES D ALLOCATION set alloc set alloc m m FIG 4 7 Illustration de la relation Set Allocation La contrainte associ e cette directive doit s assurer que si l allocation d une fonction sur une ressource est propos e alors la ressource doit appartenir l ensemble des ressources permettant son ex cution Ainsi lorsque l ensemble set alloc f est d fini au moins une allocation doit tre effec tu sur une ressource de cet ensemble Cette contrainte peut s crire en logique de fa on suivante Vfi F ar set alloc f alloc f 4 4 Co localisation t et tg doivent tre allou es sur une m me ressource Suivant l architecture disponible et suivant les syst mes il se peut que certaines fonctions soient amen es communiquer entre elles fr quemment Sachant que ces fonctions sont amen es s changer des donn es il semble logique d v
73. s curit et la fiabilit des syst mes critiques utilis s dans l a ronautique un processus de d veloppement a t d fini et doit tre appliqu pour la conception de tout syst me CHAPITRE 1 INTRODUCTION avionique embarqu En effet pour qu un syst me soit certifi et donc embarquable il doit tre prouv que le processus en question l ARP 47696 a bien t appliqu L objectif est de ma triser les diff rentes tapes du d veloppement d un syst me critique pour obtenir au final un syst me digne de confiance c est dire satisfaisant les exigences qui lui sont associ es 1 2 Processus de d veloppement des syst mes a ronautiques critiques La plupart des industriels du domaine suivent les recommandations qui sont d finies dans le do cument ARP4754 47696 Bien entendu chaque industriel est libre de d finir un processus de d velop pement sp cialis pour r pondre aux sp cificit s de l entreprise ou du type d a ronef Par exemple la directive Airbus ABD200 Air96 sp cifie le processus d di la v rification de la s curit des syst mes a ronautiques embarqu s dans les avions Airbus Comme sch matis par la figure 1 2 ces recommandations s organisent autour d un processus d va luation de la stiret de fonctionnement d un syst me bas sur quatre analyses principales FHA Functional Hazard Assessment PSSA Preliminary System Safety Assessment SSA System Safety Asses
74. set of mappings lol xj Empty mapped items IRIS ATAZ4 branch982 2P TRU APU to MPC impacted m1 IRIS ATAZ4 branch4 3G impacted m2 AIRIS ATA24 branch1 102 25L GCU2 to IDG2 impacted m3 AIRIS ATA24 branch983 2P TRU APU to MPC impacted m4 AIRIS ATA24 branch984 2P TRU APU to MPC impacted m6 1IRIS ATA24 branch1104 25L GCU2 to IDG2 impacted m7 AIRIS ATA24 branch1001 1M 5000VE to 235VU 1M APUGEN to GAPCU 1M BCL APU to MainEBay impacted m8 AIRIS ATA24 branch476 2G impacted m11 AIRIS ATA24 branch1096 15L GCL1 to IDG1 impacted m20 AIRIS ATA24 branch474 1G impacted m21 4IRIS ATA24 branch1 103 25L GCU2 to IDG2 impacted m22 AIRIS ATA27 Rudder THS Control Cable impacted m23 AIRIS ATA24 branch1105 25L GCU2 to IDG2 impacted m27 Unmapped items IRIS ATA24 branch1095 15L GCUI to IDG1 impacted Multiple mapped items OCAS RUDDER ATA27 D2 SVb fail loss m26 m28 m14 m9 OCAS RUDDER ATA27 D2 P3 fail loss m24 m26 m28 m30 m12 m16 m17 OCAS RUDDER ATA27 D2 5Vg fail loss m30 m31 OCAS RUDDER_ATA27_D2 P1 fail_loss m30 m31 OCAS HYD_ATA29_D1 EDPa1 fail loss m33 m19 OCAS RUDDER ATA27 D2 P2 fail loss m26 m28 m14 m9 OCAS HYD ATA29 D1 distb fail loss m10 m29 m32 OCAS HYD ATA29 D1 EDPg2 fail loss m5 m15 m34 OCAS RUDDER_ATA27_D2 5Vy fail_loss m24 m26 m28 m12 m16 m17 Ok Check mappings window on the Check button to perform several sanity checks on the mapping
75. sur la n gation 1 vp Intuitivement une formule disjonctive 4 V v doit pouvoir se traduire en la somme des l ments avec une in galit V rifions cette intuition en comparant les tables 4 V y litt raux Ply vo uy vy 21 0 0 0 0 0 0 1 1 1 1 110 1 1 1 111 1 2 1 A nouveau la comparaison des tables permet de valider cette r gle de transformation pour les formules disjonctives trad V vp vy gt 1 Les diff rentes r gles de transformation que nous venons d identifier nous permettent de passer d une contrainte d crite en logique un syst me d in quations lin aires Elles sont r sum es dans le tableau suivant litt raux v Y vrai vol gt 1 vrai lt 1 v gt 1 VY Vail vptvy gt 1 60 4 5 TRANSFORMATION DU MODELE CSP EN SYSTEME D EQUATIONS LINEAIRES L application de ces diff rentes r gles de transformations sur nos contraintes logiques permet d obtenir les in quations lin aires correspondantes suivantes Aic Clause vrai WET trad Clause gt 1 Clause v v e e ri trad p gt 1 Deux fonctions connect es doivent le rester une fois allou es 4 3 Partant de la formule logique d finie pr c demment il faut trouver sa forme normale conjonctive correspondante VE MEF Yr r E R alloc f r alloc f r N f enm f P g
76. syst me de contraintes r soudre Afin d automatiser la cr ation du syst me un fichier de description de l architecture fonctionnelle est n cessaire Ce fichier ne comporte que la description des connexions entre les fonctions En effet gr ce la seule information des connexions nous pouvons en d duire la liste des fonctions du syst me puisque chaque fonction du syst me utilise ou produit au moins une donn e et l envoie une autre fonction Connexions fonctionnelles f_cnx_Radar_VerAccComp 1 f_cnx_TFTAPanel_VerAccComp 1 f_cnx_Navigation_VerAccComp 1 f_cnx_Navigation_ClAlarmComp 1 94 6 6 GENERATION DES CONTRAINTES D ALLOCATION f_cnx_RadioAltimeter_ClAlarmComp 1 f_cnx_Rolli_ConsRollComp 1 f_cnx_Rol12_ConsRollComp 1 f_cnx_VerAccComp_CommandeVol 1 f cnx ClAlarmComp CommandeVol 1 f cnx ConsRollComp CommandeVol 1 f CommandeVol Navigation 1 f cnx CommandeVol RadioAltimeter 1 Le fichier de description est ensuite compl t par les hypoth ses d ind pendance pr c demment identifi es et par les directives d allocations propres au syst me Pour notre syst me nous souhaitons allouer la fonction de commande de vol une ressource particuli re car nous supposons que cette fonction n cessite une ressource ayant certaines caract ristiques Nous supposons ainsi que la ressource R3 poss de des caract ristiques qui lui sont propres et r pond
77. visible en pr sence des d faillances fail lost sources fonctions Equals Obs 81 lost lost 82 lost MON lost true lost En effet en cas de cette d faillance sur les sources ou les fonctions COM et MON le composant n est pas capable de d tecter l absence de donn e engendr e par ces d faillances et par cons quent la propagation ne sera pas stopp e 37 CHAPITRE 3 MOD LISATION ET ANALYSE DE L ALLOCATION 3 3 Mod lisation de l architecture mat rielle 3 3 1 Architecture mat rielle informatique La mod lisation de l architecture mat rielle s effectue de la m me fa on que l architecture fonction nelle mis part le fait qu il n y a que deux types de ressources ressource de communication Bus repr sentant la relation r _cnx de l architecture mat rielle et ressource de calcul Cpu repr sentant un l ment de R a Ressource de communication b Ressource de calcul Fic 3 9 Ressources mat rielles Une ressource de communication fig 3 9 a permet le transport des diff rentes donn es d un syst me Les d faillances que nous consid rons comme int ressantes pour cette ressource sont La corruption des donn es transport es due une erreur dans le protocole de communication par exemple une interf rence lectromagn tique peut entra ner un dysfonctionnement dans la transmission et par cons quent les donn es transmises s
78. 0 tyre burst for hydraulic system gt lt failmode component G HP distribution 2 fm impacted gt lt failmode component Y Suction rsvy EDP fm impacted gt lt trajectorydetails theta 9 0 kappa_in 127 kappa_out 131 gt lt trajectorydetails theta 11 0 kappa_in 127 kappa_out 131 gt lt trajectorydetails theta 15 0 kappa_in 129 kappa_out 135 gt lt hitlistitem gt lt hitlist gt lt hitlistitem name fail_tyre_burst_W4_Theta_minus15_9_Kappa_127_135 nba Dans cet exemple nous pouvons d duire de l analyse du fichier qu il s agit d une Hitlist provenant du monde Geometrical with IRIS information donn e par le champ name Comme d crit dans la section 7 3 3 il s agit d une Hitlist provenant d une analyse d une maquette num rique en 3 dimensions r alis e avec le logiciel IRIS Le champ description permet de noter qu il s agit ici d une analyse d clatement pneu d un avion de type Airbus A320 restreinte aux quipements du syst me hydraulique Le champ hitlistitem regroupe des trajectoires qui impactent les m mes quipements L exemple montre le groupe de trajectoires baptis fail tyre burst W4 Theta minusi5 9 Kappa 127 135 Ces trajectoires sont li es l clatement du 4M pneu pour des paires d angle compris entre 157 135 et 9 127 Pour toutes ces trajectoires les quipements G HP distribution 2 ligne distribution verte et Y Suction rsvy
79. 06 Cette annexe permet de d crire des mod les d erreur pour la mod lisation du comportement en pr sence de fautes La d marche g n rale propos e dans ces travaux est repr sent e dans la figure 8 1 elle consiste cr er un mod le d erreur du comportement de chaque composant en pr sence de ses propres fautes et ventuellement de ses r parations sans tenir compte de son environnement Des attributs permettent d ajouter aux v nements une probabilit d occurrence ainsi que de d finir des flux d di s au d clenchement de transitions Avionics Architecture Description Language 132 8 2 COMPARAISON AVEC DES TRAVAUX SIMILAIRES ce qui permet de mod liser les aspects probabilistes et structurels associ s la propagation de panne Ensuite par un ensemble de r gles de transformation it ratives l auteur construit le mod le de r seaux de Petri pouvant tre ensuite analys BAK04 KB96 BMT99 Mod le AADL tendu Mod le Mod le d architecture d erreur Transformation de mod le R seau de Petri FIG 8 1 Transformation de mod les ADDL avec un mod le d erreur en r seaux de Petri La description du mod le d erreur utilis pour effectuer les analyses de s ret de fonctionnement est int gralement exprimable a l aide du langage AltaRica Alors que la conception de mod le AltaRica est auto suffisante pour effectuer ces m mes analyses les mod les AADL doivent tre enr
80. 122 TO VERIFICATION DE L ALLOCATION SPATIALE 221213 2393939 Aa 127 Tod Nouvelles analysed o oaa oe GG ee Ee HAR GE 4 9 909 RR 128 Ww NECIO et ich salt oP iS ae ae es ae a Di Di A AU 130 101 CHAPITRE 7 SYSTEME HYDRAULIQUE D UN AVION DE TYPE A320 7 1 D marche utilis e La d marche que nous avons d finie dans le projet ISAAC consiste injecter les r sultats des analyses d un risque particulier dans le mod le AltaRica d architecture fonctionnelle Actuellement l analyse d un mod le pour un risque particulier par exemple pour un risque d clatement moteur consiste trouver l ensemble des l ments impact s pour chaque trajectoire de d bris eject lors de l clatement Une fois ces r sultats obtenus l analyste doit valuer si ces trajectoires conduisent des situations invalidant les exigences de s ret de fonctionnement Cette m thodologie est d compos e en plusieurs tapes 1 Construction du mod le d architecture fonctionnelle avec AltaRica et du mod le d installation avec IRIS pour le syst me tudi 2 Allocation des fonctions sur les composants du mod le d installation 3 Calcul des ensembles de composants impact s par un clatement pneu ou moteur 4 Extension du mod le d architecture fonctionnelle avec des v nements repr sentant la d faillance simultan e de toutes les fonctions allou es sur un composant impact par un clatemen
81. 2 EL86 ES03 FGH06 FLVO3 FP93 Gob02 GT04 HCDJ06 HCDJOS CAMBAZARD P E HLADIK A M DEPLANCHE N JUSSIEN ET YVON TRIN QUET D composition et apprentissage pour un probl me d allocation de t ches temps r el Dans 10e Journ es nationales sur la r solution pratique de probl mes NP complets JNPC 04 pages 123 138 Angers France 2004 CLEARSY Manuel de r f rence du langage B Support Atelier B F vrier 2007 http www atelierb societe com documents htm S A COOK The complexity of theorem proving procedures Dans STOC 71 Pro ceedings of the third annual ACM symposium on Theory of computing pages 151 158 New York NY USA 1971 ACM F CASSEZ C PAGETTI ET O ROUX A timed extension for altarica Fundam Inf 62 3 4 291 332 2004 DASSAULT SYSTEMS CATIA Basic 8D Design User s Manual 1985 X DUMAS C PAGETTI L SAGASPE P BIEBER ET P DHAUSSY Vers la g n ration de mod les de s ret de fonctionnement Dans conf rences LMO 8 et CAL 08 Mars 2008 A EVANS ET T CLARK Foundations of the Unified Modeling Language Dans Proc of the 2nd BCS FACS Northern Formal Methods Workshop Ilkley UK 23 24 September 1997 1997 E A EMERSON ET J Y HALPERN Decision procedures and expressiveness in the tem poral logic of branching time Dans In Proceedings of the Fourteenth Annual ACM Sym postum on theory of Computing STOC 82 San Francisco Californi
82. 4 2 2 MODELISATION ET VERIFICATION DE LA SECURITE DES SYSTEMES AERONAUTIQUES Ev nement Redout E D faillance du composant C D faillance du composant A D faillance du composant B Fic 2 8 Exemple de repr sentation d un arbre de d faillances L analyse qualitative par arbre de d faillances consiste d terminer l ensemble des coupes mini males Une coupe est un sous ensemble d v nements dont l existence simultan e m ne l v nement redout et cela ind pendamment de l occurrence ou non occurrence des autres v nements de l AdD Une coupe minimale est une combinaison d v nements n cessaires et suffisants pour conduire la situation redout e La recherche des coupes minimales se fait partir d une transformation de l arbre en une expression bool enne et de l utilisation des lois de l alg bre de Boole pour obtenir une expression bool enne r duite de l v nement redout RY 97 L analyse quantitative quant elle vise assigner partir des probabilit s d occurrence des v nements l mentaires la probabilit d occurrence de l v nement redout ainsi que des v nements interm diaires La m thode permettant de construire un arbre de d faillances partir d un mod le AltaRica est pr sent e dans Rau02 Dans cet article Antoine Rauzy pr sente un algorithme permettant la compi lation d automates de mode en quations bool ennes Il pr sente deux int r t
83. 6 7 Recherche et visualisation d allocation 6 7 1 Recherche d une 6 7 2 Visualisation de l allocation A A Eb BA d 7 7 Syst me Hydraulique d un avion de type A320 TJ D marche utilis e lt 5 44 4 zb ua a b on ee RED Dh cR Ox pe 7 2 Pr sentation du syst me lt a vs esei eee Roy pig EO LR E R qo uon ue uet ho ue Es a A 122 Les exigences v rifier o m oos sese a m o ed 7 3 Mod lisation de l architecture fonctionnelle du syst me hydraulique 7 3 1 Mod lisation des l ments du syst me Hydraulique ToS Validation du modela coe eaa Ness d 08 bee 7 3 3 Mod lisation g om trique 7 3 4 Les l ments impact s sous forme de HitList 7 4 Mod lisation de l allocation spatiale 7 5 V rification de l allocation spatiale 1 9 1 Wouvellesgmalyses oo 222 99 e Lee x EU die pn C D ae ee eee de es es A A 8 Conclusion 8 1 Bilan des travaux effectu s gt o 2 2 5 2 Li da RE bE RE REED o ERE E EA 8 2 Comparaison avec des travaux similaires 8 2 1 Analyses de mod les 8 2 2 D finition d allocation par r solution de contrai
84. EDP canalisation reliant le r servoir jaune avec la Pompe moteur jaune sont d t rior s Le champ trajectorydetails est utilis pour stocker des informations comme les angles des tra jectoires qui conduisent cet impact Dans le cas illustr la premi re ligne trajectorydetails indique que les trajectoires 9 127 9 129 et 9 131 impactent les m mes quipements du syst me hydraulique Les lignes suivantes concernent des trajectoires avec 0 gal 11 et 15 L attribut nb indique le nombre de trajectoires regroup es dans ce histlistitem soit 10 tra jectoires Cet attribue est utile pour valuer l impact d une allocation spatiale sur la tenue des exigences quantitatives de s rete de fonctionnement 7 4 Mod lisation de l allocation spatiale Dans cette section nous montrons l int r t d une mise en relation des mod les AltaRica et des mod les g om triques IRIS par l identification d un sc nario non pr vu li l installation Nous montrons comment les analyses du nouveau mod le AltaRica mod le incluant les placements des quipements dans l avion vont nous permettre d am liorer une installation existante Nous illustrons galement comment utiliser le MAPPINGMANAGER pour mettre en relation les mod les AltaRica et IRIS partir d une HitList L allocation spatiale que nous allons chercher v rifier a t labor e au cours de diff rentes r unions du projet ISAAC avec les cor
85. HP Distribution3 Pdistb B HP Distribution4 B HP Distribution5 FlapsLR SlatsLR spoller3 elevatorLR aileronLR 124 7 4 MODELISATION DE L ALLOCATION SPATIALE Nous avons d velopp l outil MAPPINGMANAGER O afin de faciliter la saisie de l allocation des quipements du mod le AltaRica sur les quipements du mod le g om trique Le principe de fonctionnement de cet outil est simple voir l annexe A Partant d une liste de composants g om triques et d une liste de composants fonctionnels issus d un mod le AltaRica l outil permet la mise en correspondance des l ments par une interface graphique cf figure 7 25 List of mappings List of Components X List of Components Left Right Glow Y Suctior vp EDP impacted New mapping entry Automatic mapping Button 2320 hi NPdetg lal lost 320 td P sto fadi loss 5320 m Green G HP Ontb 320 is Green G HP Distib Button area ave Load Import List of mapped components Fic 7 25 Interface du MappingManager Exemple de liste de composants pouvant tre utilis s par l outil lt failmodes name Geometrical gt lt failmode component G HP EDP TConnection fm impacted description This T connection links the Green Engine Driven Pump with the High Pressure Pipe gt lt failmode component B HP Distribution 1 fm impacted d scription Blue High Pressure Distribution line inet part V lt failmode com
86. Leackage FIG 7 9 Automate du comportement d un consommateur La transcription en AltaRica de ce comportement peut s exprimer de la fa on suivante node dist 1 2 flow 3 mom 2 a 4 SAS ME OO 2 Cita E 5 state 6 SIDO OL 7 event 8 fail_Leackage 9 init 10 true 11 trans 12 S true fail_leackage gt S false 13 assert 14 I rev S 15 edon 6 Le PTU est un des composants les plus complexes car il doit observer l tat de deux lignes hydrauliques afin de pouvoir faire basculer de la puissance d une premi re ligne vers une seconde s il vient d tecter la perte de puissance dans la seconde ligne Ce composant poss de donc des entr es afin de r cup rer de la puissance hydraulique I1 nom repr sente la puissance hydraulique de la ligne 1 I2 nom repr sente la puissance hydraulique de la ligne 2 et des sorties pour la transmettre sur l autre ligne 01 nom repr sente la puissance hydraulique fournie la ligne 1 par la ligne 2 02 nom repr sente la puissance hydraulique fournie la ligne 2 par la ligne 1 Il poss de galement des entr es A1 est vraie lorsqu il y a de la puissance hydraulique sur la ligne 1 et A2 est vraie lorsqu il y a de la puissance hydraulique sur la ligne 2 permettant d observer l tat des lignes hydrauliques et donc d activer le m canisme de transfert de puissance hydraulique Activation de I1 vers O2 A1 Flux sortant par le port O1
87. N d ordre 3707 THESE PRESENTEE A L UNIVERSIT BORDEAUX I ECOLE DOCTORALE DE MATHEMATIQUES ET INFORMATIQUE Par Laurent Sagaspe POUR OBTENIR LE GRADE DE DOCTEUR SPECIALITE Informatique Allocation s re dans les syst mes a ronautiques Mod lisation V rification et G n ration Soutenue le 4 D cembre 2008 Apr s avis de Fabrice Kordon Rapporteurs Jean Paul Bodeveix Rapporteurs Devant la Commission d examen form e de Jean Michel Couvreur Professeur des universit s LIFO Pierre Bieber Ing nieur de recherche ONERA Alain Griffault Maitre de Conf rences LaBRI Jean Philippe Domenger Professeur des universit s LaBRI Igor Walukiewicz Directeur de Recherche CNRS LaBRI Fabrice Kordon Professeur des universit s LIP6 Jean Paul Bodeveix Professeur des universit s IRIT 2008_ Directeur de Th se Co Directeur de Th se Examinateurs Examinateurs Examinateurs Rapporteur Rapporteur Remerciements Voil c est avec beaucoup de plaisir et d motion que je r dige ces derniers mots qui signent la fin de mon aventure de doctorant Je tiens remercier en premier lieu Fabrice Kordon et Jean Paul Bodeveix pour avoir accept d tre les rapporteurs de mes travaux de th se ainsi que Igor Walukiewicz Jean Philippe Domenger et Jean Michel Couvreur pour avoir accept de constituer mon jury de th se Chacun d entre eux m a apport de pr cieuses critiques enrichissantes pour mes trav
88. NTRODUCTION Pour le second sous objectif nous proposons d utiliser des techniques de r solution de contraintes Il faut donc mod liser le probl me de l allocation des l ments de l architecture fonctionnelle sur les l ments de l architecture mat rielle sous forme de contraintes Il est aussi n cessaire de d crire des directives d allocation telles que la s gr gation entre fonctions Ces directives peuvent tre mises par les concepteurs des syst mes mais nous proposons aussi une technique permettant de d river ces directives partir des r sultats des analyses de s curit effectu es sur la base du mod le fonctionnel Finalement nous avons tudi la possibilit de sugg rer des modifications de l architecture mat rielle lorsqu aucune allocation ne peut tre propos e par les techniques de r solution de contraintes 1 5 Plan de lecture de la th se Dans le chapitre 2 nous commen ons par introduire les concepts de mod lisation de syst mes et de v rification formelle de propri t s Nous pr sentons ensuite relativement au cadre d tude de la s ret de fonctionnement le type d exigences que l on souhaite v rifier ainsi qu un survol des langages de mod lisation adapt s Nous pr sentons pour finir ce chapitre le langage de mod lisation AltaRica que nous avons choisi pour nos travaux ainsi que les diff rents types d analyses associ s Ensuite dans le chapitre 3 nous d crivons notre approche pou
89. P distribution 2 fm impacted description Blue High Pressure Distrib line part2 gt lt failmode world Geometrical component B HP distribution 3 fm impacted description Blue High Pressure Distrib line part3 gt lt map gt lt mapping gt 7 5 V rification de l allocation spatiale Comme nous l avons vu dans les chapitres pr c dents nous repr sentons une allocation en introdui sant dans un mod le AltaRica des d faillances de causes communes qui regroupent les d faillances des composants allou s une m me ressource Dans ce chapitre nous pourrions analyser de la m me facon Vallocation spatiale en analysant l effet sur le mod le AltaRica de la d faillance de chaque composant du mod le g om trique Par exemple la d faillance de l quipement G Suction rsvg EDP entra ne la perte des composants EDPg et rsvg ce qui conduit la perte de la ligne verte jusqu ce que le PTU alimente les consommateurs verts avec 1 hydraulique jaune Mais le mod le g om trique fournit travers les Hitlists des informations suppl mentaires sur les d pendances entre quipements que nous cherchons exploiter Nous introduisons des d faillances de cause commune qui regroupent les d faillances des composants du mod le AltaRica qui correspondent aux quipements impact s par une trajectoire de d bris de pneu ou de moteur Pour enrichir le mod le AltaRica avec les informations provenant des Hitlist nou
90. PINGMANAGER Selected mapping Mapping Manager 7 r Mapping Manager impactedOnly List of mapped r Left a320_iris Components impacted al Left Blue B HP Distribution41 impacted c Mappirfis impactedOnly gt gt gt List of mapped Components Right Green G HP EDP TConnection impacted Green G Suction tsvg EDP impacted ellow HP Distribution3 impacted ellow Y HP EDP T Connection impacted ellow Y Suction rsvy EDP impacted r Current GreenDist gt a320_fxl NPdista fail loss 320 f l Pdistg fail loss 3320 iris Green G HP Distrib 3320 iris Green G HP Distrib List of mapped components gi Add Remove View New Viewing a mapping 2 4 View a mapping Select a mapping by double clicking on its name in the mapping list The names of mapped components should appear on the list of mapped items and their names should be coloured in Purple in the component lists 2 5 Remove a mapping Select a mapping by double clicking on its name in the mapping list Click on the Remove button to remove the mapping 2 6 Save mappings into a file Click on the Save button to save mappings into a file a window will appear to help you select a file 2 7 Load mappings from a file Click on the Load button to load mappings from a file a window will appear to help you select a file 144 2 8 Click Check a
91. QUES POUR LA MODELISATION ET LA VERIFICATION 28 DEUXIEME PARTIE METHODE PROPOSEE L CHAPITRE 3 MOD LISATION ET ANALYSE DE LALLOCATION D cette partie nous expliquons comment mod liser la relation d allocation dans un mod le AltaRica puis comment v rifier les exigences sur ce mod le d allocation Nous justifions la correspondance faite entre la notion de synchronisation en AltaRica et le concept d allocation SOMMAIRE 3 1 D FINITIONS PR LIMINAIRES 4 4 4 4 4 da teka raha de ha beha re dh ri 3 2 MOD LISATION DE L ARCHITECTURE FONCTIONNELLE 3 3 MOD LISATION DE L ARCHITECTURE MATERIELLE 3 3 1 Architecture mat rielle informatique 3 32 nno Roc mm a eum X X X AREER FRERE X a 3 4 MOD LISATION DE L ALLOCATION 3 4 1 Application au COM MON 3 5 BILAN 32 33 38 38 42 44 46 49 3l CHAPITRE 3 MOD LISATION ET ANALYSE DE L ALLOCATION 3 1 D finitions pr liminaires Le syst me qui nous int resse est mod lis sous la forme d une architecture fonctionnelle l en semble des fonctions n cessaires et d une architecture mat rielle l ensemble de ressources disponibles L architecture fonctionnelle est caract ris e par un graphe F f cnx orient pour lequel l ensemble des noeuds F fi fm d signe les fonctions et l ensemble des arcs f cnx C F x F repr sen tant les communications entre les fonctions Un arc rij f cnz fi f mod
92. RE 3 MOD LISATION ET ANALYSE DE L ALLOCATION 50 L CHAPITRE 4 R SOLUTION DE CONTRAINTES D ALLOCATION Omme vu pr c demment la validation d une allocation passe par l analyse des archi tectures et la v rification des exigences suivant l allocation Nous souhaitons pouvoir aborder le probl me d une mani re oppos e c est dire partant d une description de l archi tecture fonctionnelle et des diff rentes exigences v rifier chercher en d duire une relation d allocation ainsi que l architecture mat rielle qui les garantit Dans cette partie nous d taillons comment utiliser le formalisme des syst mes de contraintes pour r soudre un probl me d allocation Le probl me d allocation consiste trouver l allocation alloc respectant un ensemble de contraintes num r es par la suite La r solution de ce probl me est possible condi tion de transformer le probl me d allocation en un Probl me de Satisfaction de Contraintes csP Constraint Satisfaction Problem SOMMAIRE 4 1 MOD LISATION ET APPROCHE PAR CONTRAINTES 4 2 LES VARIABLES DU PROBLEME D ALLOCATION o co ca sa 6 6 94 6 3 4 3 LE DOMAINE DES VARIABLES UTILIS ES 4421 LESCONTRAINTES 3l om 03x be ae AM ua LE ee AA or e BAS Y ed 4 5 TRANSFORMATION DU MOD LE CSP EN SYSTEME D EQUATIONS LIN AIRES 4 5 1 Des relations vers des var
93. SEGREGATION 1 using Updates_follow_failure prove failure_cond 2 3 CounterExample COM fail error update Interrup fail close L analyse du contre exemple permet d identifier un premier couple de fonctions rendre ind pendantes savoir COM et Interrup Pour identifier les autres relations d ind pendance n cessaires afin de valider la propri t consid r e il faut changer la propri t en prenant en compte le premier contre exemple identifi La propri t devient e 2 assert F Interrup 0ut error X Interrup Out error gt 3 F event COM fail error amp F event Interrup fail close La v rification de cette formule nous propose un nouveau contre exemple permettant l identification d une nouvelle ind pendance entre fonctions Pour l exemple COM MON la v rification de la propri t est possible apr s identification des ind pendances suivantes idp COM Interrup 1 idp S1 Interrup 1 Ainsi de cette mani re incr mentale nous construisons une formule qui peut tre g n ralis e par la suivante F SRAXSR M F ev A F ev evi ev Eidp o ev ev correspond une paire de d faillances l mentaires Afin de prouver l exigence de s ret nous devons nous assurer que toutes les d faillances regroup es en paires sont ind pendantes Nous d rivons les hypoth ses d ind pendance de la forme Vi j
94. _Kappa_127_13 est ajout qui regroupe les v nements suivants Pdistg fail_lost NormBrakes fail_leakage RevEngl fail_leakage Yawdamper1 fail_leakage FlapsR fail_leakage Rudderg fail leakage Spoiler fail leakage Stabilizer fail leakage elevatoril fail leakage 127 CHAPITRE 7 SYSTEME HYDRAULIQUE D UN AVION DE TYPE A320 aileronR fail_leakage Spoilerb5 fail leakage rsvy fail lost EDPy fail lost EMPy fail lost Voici l algorithme nous permettant de construire les synchronisations ajouter au mod le AltaRica Algorithme 1 Obtention des synchronisations entr es Une Hitlist Hl hl hlo hln une allocation Mapp Cr gt Cf est l ensemble des composants du mod le AltaRica et C est l ensemble des composants du mod le g om trique sortie Un vecteur de synchronisation Wisi pour 1 n faire hl 1 pour j 1 m faire si Mapp cpi lt vide alors retourner Pas de correspodance sinon Ul syne Mapp cp retourner Visyne Nous obtenons donc dans le mod le AltaRica une nouvelle d faillance pour chaque analyse d duite de la Hitlist Cette d faillance repr sente la synchronisation de tous les composants AltaRica impact s par une trajectoire donn e L ajout de nouvelles d faillances dans le mod le AltaRica ne doit pas invalider nos exigences de d
95. a United States May 05 07 1982 ACM New York NY 169 180 E A EMERSON ET C LEI Model checking in the propositional mu calculus Rapport Technique University of Texas at Austin Austin TX USA 1986 N EEN ET N SORENSSON An extensible sat solver Dans SAT pages 502 518 2003 P H D GLUCH ET J J HUDAK The Ar chitecture Analysis amp Design Language AADL An Introduc tion Rapport Technique Software Engineering Institute SEI http www sei cmu edu publications documents 06 reports 06tn011 html 2006 P H FEILER B LEWIS ET S VESTAL The SAE architecture analysis amp design lan guage AADL standard A basis for model based architecture driven embedded systems engineering Dans RTAS 2003 Worshop on Model Driven Embedded Systems Washing ton D C May 2003 IEEE L FRIBOURG ET M VELOSO PEIXOTO Concurrent constraint automata Dans ILPS 193 Proceedings of the 1998 international symposium on Logic programming page 656 Cambridge MA USA 1993 MIT Press R GOBARD Traduction altarica vers lustre Rapport Technique LaBRI 2002 E GIUNCHIGLIA ET A TACCHELLA diteurs Theory and Applications of Satisfiability Testing 6th International Conference SAT 2008 Santa Margherita Ligure Italy May 5 8 2008 Selected Revised Papers volume 2919 de Lecture Notes in Computer Science Springer 2004 P E HLADIK H CAMBAZARD A M DEPLANCHE ET N JUSSIEN Guiding architec tural desi
96. a formalisation de cette situation redout e dans le mod le SdT est Pitch Out erroneous amp Alarm 0ut false Manoeuvre de D gagement erron e La manoeuvre de d gagement n cessite de disposer d un angle de roulis correct Si l angle de roulis est erron la manoeuvre peut conduire la perte de l appareil La formalisation de cette situation redout e dans le mod le SdT est Pitch Out erroneous Alarm 0ut true amp Roll Out erroneous 91 CHAPITRE 6 LE SYSTEME DE SUIVI DE TERRAIN SDT D UN AVION DE CHASSE Exigences Majeures D gagement intempestif Cette situation appara t lorsque l alarme se d clenche alors que l ordre de tangage est calcul correctement Cette situation est redout e puisque le d gagement peut g ner le pilote et l emp cher de terminer sa mission correctement La formalisation de cette situation redout e dans le mod le SAT est Pitch Out correct Alarm 0ut true Exigences Mineures Perte du SdT La perte du syst me SDT n est pas une situation risque mais nous ne souhaitons pas que cette situation apparaisse trop souvent Nous voulons donc identifier l ensemble des d faillances qui causent l arr t de ce pilotage automatique La formalisation de cette situation redout e dans le mod le SdT est Pitch 0ut lost Pour chacune de ces exigences nous associons un noeud observateur en AltaRica et nous effectuons les v rific
97. a revient remplacer ces deux v nements par Synchronisation g a and g_b sync ab gt X a X b Ab Diffusion g_a or g_b sync ab gt X a if g_a then A a X b if g_b then A b DCC g a or g b sync ab gt X a if g_a then A a X b if g b then A b g_a l gt g_b l e_b gt X_b Ab Nous avons ici d crit les principales caract ristiques du langage AltaRica Nous proposerons des mod les AltaRica repr sentant des syst mes complexes dans les chapitres suivants 2 2 4 Analyses et outils disponibles pour le langage AltaRica L valuation de la s ret de fonctionnement d un syst me consiste analyser les d faillances de composants pour d terminer leurs causes et estimer leurs cons quences sur le service rendu par le syst me L analyse de s ret de fonctionnement peut tre qualitative et ou quantitative L analyse qualitative a pour but la d monstration de propri t s par l identification de l ensemble des sc narios menant le syst me d un tat de fonctionnement normal vers un tat redout Les sc narios correspondent aux diff rentes combinaisons de d faillances menant la situation re dout e L analyse quantitative a pour objectif de quantifier les sc narios d termin s par l analyse qualitative en terme de probabilit d occurrence C est g n ralement suite cette analyse que le syst me est valid ou non Pa
98. a s gr gation entre quipements qui sont suppos s tomber en panne de fa on ind pendante comme par exemple les lignes jaune verte et bleue du syst me hydraulique Tous ces types d exigences peuvent tre valid es l aide des mod les g om triques 118 7 3 MODELISATION DE L ARCHITECTURE FONCTIONNELLE DU SYSTEME HYDRAULIQUE Fic 7 20 Mod le g om trique du syst me Hydraulique vue g n rale Blue RAT Blue EMP M A C Forward Yellow EMP Yellow HP Manifold Yellow reservoir AA Y Sy Yellow Priority valve Power transfer Unit Green EDP Green reservoir Green HP Manifold Green Priority valve Blue eee Fic 7 21 Repr sentation du syst me Hydraulique vue d taill e 119 CHAPITRE 7 SYSTEME HYDRAULIQUE D UN AVION DE TYPE A320 Une fois l ensemble des quipements et des connexions mod lis s il est possible d utiliser ce logiciel pour effectuer des analyses li es la s ret de fonctionnement En effet par des simulations d clate ment de pneu et ou de moteurs le logiciel permet de v rifier si l installation choisie est acceptable du point de vue des exigences de s ret de fonctionnement Les mod les g om triques d finis par IRIS permettent d identifier les l ments qui sont impact s par les diff rentes projections de d bris provenant de l explosion simul e En revanche IRIS ou les outils similaires comme CATIA ne permettent pas de d terminer s
99. aboration ordre en profondeur etc Ces ordres de pilotage sont ensuite directement envoy s aux commandes de vol CDVE En parall le le syst me SdT surveille en permanence la coh rence et le bon fonctionnement des ressources et des t ches et produit en cas d anomalie une alarme de d gagement calcul e par une 85 CHAPITRE 6 LE SYST ME DE SUIVI DE TERRAIN SDT D UN AVION DE CHASSE fonction d Elaboration d alarme de d gagement et renvoy e sur les diff rents contr les du pilote Haut parleur HP SdT cran de contr le Display SdT Image_Terrain Radar_SdT H pu ES A laboration Donn es_terrain P_SdT ordre terrain yZCC Elaboration Elaboration DOLONGI ordre_profondeur ordre limite de pente ordre en profondeur Elaboration new ordre alti S Navigation Test_TAC E 2 i Alarme TAC A gt NOV eisberg Bew HRS Alarme_son l i El i aboration aboration HP SdT ordre d gagement alarme d gagement Commande_degt Elaboration roulis consolid Alarme_visu Display_SdT FIG 6 3 Architecture fonctionnelle du Suivi de Terrain 6 2 2 Architecture mat rielle Le syst me SdT est un syst me distribu fonctionnant sur une architecture de type IMA Dans ce type d architecture les ressources de calcul et de communication sont partag es par les diff rentes fonctions du syst me L architecture du syst me est repr sent e par la figure 6
100. aded click on the button labeled lt CutSets a dialog window will appear that will let you select a safety assessment results file Click on the button labeled when the file is selected Then another dialog window will appear to select the file name for the geometrical cut sets Once this file is selected two geometrical cut sets files are generated one using the XML format described in section 1 2 and the other file contains the same geometrical cut sets in a text format If a_geo_name xml is the name of the geometric cut set file selected by the user then a_geo_name cat txt is the name of the geometric cut sets in text format 147 ANNEXE A MANUEL D UTILISATION DU MAPPINGMANAGER 2 12 Mapping Manager commands The mapping manager can be called using the following commands mapmanager option file_name option parameter option mp loads file_name as a mappings file option hll imports file name as the Left component list option hlr imports file name as the Right component list option traj if parameter 1 includes trajectory details in the generated failset else parameter 0 do not include trajectories details in the failset option fseti file name is the hit list file used to generate failsets option fseto file name is the failsets file option cseti file name is the cut set file used to generate geo cut sets option cseto file name is th
101. ae ga hee ea du Rubi 125 8 1 Transformation de mod les ADDL avec un mod le d erreur en r seaux de Petri 133 xiii xiv PREMIERE PARTIE INTRODUCTION AU DOMAINE CHAPITRE 1 INTRODUCTION 1 1 Contexte g n ral S curit et fiabilit des syst mes a ronautiques Le contexte applicatif dans lequel s inscrivent nos travaux est celui de la conception et la validation de syst mes avioniques ayant un r le critique dans le fonctionnement d un avion syst me hydraulique syst me lectrique syst me de gestion de vol etc Ces syst mes sont comme consid r s critiques du point de vue de la s curit aussi nomm e s curit innocuit dans Lap96 car leur dysfonctionnement est susceptible d avoir des cons quences catastrophiques sur les personnes l quipage les passagers ou les personnes au sol les biens l avion l a roport ou l environnement Une fois embarqu s dans les avions ces syst mes doivent galement pr senter une forte fiabilit qui selon Lap96 est d finie par l aptitude d un syst me assurer sa fonction pendant sa dur e de vie c est dire tout au long de la dur e d exploitation d un avion qui avoisine les 50 ans Bien s r certains composants de ces syst mes seront amen s tre remplac s en cas de panne du fait d usure mat rielle mais de mani re g n rale la plupart d entre eux seront maintenus tout au long de la vie d un avion Il est donc primordial que c
102. aleur de v rit est vraie d crivent les orien tations respecter pour construire l architecture mat rielle Afin de mieux repr senter le r sultat obtenu il est possible de visualiser cette allocation l aide d un outil d velopp dans ce travail La repr sentation de l allocation par l outil est donn e par la figure suivante 97 CHAPITRE 6 LE SYSTEME DE SUIVI DE TERRAIN SDT D UN AVION DE CHASSE x Allocation Viewer Taches Ressources Statistiques Nb Solutions 1 Independance 7 Voir les conflits All Solutions Divise J Ext Fic 6 8 AllocViewer pour la visualisation des r sultats Grace a cet outil il est possible de visualiser les allocations possibles une une afin de s lectionner celle qui poss de le plus d int r t pour le concepteur de l architecture En effet par l appui sur le bouton All Solution l outil retourne l ensemble des solutions ayant le m me crit re optimis Ensuite par des appuis successifs sur les fl ches l utilisateur peut parcourir les solutions cf figure 6 9 98 6 8 BILAN Allocation Viewer Allocation Viewer Taches Ressources Ressources mmm BE mu Statistiques Nb solutions 132 Statistiques Nb solutions 132 Independance 7 Independance 7 Voir les conflits Voir les conflits snae Ek 2 MUCH a Allocation 1 b Al
103. allocation 32 Mod le COMAMON Quorum bx SOE Aa E E 33 Comportements possibles des fonctions 33 Repr sentation du noeud Main du COM MON 39 Le composant Equal 22s os Raw ir dus Rep des Lama 3 36 Le composant Inberrup bd Ee oe 36 Exemple utilis pour l analyse du 36 Injection d une d faillance sur COM 37 Ressources mat rielles 38 Comportements possibles des ressources 39 Exemple d architecture mat rielle 40 Regroupements possibles de composants 40 Exemple de repr sentation d une ressource Al Exemple de connexion entre les ressources Al Les ressources de calcul simples lt 4 4 6 coop our ERE 41 Composant repr sentant une zone avion 42 Exemple de repr sentation d une zone 43 Repr sentation possible des zones d un avion 43 Premi re Architecture pour le COM MON 46 Une allocation possible pour le COM MON 46 Deuxi me Architecture pour le COM MON 47 Une allocation possible pour le COM MON
104. allocation doit conserver les connexions entre les fonctions En effet si lors de la mod lisation de l architecture fonctionnelle plusieurs fonctions sont amen es communiquer entre elles il faut qu une fois allou es elles puissent continuer le faire Pour cela il faut s assurer que lors de l allocation les ressources h bergeant les fonctions restent bien en connexion cf figure 4 4 f cenx FIG 4 4 Contrainte de connexion Pour permettre cela il faut supposer que la relation u_ cna respecte deux propri t s la tran sitivit et la r flexivit En effet lorsque plusieurs fonctions interconnect es sont allou es sur une m me ressource nous souhaitons pouvoir conserver la propri t de cette interconnexion Ainsi la propri t de r flexivit de u_cnx permet de sp cifier que Vr ER r r u_cnz cf figure 4 5 Ly 4 alloc r alloc Fic 4 5 u_cnz relation r flexive La propri t de transitivit permet d exprimer par une simple relation entre deux ressources le fait qu il existe un chemin entre ces deux ressources Un chemin correspond une route entre deux ressources en utilisant des connexions avec d autres ressources La transitivit de u_cnx signifie donc dans notre probl me que ri r2 u_cnz r2 3 Cu 71 73 cnc Vr1 72 7T3 ER 56 4 4 LES CONTRAINTES Fic 4 6 u_cnz fermeture transitive Ainsi
105. ance Le probl me d allocation consiste trouver la relation alloc tout en garantissant certaines exigences de s ret de fonctionnement Nous proposons d utiliser les techniques de validation des exigences vues dans la section 2 2 4 pour identifier les sc narios pertinents lors de la validation d un syst me L analyse de ces sc narios nous permet d identifier les fonctions qui doivent tre allou es sur des ressources diff rentes pour ne pas invalider les exigences Voyons en d tail les deux techniques d analyse de mod le AltaRica g n ration de s quences et model checking qui vont permettre d identifier les fonctions jouant un r le important du point de vue de la s ret de fonctionnement 5 1 1 Identification par analyse de sc narios Une premi re technique consiste utiliser le g n rateur de s quence cf section 2 2 4 afin de produire un ensemble de sc narios minimaux menant la situation redout e FC Partant d un ensemble de sc narios Sc compos de p sc narios Sc Ci C2 Ci Cp et connaissant le degr N de criticit de la situation redout e il faut identifier les fonctions qui ne doivent pas tre allou es sur une m me ressource Soit C un sc nario dans Sc compos de k v nements C evi ev2 eux C repr sente donc une s quence minimale menant la situation redout e FC tant donn que cette s quence est produite par l analyse du mod le de l architecture fonctionnelle
106. artenaire de Squash qui avec son short et sa gentillesse a su me donner envie de faire du th tre Quelques mots aussi pour remercier mes coll gues d APSYS qui dans les derniers mois de cette iii th se m ont encourag et permis de terminer dans de bonnes conditions Merci Nico Pierre S Pierre M Amandine Julien Xavier Alexis S bastien Fran ois et Val rie Je tiens galement remercier Jean pour sa confiance et la chance qu il m a donn en me permettant de travailler sur des sujets proches de ma th se Je tiens galement remercier ma famille Mon fr re pour m avoir accompagn et soutenu pour ma derni re preuve de vie de Th sard La soutenance Mes parents pour leur soutien je pense aux relectures courageuses de mon p re malgr son incompr hension du domaine et des moyens techniques d favorables au fin fond du Pays Basque et je pense la fiert de ma m re de me voir aller jusqu au bout Enfin je pense tr s fort mes grands parents Papou Mamette A taxi Amatxi qui de pr s ou de loin m ont toujours accompagn Je n oublie pas la famille Gaudan pour leur compr hension et leur soutien dans les deniers mois C est aussi gr ce eux que la soutenance a pu se d rouler dans les meilleures conditions possibles La derni re personne et non la moindre que je souhaite remercier de tout mon coeur est ma moiti Elle a su toutes ces ann es trouver les mots pour m encourager et me soutenir surtou
107. ations correspondantes newSpeed Lost_TFTA Ver ccComp i 4 Alarm intemp 1 Cum PI lost on dete ct err new lt FIG 6 7 Observateurs associ s aux situations redout es 6 5 Identification des ind pendances L outil Cecilia OCAS permet en plus de la mod lisation de g n rer les diff rents sc narios menant aux situations redout es cit es pr c demment Voyons plus en d tail les diff rents sc narios Pour la g n ration des sc narios menant aux situations redout es il ne faut ni consid rer les composants mat riels ni les composants fonctionnels repr sentant la communication les Bus car leur r le dans l architecture n intervient que pour simuler des d faillances mat rielles Or ce stade de l analyse nous ne souhaitons pas consid rer ce type de d faillances Nous souhaitons juste nous assurer que l architecture mod lis e respecte bien les exigences qualifi es CAT et MAJ pr d finies pr c demment 92 6 5 IDENTIFICATION DES INDEPENDANCES Il faut pr ciser que le syst me tudi est un syst me militaire qui n est pas soumis des exigences de s curit aussi lev es qu un avion civil Aussi il est commun ment admis de d grader d un cran le niveau des exigences de s curit Ceci signifie que l exigence militaire associ e une situation redout e class e Catastrophique est le taux de d faillance doit tre inf rieur 1077 par heure
108. aux Je tiens galement 4 remercier chaleureusement Alain Griffault pour ses conseils et l attention toute particuli re qu il a su me donner Sa gentillesse et sa disponibilit ont permis de minimiser la distance Bordeaux Toulouse Mes plus sinc res remerciements s adressent 4 Pierre Bieber sans qui cette th se n aurait vu le jour car il a initi ces travaux et m a donn la chance de travailler ces cot s et oui 3 ans partager le m me bureau Ses comp tences m ont toujours impressionn mais gr ce son attention sa p dagogie sa bonne humeur et surtout son optimisme il a r ussi transformer cette difficile preuve de th se en ann es inoubliables d excellents souvenirs ses c t s Il a su trouver les bons mots pour faire avancer les choses et dans les moments difficiles sa bonne humeur et son optimisme ont t d cisifs pour ma motivation Ses enseignements resteront grav s en moi qui resterai enrichi de ses explications de ses nombreux coups de crayon et dessins ind l biles Encore mille fois merci pour tout Pierre Comment parler de l ambiance de ce bureau sans penser tous les acteurs du d partement qui y ont particip Je pense Christel qui a toujours t de tr s bon conseil sa gentillesse sa bonne humeur et sa disponibilit m ont rendu beaucoup de service Son perfectionnisme tant redout par les th sards lors des r p titions est tellement constructif et enrichissant qu
109. b Pdisty fail_loss map Y rswvy EDP Yellow Y HP Distribution3 impacted Yellow Y HP EDP TConnection impacted Yellow vY Suction rsvy EDP impacted kl Current map G rsvg EDP A320 FXL Component rsvg fa A320 IRIS HitList Green G ox Mapping Manager Map_4320 rLeft A320 IRIS HitList Maps Right 4320 FXL Component Blue B HP Distribution21 impacted map B HP Distrib lI EDPg fail loss Blue B HP Distribution41 impacted map G EDP TConnection EDPy fail loss i ml I Add Remove gt FailSet Open Save Exit gt Failset button Once a mapping was defined or loaded click on the button labelled gt FailSet a dialog window will appear that will let you either select the files loaded in the Right or Left side as a hit list or select a hit list stored elsewhere Choose HitList File HitList file Y GO Dismiss Failset Hitlist selection dialog Click on the button labeled GO when the hit list is selected Then another dialog window will appear to select the file name for the failsets Once this file is selected the fail sets file is generated Notice that for the failset generation to work properly the value of the name attribute of the hitlist should match the value of the left or right attribute of the currently loaded mapping file 2 11 Generate Geometrical Cut Sets Once a mapping was defined or lo
110. bir une d faillance fail_close le rendant dans la position bloqu e ferm e Dans cette position il est impossible d interrompre le signal mis par COM mm mn update c fail_close Interrup closed stuck fail_close Fic 5 2 Nouveau comportement de Interrup Pour obtenir un tel comportement il suffit de remplacer le noeud AltaRica de l interrupteur actuel par le noeud suivant 1 node interrup 2 state 3 S iopen closed closed stuck 4 flow 5 correct error los re 6 lin e shin Sal Codes es ERROR 7 2190048 8 event 9 fail_close update 10 trans 11 Eq false amp S closed update gt S open 12 5 closed or S open fail_close gt S closed_stuck 13 assert 14 Out case 15 S open lost 16 else In 17 e 18 init 19 S closed 20 edon Apr s ces modifications du mod le il faut galement modifier la formalisation de la situation re dout e En effet lorsque les voies de calcul COM et MON produisent des donn es diff rentes alors 72 5 1 IDENTIFIER LES HYPOTHESES D IND PENDANCE Vinterrupteur n interrompt plus la fourniture de donn es instantan ment Ce n est qu apr s avoir jou la transition correspondant l v nement update que l interrupteur s ouvre Donc pendant un instant il est possible qu une donn e erron e soit propag e La nouvelle situation redout e que nous souhaitons consid rer
111. btenir un premier syst me r soudre sont celles identifi es pour respecter les ind pendances En effet les analyses pr c dentes ont permis de mettre en vidences plusieurs ind pendances entre fonctions 4 respecter pour tenir certaines de nos exigences La description du syst me identifie les ind pendances respecter par un ensemble de variables d finies comme suit idp_Fonction1_Fonction2 gt 1 Pour chaque couple de fonctions pr sentes dans une contrainte d ind pendance il faut s assurer que les deux fonctions du couple ne sont pas allou es sur une m me ressource Par exemple dans le cas de l ind pendance entre la fonction de calcul de l alarme de d gagement et la fonction de Navigation la variable permettant la description est la suivante idp_ClAlarmComp_Navigation gt 1 Les in quations qui en d coulent pour s assurer que la fonction de calcul de l alarme et la fonction Navigation ne sont pas allou es sur une m me ressource sont les suivantes en consid rant qu il existe trois ressources R1 R2 R3 alloc_ClAlarmComp_Ri alloc Navigation R1 idp_ClAlarmComp_Navigation alloc_ClAlarmComp_R2 alloc_Navigation_R2 idp_ClAlarmComp_Navigation alloc_ClAlarmComp_R3 alloc_Navigation_R3 idp_ClAlarmComp_Navigation Le syst me de contraintes est ensuite enrichi par l ensemble des contraintes d finies dans 4 4 et appliqu aux diff rentes variables du syst me pour c
112. c_COM_RM u_cnx_SM_RM lt 1 alloc_S1_SM alloc_COM_SC u_cnx_SM_SC lt 1 alloc S1 RM alloc_COM_SC u_cnx_RM_SC lt 1 Une fois le syst me d quations lin aires cr c d apr s r it ration des traductions sur l ensemble des fonctions il suffit d utiliser l outil SATZOO afin qu il nous propose une solution possible notre probl me d allocation Une allocation propos e par l outil SATZOO est la suivante u_cnx_RM_SC u_cnx_RM_SM alloc_COM_SC alloc_MON_SM alloc_S1_SC alloc_S2_SM alloc_Equals_RM alloc_Interrup_RM Cette allocation propos e peut facilement tre repr sent e par la figure 4 12 64 4 6 RESOLUTION DU SYSTEME DE CONTRAINTES Fic 4 12 Allocation propos e par SatZoo Cette allocation est tout fait acceptable car elle est identique celle valid e dans le chapitre pr c dent Cette d marche sera valid e sur le probl me de l allocation d un syst me de navigation Suivi de Terrain sur des ressources mat rielles d un avion militaire de type Dassault Mirage 2000 cf chapitre 6 4 6 1 Trop d allocations possibles Plus nous ajoutons de contraintes et plus l espace des solutions admissibles r tr cit Mais dans certains cas l ensemble des solutions acceptables reste trop grand Un des principaux avantages formaliser notre probl me d allocation en un probl me de satisfaction de contraintes est qu il est possible de sp cifier un crit
113. cng Correspondant aux connexions entre les ressources Consid rons par exemple le probl me d allocation de 4 fonctions fi fo f3 fa connect es comme d apr s la figure 4 8 sur un ensemble de 3 ressources suppos es interconnect es Fic 4 8 Exemple de probl me d allocation 59 CHAPITRE 4 RESOLUTION DE CONTRAINTES D ALLOCATION Il existe ici des connexions entre les fonctions fi avec fo fo avec fa et f4 avec fa La relation Seng correspondante cet exemple est la suivante f cena fi fe 21 f_cnx fa fa f_cnx fa fa L ensemble des variables bool ennes n cessaires est donc le suivant T Vy cena v_ f_cnx_f1_f2 v_f_cnx_f2_f3 v_f_cnx_f3_f4 Une fois toutes les variables identifi es il faut adapter nos diff rentes contraintes afin de construire notre syst me d quations lin aires 4 5 2 Des variables bool ennes vers des in quations lin aires Nous d finissons des lois de transformations trad applicables des formules en forme normale conjonctive c est dire de la forme N Clause o Clause V V Yn i 1 k pj est un litt ral Soit y une variable alors trad y vy Afin d valuer nos lois de transformation la comparaison des tables de v rit s av re n cessaire t variable e 1 vo 0 1 1 1 0 0 Ces deux colonnes tant identiques nous pouvons en d duire une premi re loi de transformation
114. ct file to import in left side Browse Select file to import in right side Browse MapManager Input Output Window MapManager Mapping File Name window The list of imported components should appear in the GUI 2 3 Create manually a mapping Once component lists are imported the definition of the mapping can start 142 W Mapping Manager 1 4 4 06 07 14 Mapping Manager 01 mapATA24 ATA27 ATA29 Left IRIS TA24 branch1095 15L GCUT to IDG1 impacted TA24 branch382 2P T RU APU to MPC impacte TA24 branch383 2P TRU APU to MPC impacte TA24 branch384 2P T RU APU to MPC impacte TA27 Rudder THS Control Cable impacted TA27 Rudder branchB80 15FC Rudder Servo Ctl TA27 Rudder branch687 1 MFC Rudder Servo Ctl TA27 Rudder branch693 2MF9 Rudder Servo Ctl TA27 Rudder branch 24 2MF3 Rudder S ervo CHl TA27 Rudder branch 26 2MF9 Rudder S ervo Ctl T 27 Rudder branch 37 25F 9 Rudder S ervo Ctl TA27 Rudder branch 38 25F Rudder Servo Ctl B TA27 Rudder branch 33 2MF Rudder S ervo Ctl E T 27 Rudder branch S5 2MF Rudder Servo Ctl E TA24 branch1 001 1M SODOVE to 235V4U 1M APL_4 Current m16 IRIS ATA27 Rudder branchEBS 2MFS OCAS RUDDER AT 27 D2 SVy fail QCAS RUDDER AT 27 D2 P3 fail Ic HYD_ATA29_D1 EDPg1 F HYD_ATA29_D1 EDPg2 f HYD_ATA29_D1 EDPy fa HYD_ATA29_D1 distb fall HYD_ATA29 D1 distg fail HYD ATA29 D1 disty fail Add re
115. ctions o f et f sont deux fonctions connect es tel que l orientation est de f vers f la traduction en AltaRica doit pr server la correspondance entre les flux entrants dans le composant f et les flux sortants du composant fi Wis fj f enm fi gt f FE pout En appliquant cette derni re r gle de transformation toutes les fonctions du syst me COM MON nous obtenons le code AltaRica correspondant au noeud global Main suivant 1 node Main 2 sub 3 COMES 4 ronca 5 EQU 6 7 assert 8 Interrup in com COM out 9 Camel Ieee 10 Equals in_com COM out 11 Equals in mom MON out 12 edon Lors de la lecture du code AltaRica du noeud Main nous remarquons que les composants Equals et Interrup ne sont pas d clar s comme fonct Ce choix est volontaire car ces 2 composants n ont pas le m me comportement qu une fonction de calcul lorsqu ils sont en pr sence de d faillances 1 Le composant Equals qui effectue la comparaison des donn es fournies par la fonction COM et la fonction MON n est pas sujet aux d faillances Nous supposons que cette comparaison s effectue toujours sans la pr sence d une d faillance Le comportement de ce composant est donc limit au signalement par un bool en de la diff rence de valeurs de ses deux entr es Le comportement de ce composant poss de une limitation en cas de pr sence
116. cture tudi e En effet suivant les choix d architecture certains calculateurs ne peuvent changer des donn es qu avec certaines ressources de communication l utilisation des proto coles varie suivant les d bits d informations et le type d information qui circule Ainsi les connexions des ressources de communication d pendent du nombre de ressources de calcul connect es Lors de la r alisation de l architecture il faut modifier le code AltaRica de chaque ressource de communication afin d y ajouter les bonnes connexions entrantes et sortantes des autres ressources connect es Prenons maintenant l exemple d une architecture permettant de supporter le syst me COM MON de la section pr c dente Elle est compos e de 2 ressources de communication Busi Bus2 et 4 ressources de calcul R4 Ra R3 R4 Consid rons que R produise certaines quantit s de donn es ne pouvant tre v hicul es que par une ressource de communication de haut d bit consid rons aussi que les 2 calculateurs et R4 doivent s changer des donn es afin de se partager le calcul d une t che importante et consid rons enfin que la ressource R2 permet de faire la liaison entre les donn es produites par R et celles produites par le couple Re Une telle architecture peut tre repr sent e par la figure suivante 39 CHAPITRE 3 MOD LISATION ET ANALYSE DE L ALLOCATION Fic 3 11 Exemple d architecture mat rielle Comme vu
117. d abord n cessaire de d finir l ensemble des l ments consid rer Dans notre exemple il faut identifier et mod liser le syst me hydraulique puis l ensemble des consommateurs critiques de la puissance qu il fournit les gouvernes etc ainsi que la puissance minimale suffisante pour chacun des consommateurs Une fois ces l ments caract ris s il est possible de formaliser une partie de l exigence qui est P Le syst me hydraulique fournit une puissance suffisante aux consommateurs critiques Pour exprimer formellement qu une propri t doit tre v rifi e par tous ou certains des tats accessibles d un syst me il est n cessaire de manipuler des ensembles d tats pour v rifier que chaque tat dans cet ensemble satisfait la propri t Les logiques temporelles permettent de manipuler ce type d ensembles Parmi elles nous en citerons trois 11 CHAPITRE 2 TECHNIQUES POUR LA MODELISATION ET LA VERIFICATION LTL Linear Temporal Logic Pnu77 permettant d expri mer des propri t s devant tre satisfaites par les diff rents tats accessibles d un syst me au cours d une volution O 0 9 9 J du syst me donn e sur un chemin donn repr sentant les tats successifs du syst me comme illustr par la figure ci contre Par exemple on peut exprimer les propri t s du type d s que le syst me tombe en panne une alarme doit le signaler Plus g n ralement les propri t
118. dans la figure les connections entres les diff rentes ressources sont consid r es comme bi directionnelles c d qu une ressource ne se contente pas d crire sur la ressource mise sa disposition pour communiquer elle doit aussi pouvoir lire des donn es circulant sur cette derni re L analyse de cette architecture permet d identifier certains regroupements de ressources ayant le m me comportement et par cons quent le m me code AltaRica Ainsi R et R4 peuvent tre regroup es car elles poss dent chacune une seule connexion vers une ressource de communication Ro peuvent elles aussi tre regroup es car elles sont toutes les deux connect es deux autres ressources Les ressources de communications Bus et Busz quant elles peuvent tre regroup es car elles poss dent trois connexions avec d autres ressources Fic 3 12 Regroupements possibles de composants Ainsi seulement trois noeuds AltaRica suffisent pour mod liser cet exemple Partant du compor tement g n rique d fini pr c demment on peut en d duire le code de chaque groupe Le premier groupe G1 est compos de deux ressources de calcul identiques ne poss dant qu une entr e sortie vers une autre ressource Il suffit donc de lui ajouter le comportement souhait de ses sorties en fonction de l tat interne du composant Toujours dans l id e d associer chaque composant un comportement g n rique il faut sp cifier que chaque compo
119. de dans la g n ration de s quence sur des mod les de grande taille Le temps d obtention des diff rentes s quences augmente proportionnellement avec la taille du mod le et exponentiellement par rapport la profondeur du parcours r aliser profondeur d finie par la borne associ e la g n ration Tho06 26 2 2 MODELISATION ET VERIFICATION DE LA SECURITE DES SYSTEMES AERONAUTIQUES Les outils disponibles pour les mod les AltaRica Les outils Cecilia OCAS et SIMFIA tant principalement d di s des analyses de s ret de fonc tionnement ils int grent des modules permettant Une simulation pas pas 5 04 des d faillances du syst me Tout v nement du syst me peut tre tir individuellement ou par regroupement et les diff rents impacts sont directement visibles sur le mod le La simulation permet de v rifier que le syst me que nous mod lisons poss de le bon comportement Un g n rateur automatique d arbre de d faillances Rau02 qualifi pour la certification de syst mes a ronautiques Les arbres ainsi obtenus peuvent ensuite tre utilis s par d autres outils sp cialis s pour le calcul de probabilit s Aralia etc sachant que dans ce cas nous ne nous int ressons pas l ordre d apparition des d faillances Un g n ration de s quence sous forme de coupes minimales En effet lorsque la dynamique du syst me n autorise plus la g n ration d arbres le syst me e
120. de la premi re sous contrainte en in quation suffit pour identifier la deuxi me in quation correspondante coloc f1 f2 alloc fi r alloc f2 r coloc fi f2 V alloc f1 r V alloc f2 vrai 1 coloc fi fa 1 alloc fi r alloc f2 r gt 1 2 coloc fi f2 1 alloc fi T alloc fo r gt 1 coloc fi fa alloc fi r alloc f2 r 1 0 61 CHAPITRE 4 RESOLUTION DE CONTRAINTES D ALLOCATION Ainsi les contraintes satisfaire sont coloc f f2 alloc f1 r alloc f2 r lt 1 Vi f F Vr ER coloc fi f2 alloc f2 r alloc fi r lt 1 3 ind pendance 4 6 Vio fj E F Yr E R alloc fi r alloc f r idpt fi fj lt 2 4 6 R solution du syst me de contraintes Le nombre de contraintes et de variables d pend du nombre de composants utilis s dans les archi tectures fonctionnelle et mat rielle Or plus le nombre de variables est grand plus la satisfaction de contraintes peut prendre du temps et plus la solution s av re difficile trouver En raison du probl me d explosion combinatoire d au fait que le probl me appartient la classe des probl mes NP complet Coo71 il est pr f rable de limiter le nombre de variables mais aussi le nombre de contraintes pour obtenir une allocation possible Ainsi les contraintes sur les diff rents choix d allocation imposer ou interdire l allocation d une fonc tion sur une ressource s
121. de ressources et les modifications effectuer sont guid es par les conflits de ressources associ s Ce nouveau crit re s crit donc Vr R c min y con flit r Approche incr mentale Les variables de conflits permettent donc de trouver une allocation malgr le non respect de certaines contraintes L ajout de ces variables et le changement du crit re d optimi sation permettent d identifier rapidement les ressources ne respectant pas les contraintes Une m thode a t d velopp e afin de combiner la recherche d allocation et lorsque cette recherche ne fournit pas de r sultat l identification des ressources posant probl me Cette technique permet d automatiser le processus d obtention d une premi re allocation possible Elle consiste rechercher progressivement l allocation en modifiant lorsque cela s av re n cessaire l architecture propos e La d marche propos e peut tre synth tis e par le diagramme de la figure 5 6 Partant d une des cription de l architecture et d un ensemble de directives il est possible de construire le syst me de contraintes correspondant Lorsqu il n existe pas d allocation il suffit d analyser les conflits pour iden tifier les ressources posant probl me dans l architecture Une solution de remplacement de la ressource posant probl me par deux nouvelles ressources permet de modifier l architecture et de relancer les analyses la recherche d une allocation possible 78 5 3
122. de ses cat gories la standardisation du langage associe une ic ne permettant une repr sentation normalis e des diff rents composants d un syst me 3 Architecture Analysis and Design Language Society of Automotive Engineers 14 2 2 MOD LISATION ET VERIFICATION DE LA S CURIT DES SYST MES AERONAUTIQUES cat gories logicielles cat gories processor Memory device cat gorie composite FIG 2 1 repr sentation graphique des composants AADL Chaque composant AADL a deux niveaux de description le type et l impl mentation Le type component types correspond l interface fonctionnelle du composant il d crit comment le composant est visible par l environnement c d quelles sont ses propri t s et caract ristiques L impl mentation component implementations correspond la structure du composant en terme de sous composants connexions et modes op rationnels plusieurs impl mentations peuvent tre associ es un m me type chaque composant on peut associer des propri t s et leur donner des valeurs Celles ci permettent de caract riser le composant Certaines propri t s sont pr d finies elles sont identifi es par un nom un type et la liste des cat gories de composants sur lesquelles elles s appliquent Par exemple les t ches thread disposent de propri t s temps r el telles que la p riode l ch ance ou la dur e d ex cution L interconnexion ent
123. des avantages quivalents lorsque nous nous int ressons la s ret de fonctionnement l approche AADL repr sente l alternative la plus s duisante mais il reste encore am liorer les outils supportant les analyses de s ret de fonctionnement pour atteindre le niveau d AltaRica Un grand avantage d AADL est qu il permet de traiter d autre point de vue que la s ret de fonctionnement comme les performances temps r el Ceci dit AADL reste confin la mod lisation des syst mes informatiques Ce qui n est pas satisfaisant lorsqu on s int resse des probl mes d allocation de syst mes h t rog nes lectriques hydrauliques commandes de vol sur les quipements de l avion 8 3 Perspectives Dans cette section nous dressons un bref aper u d un ensemble de perspectives que nous avons identifi es Nous commengons par une perspective technique d am lioration de notre m thode de r so lution de contrainte Nous pr sentons ensuite les perspectives d exploitation de nos travaux avant de pr senter une perspective g n rale de nos travaux 134 8 3 PERSPECTIVES 8 3 1 Utiliser l existant Une premi re perspective de travail pr sent consiste int grer l approche dans le processus de d veloppement existant En particulier les techniques de mod lisation et de v rification de l allocation permettent d assister les analystes de type CCA comme les analyses de risque particulier clatement pneu moteur
124. dire certaines ressources n ayant pas les caract ristiques suffisantes pour ex cuter certaines fonctions 58 4 5 TRANSFORMATION DU MODELE CSP EN SYSTEME D EQUATIONS LINEAIRES La contrainte permettant l exclusion de certaines fonctions sur des ressources est exactement l oppos de la contrainte de la pr c dente et s crit de la fa on suivante alloc ta ra 0 5 Ind pendance f ne doit pas tre allou e sur la m me ressource que fa Cette contrainte traite l ind pendance de deux fonctions Deux fonctions sont consid r es comme ind pendantes lorsqu elles ne doivent pas se retrou ver allou es sur une m me ressource Cette ind pendance est n cessaire afin de respecter certaines exigences de s ret de fonctionnement Sachant que ces exigences visent contr ler le nombre de pannes menant une situation redout e lorsque celle ci concerne une panne simple il ne faut pas qu une seule d faillance sur une ressource impacte plusieurs fonctions et par cons quent invalide l exigence D o l importance de respecter l ind pendance lorsqu elle est clairement identifi e et d isoler certaines fonctions importantes pour le syst me La contrainte correspondante pour emp cher l allocation de deux fonctions ind pendantes sur une m me ressource est la suivante Vf f2 F Vr ER idpt fi fo gt alloc fi r alloc f2 r 4 6 4 5 Transformation du mod le CSP en syst me d quations lin
125. distg fm fail loss zone LeftWing gt lt fail mode component EDPy fm fail loss zone RightWing gt lt failmodes gt To automatically create mapping suggestions click on the automatic mapping button a window should appear that asks for the attribute to use to group components Select an attribute in the list and click on the Go button 145 ANNEXE A MANUEL D UTILISATION DU MAPPINGMANAGER Automatic Mapping 1 Mapping hints map components with same attribute zone ja Selection of an attribute for Automatic mapping suggestion A list of created mappings appears in the mapping list area for each value V of the attribute a mapping map_v is created Mapping Manager r Mapping Manager mapZone Right 3320 f zone EDPa fail loss mapp FrontCargo mapp Wheelw ell New RATb fail loss ptu eq fail loss Auto rsvb fail loss Current mapp_Rightwing 320 zone EDPy fail loss 320 f l zone NPdisty fail loss 320 f zone Pdisty fail loss 3320 fl zone PDistb fail loss F Automatically created mapping 2 10 Generate Fail Sets 146 A AAA A Green G HP Distribution 2 impacted map_G HP Distrib EDPy fail_loss Green G HP Distribution 3 impacted map_G rsvg EDP sd Pdistb fail_loss Green G HP EDP TConnection impacted map_Y EDP Connection Pdistg fail_loss map_Y HP Distri
126. donn e ces logiciels fournissent la liste compl te des quipements pr sents dans ce c ne de d bris Les l ments int ressants dans ces analyses sont les composants impact s mais aussi le degr d impact de ces derniers En effet les quipements impact s poss dent des degr s diff rents d impact suivant la distance qui les s pare de l explosion Certains seront compl tement d truits alors que d autres n auront qu une l g re d t rioration qui ne g nera pas son fonctionnement mais qui emp chera de garantir un fonctionnement parfait de l quipement Pour standardiser l importation d une liste d l ments impact s produite par diff rents outils d ana lyse nous avons impos le choix d un formalisme Une liste d l ments impact s Hitlist doit tre re pr sent e par son nom et une liste des analyses effectu es Chaque l ment de cette liste hitlistitem doit correspondre une tude d un certain clatement d crit par 121 CHAPITRE 7 SYSTEME HYDRAULIQUE D UN AVION DE TYPE A320 le type d analyse d termin par exemple par le nom de l l ment qui va exploser un clatement d un des pneus de l avion ou d un des moteurs les quipements qui sont impact s ainsi que le degr de leur d t rioration les diff rentes trajectoires associ es aux impacts Prenons un exemple pour illustrer une Hitlist lt hitlist name Geometrical_with_IRIS description A32
127. donn es repr sentent des valeurs r elles calcul es par des fonctions ou fournies par les capteurs Par exemple le radioaltim tre permet de d terminer la position de l avion par rapport au sol Cette donn e repr sentant l altitude doit tre la plus pr cise possible afin d effectuer les bons rep rages du terrain pour permettre en cas d activation du pilotage automatique de maintenir l avion l altitude la plus basse possible tant donn que l analyse que nous souhaitons effectuer sur ce syst me est orient e sur le comportement global du syst me en pr sence de d faillances nous ne consid rons pas la valeur r elle de cette donn e d altitude mais uniquement une valeur abstraite d notant l occurrence d une d faillance en amont dans la chaine de traitement de cette donn e Une premi re abstraction n cessaire pour la mod lisation de ce syst me concerne les donn es chang es Pour nos analyses nous consid rons trois types de valeur d not s par la figure 6 3 1 correct Cette valeur permet de repr senter l ensemble des donn es n ayant pas subi de d faillance et dont la valeur r elle appartient l intervalle de valeurs pour d un fonctionnement correct erroneous En cas d occurrence d une d faillance dans les fonctions n cessaires la production d une donn e nous consid rons que la donn e est influenc e par cette d faillance et nous suppo sons par exemple que le comportement erron de la
128. du possible de poser le probl me de collision entre les d bris d un pneu ou d un moteur et des quipements sous la forme d un probl me de contraintes Mais il s agirait de domaines de contraintes par exemple des quations lin aires avec solutions r elles qui s loignent des techniques pr sent es dans les chapitres 4 et 5 Il semble qu il serait possible d appliquer notre approche mais avec une mod lisation g om trique plus abstraite que celle r alis e aujourd hui l aide d outils comme CATIA ou IRIS Il s agirait d un mod le d installation sous la forme d un graphe des zones de l avion et des routes interconnectant ces zones Cette id e a t soumise plusieurs partenaires industriels qui l ont jug e int ressante mais nous n avons pas pu obtenir d informations pr cises sur les zones et les chemins de c bles qu il serait pertinent d utiliser dans un tel mod le 130 m CHAPITRE 8 CONCLUSION 8 1 Bilan des travaux effectu s Dans nos travaux nous avons tout d abord montr que le langage AltaRica pr sente une expressivit suffisante pour mod liser des syst mes bas s sur des architectures fonctionnelles et physiques Ce langage dispose d un ensemble de concepts permettant la d finition et l analyse de l allocation de fonctions sur des composants physiques C est notamment la construction sync de synchronisation qui permet ais ment de d finir une allocation dans un mod le AltaRica la synchronisation perme
129. du syst me de suivi de terrain SdT adl00 est de permettre d laborer un pilotage automatique ou manuel dans le plan vertical selon le choix du pilote influenc par les conditions m t orologiques partir des informations de terrain fournies par le Radar et le pilote pr alablement enregistr es et des informations de navigation fournies par les diff rents capteurs au cours du vol La propri t principale de ce pilotage est de permettre le franchissement des diff rents obstacles du terrain tr s basse altitude minimum 60m en maintenant un haut niveau de s curit Ce mode de vol basse altitude permet de rendre l avion le moins d tectable possible altitude a time FIG 6 1 Illustration du Suivi de Terrain Ce SdT peut provoquer en cas de situation de vol critique un ordre de d gagement permettant une mont e tr s rapide de l avion par rapport sa derni re position fournie par les capteurs Ainsi il est primordial d assurer que les informations utilis es pour ce d gagement d terminent correctement la position de l avion afin de donner une bonne orientation ce d gagement Selon l approche CARLIT le SdT est d fini par un ensemble de cha nes fonctionnelles associ es un certain mode Ces cha nes fonctionnelles sont constitu es par des fonctions reli es entre elles par des changes d informations Chaque fonction intervenant dans les cha nes du SdT est pr alablement sp cifi e ind
130. e tape 4 La figure 7 18 montre l effet sur le r servoir de la ligne verte de la fuite du consommateur AltBrake En effet la fuite se propage travers le PTU de la ligne jaune vers la ligne verte apr s l v nement rsvg update le r servoir de la ligne verte commence baisser mais comme il n est pas totalement vide les consommateurs des lignes jaune et verte sont toujours aliment s en puissance hydraulique 115 CHAPITRE 7 SYSTEME HYDRAULIQUE D UN AVION DE TYPE A320 engl ng4 ESV DP g EDP LandingGear SlatsFlaps le rsvEDPy EDPy EA 2 RevEng2 spoiler2 piy elevatorR er NPdisty spoilera Fic 7 18 Sc nario de perte des lignes Jaune et Verte tape 5 La figure 7 19 montre l effet final de la fuite du consommateur AltBrake la perte des lignes verte et jaune Apr s l v nement rsvg update le r servoir de la ligne verte est vide donc les consommateurs des lignes jaune et verte ne sont plus aliment s en puissance hydraulique et apr s l v nement PTU update le PTU se d sactive mais cela n a plus d effet sur les consommateurs engl NPdistg mg mus NormB LandingGear T Revi YauDa Fla d Rud PA stabilizery poi YanDemperz stabi Revingz T elev Pdisty 8 Flaps 19 z spoilerz d spoi Yd AltBrake f elevatorR spoilera d Flaps Fic 7 19 Sc nario de perte des lign
131. e afin de d terminer si cela conduit une des situations redout es identifi es Parmi les diff rents langages de mod lisation existants nous avons choisi de ne pr senter que les langages qui ont t utilis s pour la v rification de propri t s de s curit Nous ferons donc une br ve pr sentation des langages AADL pour la description des syst mes des r seaux de Petri pour la simula tion des syst mes dynamiques du langage associ au model checker SMV et enfin du langage AltaRica qui permet la g n ration automatique d arbres de d faillances Le Langage AADL AADL 3 FLV03 FGH06 Lew06 a t con u pour permettre la conception et l analyse de syst mes complexes critiques temps r el dans les domaines de l avionique l automobile et le spatial Ce langage est en cours de standardisation sous l autorit du SAE dont une premi re version stable AADL 1 0 a t publi en novembre 2004 Langage de description Le langage AADL V1 permet de d crire comment les composants sont combin s en sous syst mes et comment ils interagissent entre eux Les architectures sont d crites de mani re hi rarchique Les composants sont les briques de base des architectures AADL Ils sont group s en trois cat gories 1 logicielle processus sous programme donn e fil d ex cution thread groupe de fils d ex cution 2 plate forme processeur m moire dispositif bus 3 composite syst me chacune
132. e se r alise ou non 16 2 2 MOD LISATION ET VERIFICATION DE LA S CURIT DES SYST MES AERONAUTIQUES Ch Fic 2 3 Exemple de franchissement de transitions d un r seau de Petri P T SMV Le langage SMV McM98 est un langage de description l origine con u pour la v rification de syst mes mat riels BC M90 Il permet de d crire les syst mes de mani re modulaire et hi rarchique Les syst mes manipul s sont d crits par des ensembles finis d tats Globalement le langage SMV permet de d crire le mod le l aide de d clarations de types de signaux s quences infinies d un type donn d affectations de modules types structur s etc de conditions et de boucles loop etc les propri t s que le mod le doit satisfaire formalis es l aide d expressions logiques d assertions exprim es avec la logique CTL ou LTL EH82 Le formalisme du langage SMV est proche de celui d AltaRica pour les types communs Une passerelle permettant de transformer des mod les AltaRica vers des mod les SMV existe et permet de b n ficier des outils d analyse de mod les SMV aux mod les AltaRica Voyons pr sent les diff rents types d analyses de syst me qui sont disponibles sur des mod les SMV Tout d abord il est possible d effectuer des v rifications formelles compositionnelles de propri t s par preuve Le principe de la v rification compositionnelle est assez simple il consiste lorsqu un
133. e geo cut sets file 148 Bibliographie 47696 ABC94 ad100 Air96 Air00 APGROO AWO5 BAK04 BBC 08 BCMD90 BLED99 BMT99 BR94 Bry86 BV06 BV 03 CCGRO0 ARP 4761 Guidelines and methods for conducting the safety assessment process on civil airborne systems and equipement Aerospace Recommended Practice SAE 1996 A ARNOLD D B GAY ET CRUBILLE Construction and analysis of transition systems with MEC World Scientific 1994 ARM E DE L AIR Mirage 2000d Suivi de terrain Rapport Technique Arm e de l air 2000 AIRBUS ABD200 Requirements and Guidelines for the systems designers 1996 AIRBUS IRIS Basic 3D Design User s Manual 2000 A ARNOLD POINT A GRIFFAULT ET A RAUZY The altarica formalism for describing concurrent systems Fundamenta Informaticae 40 109 124 2000 AADL WGL AADL Error Model Annex 2005 C BETOUS ALMEIDA ET K KANOUN Construction and stepwise refinement of de pendability models Performance Evaluation 56 1 4 277 306 2004 P BIEBER J P BODEVEIX C CASTEL D DOOSE M FILALI F MINOT ET PRALET Constraint based design of avionics platform preliminary design explora tion Dans ERTS08 2008 J R Burcu E M CLARKE K L MCMILLAN ET D L DILL Sequential circuit verification using symbolic model checking Dans DAC pages 46 51 1990 N BLACKWELL S LEINSTER EVANS ET S DAWKINS Developing sa
134. e le nom du composant impact le champ fm donne le nom de la d faillance qui est associ e au composant le champ world indique le monde d o provient le composant Les mondes possibles sont le monde fonctionnel Functional et le monde g om trique Geometrical Tous les attributs optionnels trouv s dans la liste des composants au moment de l importation dans l outil sont ajout s automatiquement dans le fichier mapping name A320 Hydraulic Light erate right Functional gt lt map name Yellow Engine Driven Pump gt lt failmode world Functional component EDPy internal MA320 Hyd EDPy description Yellow Engine Driven Pump gt lt failmode world Geometrical component Y EDP fm impacted description Yellow Engine Driven Pump gt lt map gt lt map name Blue Non Priority Distribution gt lt failmode world Functional component NPdistb ioa P description Blue Priority Distribution line gt lt failmode world Functional component CSMG fm fail_leakage description CSMG consumer gt lt failmode world Functional component Slats fm fail_leakage description Slat consumer gt lt failmode world Geometrical component B HP distribution 1 fm impacted description Blue High Pressure Distrib line part1 gt 126 7 5 VERIFICATION DE L ALLOCATION SPATIALE lt failmode world Geometrical component B H
135. e ms Correct 17 and not pre_0ut correct update gt pre_Out correct 18 assert 19 Out pre_0ut 2 edon 6 3 2 Mod le d architecture mat rielle Nous ne d taillons pas le mod le d architecture mat rielle qui est r alis selon les principes d crits dans le chapitre 3 6 4 Exigences de s ret de fonctionnement du SDT Les diff rentes d faillances consid r es sur les composants de ce syst me peuvent lorsqu elles sont combin es entra ner la perte du contr le de l appareil Dans cette situation il est permis au pilote de reprendre le contr le de son appareil afin d viter le crash Pour que tout se d roule correctement il est imp ratif que le pilote puisse conna tre l tat de son syst me pour ainsi d celer d ventuels dysfonctionnements Ainsi partant de ces suppositions diff rentes exigences sont d riv es pour que les missions puissent se d rouler sans probl mes Les exigences consid r es sont r parties suivant leurs degr s de criticit Exigences Catastrophiques Pitch erron non d tect Nous nous int resserons l absence d alarme en cas de Pitch erron Cette situation est tr s critique car en mode de pilotage automatique cette alarme est le seul moyen d viter un crash Le pilote doit toujours tre inform de l tat du SDT car en cas de d faillance dans le syst me il doit pouvoir reprendre le pilotage pour s curiser l appareil L
136. e syst me Comme la puissance transitant dans les connexions varie suivant la pression du fluide dans ces connexions il faut informer les composants connect s de la pr sence d une fuite Par exemple en cas de pr sence de fuite l information doit parvenir la source du fluide pour mod liser la baisse de niveau de fluide De m me que pr c demment cette caract ristique est repr sent e par un bool en vrai en cas de pr sence d une fuite et faux dans le cas inverse 105 CHAPITRE 7 SYSTEME HYDRAULIQUE D UN AVION DE TYPE A320 Fluid Leak Fic 7 3 Mod lisation des informations circulant dans le syst me Pour la suite de la mod lisation nous consid rons que le sens dans lequel le fluide est amen se d placer repr sente le sens normal nom et inversement le sens permettant de caract riser une fuite leak sur la figure 7 3 repr sente le sens inverse inv La mod lisation d une telle information en AltaRica passe par la cr ation d un nouveau type Ce type permet lorsqu il est associ un port de connexion d un composant de manipuler les deux sens tout en utilisant qu une seule connexion En effet si nous consid rons par exemple un composant n ayant qu une seule connexion 0 et que cette derni re repr sente une production de fluide alors le sens normal de la connexion repr sente l information de pr sence de fluide et le sens inverse repr sente l information de pr sence d une fuite gt
137. e une abstraction des diff rentes zones d un avion pour n obtenir qu un graphe d crivant l agencement des zones Consid rons qu une zone d un avion soit repr sent e par un cube Les diff rentes faces de ce cube repr sentent les diff rentes connexions possibles avec les autres zones Ainsi comme illustr dans la figure 3 16 les noms des faces expriment les positions possibles des zones adjacentes Partant de cette consid ration une mise plat de ce cube est possible en prenant quatre faces comme les quatre c t s du carr avec en plus deux connexions au niveau de deux coins North Up lt gt gt West East Down South FIG 3 16 Composant repr sentant une zone avion Cette mod lisation par un graphe des zones d un avion permet d appliquer notre technique sur le probl me de l allocation spatiale En effet partant de ce graphe il est possible de le consid rer comme une architecture mat rielle Ce graphe permet de r soudre le probl me de placement des quipements dans un avion et donc consid rer le probl me comme un probl me d allocation d quipements sur des zones de l avion Le comportement AltaRica repr sente les d faillances associ es une zone de l avion comme l impact d un d bris de pneu ou de r acteur qui conduisent la perte des quipements plac s dans cette zone ou comme l agression lectromagn tique qui va corrompre les donn es transmises ou stock es par les quipements positi
138. e v ri fication d une propri t sur le syst me global est jug e trop compliqu e la d composer en v rification sur les sous syst mes moins complexes qui la composent De plus afin de v rifier une propri t il est possible d avoir recours des hypoth ses assumptions exprim es par le mot clef assume Cela peut grandement faciliter une preuve mais cela demeure un m canisme dangereux s il est utilis tort ce qui est le cas par exemple lorsque les hypoth ses ne sont pas coh rentes entre elles Un autre type d analyse est la v rification du raffinement d un mod le y a raffinement d un mod le lorsque depuis un premier mod le abstrait d crivant un syst me un second mod le plus d taill est d riv d crivant le m me syst me La difficult r side dans la coh rence entre les diff rents mod les du m me syst me et dans la pr servation des bonnes propri t s Pour garantir la coh rence entre plusieurs mod les d crivant un m me syst me le langage SMV propose d utiliser un refinement maps appel invariant de collage en langage Cle07 Il permet de d crire la correspondance entre les propri t s exprim es sur les diff rents mod les concern s Langage AltaRica AltaRica est un langage cr par le Laboratoire Bordelais de Recherche en Informatique LaBRI au milieu des ann es 90 APGROO Poi00 PR99 Ce langage formel est n de la volont d industriels et de chercheurs d tablir d
139. e validante Cela permet d viter de remettre en cause l ensemble d une architecture donn e ce qui est favorable la r utilisation et l adaptation d architectures d un avion l autre Lorsqu il n existe pas d allocation possible pour une architecture donn e le syst me d quations lin aires d crivant les contraintes n a pas de solution nous avons labor une m thode permettant d identifier dans l architecture propos e la ou les ressource s modifier pour obtenir une bonne allocation Deux configurations peuvent rendre impossible la d finition d une allocation conforme aux contraintes 1 un syst me de contraintes impossible r soudre 2 une architecture mat rielle incompatible avec les contraintes Pour se pr munir du premier cas il est n cessaire de v rifier la coh rence de l ensemble des contraintes Dans le second cas il est n cessaire de modifier l architecture mat rielle pour la rendre compatible des exigences du syst me Nous nous int ressons ici ce second cas dans lequel l architecture mat rielle propos e ne poss de pas suffisamment d quipements pour permettre une allocation correcte Nous souhaitons donc pouvoir identifier dans l architecture les types de ressources dont le nombre est insuffisant Pour faciliter cette identification nous ajoutons notre syst me de nouvelles variables pour rep rer les conflits dans l architecture que nous d finissons ci apr s Un conflit sur une
140. ensemble des tats d un automate les transitions existantes entre ces tats et les contraintes de franchissement associ es pour ce qui est des r seaux de Petri il s agit de d finir l ensemble des places du r seau ainsi que toutes les transitions puis enfin le marquage initial des places La v rification d une propri t sur un syst me mod lis ne peut bien s r porter que sur les in formations contenues dans le mod le au travers des l ments qui le composent et sur la dynamique du syst me mod lis Il est donc important de conna tre tout d abord le type de propri t s que l on souhaite v rifier sur un syst me avant de pouvoir choisir un moyen de mod lisation permettant de repr senter toutes les caract ristiques du syst me impactant la satisfaction de la propri t 2 1 2 Expression des exigences que le mod le doit v rifier D finir une exigence ou propri t qu un syst me doit satisfaire consiste tout d abord exprimer en langage naturel cette exigence Il peut s agir par exemple dans le cas d un syst me hydraulique d avion de l exigence suivante le syst me hydraulique doit toujours fournir une puissance suffisante ses consommateurs identifi s comme critiques Cette exigence d finie en langage naturel doit tre formalis e et pr cis e pour pouvoir tre v rifi e de mani re automatique sur un mod le Il s agit d exprimer l exigence de mani re logique Il est tout
141. ent d un r servoir 107 7 8 Automate du comportement d une pompe 108 7 9 Automate du comportement d un consommateur 109 Lis ee he NL Re E E E ea eut di dede eu 109 7 11 Comportement du en cas d activation Al 110 7 12 Mod lisation du syst me Hydraulique avec OCAS 111 7 13 Observateurs associ s aux situations redout es 113 7 14 Sc nario de perte des lignes Jaune et Verte tape 1 114 7 15 Sc nario de perte des lignes Jaune et Verte tape 2 114 7 16 Sc nario de perte des lignes Jaune et Verte tape 3 115 7 17 Sc nario de perte des lignes Jaune et Verte tape 4 115 7 18 Sc nario de perte des lignes Jaune et Verte tape 5 116 7 19 Sc nario de perte des lignes Jaune et Verte tape 6 116 7 20 Mod le g om trique du syst me Hydraulique vue g n rale 119 7 21 Repr sentation du syst me Hydraulique vue d taill e 119 7 22 Repr sentation du syst me Hydraulique par IRIS 120 7 23 Analyse d un clatement pneu suivant l angle K 121 7 24 Analyse d un clatement pneu suivant l angle theta 121 7 20 Interface du MlappingManager oos s soti us 9 mom e
142. ents synchronis s En effet ce nouvel v nement effectue un broadcast sur tous les v nements pr sents dans la synchronisation c d que ce nouvel v nement va se substituer chaque v nement pr sent dans la synchronisation et lorsque la garde le permet il va s appliquer Voyons pr sent le comportement d une telle synchronisation Pour cela prenons l exemple de trois t ches Fx1 1 Fx1 2 Fx1_3 allou es sur une m me ressource Ress Le comportement souhait d une telle allocation est que la perte de la ressource engendre la perte des trois t ches Pour cela une premi re synchronisation introduit un nouvel v nement de type broadcast Frl_ fail permettant de repr senter la perte simultan e des t ches concern es En effet cet v nement s applique toutes les t ches allou es mais ne tre doit tir que lorsque ces derni res l autorisent lorsque les gardes permettent cet v nement Sachant que les diff rentes taches allou es ne sont pas toujours actives cette forme de synchronisation permet d appliquer les d faillances seulement aux t ches actives Une seconde synchronisation doit tre ajout e pour cette fois ci simuler la perte de la ressource ainsi que l ensemble de ses taches qui y sont allou es cette nouvelle d faillance est nomm e alloc fail Contrairement la synchronisation pr c dente celle ci doit imp rativement changer l tat de la res source lorsque q
143. eraient erron es Cette d faillance correspond dans la r alit une erreur sur quelques bits des donn es lors d une transmission De plus cette d faillance n est pas n cessairement permanente Une perte compl te de la ressource due une d faillance comme par exemple une coupure du c ble n cessaire la transmission entra ne l interruption totale de la communication Une ressource de calcul fig 3 9 b permet d ex cuter les diff rentes t ches du syst me Tout comme la ressource de communication cette ressource peut subir des d faillances Nous consid rons deux d faillances possibles Une d faillance pour exprimer une erreur intempestive du calculateur c d que durant un laps de temps tr s court le calculateur va produire une donn e erron e Ces d faillances peuvent apparaitre lorsque les calculateurs sont amen s ex cuter plusieurs t ches en parall le Une d faillance permanente permettant de mod lisation la perte totale de la ressource La perte totale d un calculateur correspond par exemple la perte de l alimentation n cessaire la res source Il est certain que si la ressource n est plus aliment e alors elle est dans l incapacit d ex cuter une t che Ainsi chaque composant repr sentant une ressource mat rielle pr sente deux types de d faillances fail error et fail lost Ces d faillances permettent de mod liser les pannes qui nous int ressent savoir la d failla
144. es Jaune et Verte tape 6 Le probl me r side dans la mauvaise activation du PTU lors d une fuite d une des deux lignes jaune ou verte Il faudrait doter le PTU d un capteur permettant de d tecter les situations o l absence de puissance hydraulique est due une fuite et ne pas activer le PTU dans ce cas Nous modifions le comportement du P TU nous consid rons qu il ne propage plus la fuite sauf lorsque le capteur est d faillant Nous ajoutons au comportement du P TU l v nement fail leakage pour repr senter la d faillance du capteur de fuite 1 node PTU 2 flow 3 icone 1 2 private 4 nom boolean 5 lexo O g Gus S 6 1 219004 2 CUR 7 Dal sec 8 9 INPXS DOOI E aia e 116 7 3 MODELISATION DE L ARCHITECTURE FONCTIONNELLE DU SYSTEME HYDRAULIQUE 42 O26 rev in DOO 1027 eG 8 OOOIL 8 Os 5 state Ke P12 1 Dil b ONE event Fa 05 6 fail_leakage update trans or S leak i lost S ok fail_leakage gt S leak S ok or S leak update gt P21_nom not PHP nome A2 and 21_ not A1 and P12_rev not A2 and assert 01 nom S ok or S leak and P21 nom 02 nom S ok or S leak and P12_nom Ii rev S leak and P12 rev I2 rev
145. es included in a trajectorydetail line such as theta kappa_in and kappa_out are optional They are generally specific to a Geometric World implementation line CATIA v5 IRIS or ICAD Disk Burst World lt hitlist name Geometrical description A320 tyre burst hit list for hydraulic system gt lt hitlistitem name fail_tyre_burst_W4_K127 gt lt failmode component B HP distribution 1 fm impacted gt lt failmode component Y EDP fm impacted 139 ANNEXE A MANUEL D UTILISATION DU MAPPINGMANAGER lt trajectorydetails theta 5 kappa in 131 kappa_out 145 gt trajectorydetails theta 4 kappa in 138 kappa out 145 trajectorydetails theta 3 kappa in 142 kappa out 145 gt lt trajectorydetails theta 2 kappa in 144 kappa out 145 lt hitlistitem gt lt hitlist gt Mapping File A mapping is a table that relates component and failure modes of the functional world with components and failure modes of the geometrical world In the following example we suppose that the list of Geometrical components was imported in the left side of the Mapping manager and it is called Geometrical whereas the other list was imported in the right side and is called Functional For each line of the table a map item is added it contains all related components For each component a failmode item is added its attribute world is either equal to the name of the list of component
146. essources de calcul et de communication Les exigences de s ret de fonctionnement associ es aux fonctions ont t interpr t es en contraintes d allocation utilis es pour g n rer automatiquement l aide d un outil de r solution de contraintes une ou plusieurs allocations possibles Pour terminer nous avons appliqu la m thode de v rification d exigences de s ret de fonction nement sur un syst me d fini dans l espace en trois dimension pour lequel l allocation consid r e est l allocation de composants r els dans diff rentes zones d un avion Pour cela nous avons consi d r l ensemble des pannes ayant un impact g ographique sur des zones avion clatement d un pneu clatement moteur etc et nous avons v rifi pour chacune d entre elles que l allocation des composants dans les zones garantissait l absence de cons quence catastrophique 8 2 Comparaison avec des travaux similaires Le travail r alis lors de cette th se c est d roul dans le cadre de deux projets de recherche in dustriels le projet CARLIT sur les techniques de d veloppement associ es l avionique modulaire int gr e et le projet europ en ISAAC sur les techniques d analyse de la s curit des syst mes a ronau tiques Dans ces deux projets les choix techniques avaient t r alis d s leur lancement En particulier la langage de mod lisation AltaRica avait t s lectionn C est pour c
147. essources supportant les t ches dans l approche propos e par les auteurs les contraintes expriment des temps de r ponses garantir sur l ex cution de taches p riodiques et sont traduites en contraintes d ordonnancement portant sur les priorit s des process ex cutant les taches leurs p riodicit s etc Finalement l allocation repr sente l architecture temps r el et donc la r partition des t ches sur diff rents process ayant diff rentes priorit s et p riodicit Cette allocation doit satisfaire les contraintes des temps de r ponse associ s aux diff rentes t ches 8 2 3 Conclusion En conclusion il nous semble que certains concepts d AltaRica sont tr s adapt s au probl me de la mod lisation du probl me d allocation Tout d abord l aspect formel du langage permet d effectuer des analyses aussi bien qualitatives que quantitatives sans qu il soit n cessaire de traduire les mod les dans un autre langage Le possibilit de construire des mod les compositionnels ainsi que la notion de synchronisation d v nements permettent de construire et d analyser efficacement un grand nombre de possibilit s d allocations En effet il n est pas n cessaire de modifier la mod lisation des architectures fonctionnelles ou mat rielles pour traiter une nouvelle allocation Seule la relation de synchronisation est modifier pour traiter une nouvelle allocation Nous n avons pas retrouv ce jour de langage de mod lisation offrant
148. est situ e au niveau de Vallocation de la donn e dMON En effet cette donn e repr sentant la communication entre le MON et Equals qui tait allou e au Bus Or dans cette allocation cette donn e n a pas besoin de transiter par un bus puisque l ensemble des t ches qui l utilisent sont sur la m me ressource de calcul Spy G n ralement on consid re que les ressources de calcul poss dent un service de communication pour l change des donn es entre les t ches allou es cette ressource Fic 4 14 Une allocation minimale propos e par l outil SatZoo La figure pr c dente 4 14 ne montre pas la ressource de communication assurant la connexion entre Ry et Sy puisqu elle n est pas utilis e De m me la figure ne montre pas la ressource inutile Ry 4 7 Bilan Dans ce chapitre nous avons montr comment en partant de la description des architectures fonc tionnelles et mat rielles et de directives d allocation comme l ind pendance et la co localisation il tait possible de produire automatiquement l allocation des fonctions sur les ressources mat rielles Ceci passe par une tape de formalisation sous forme de contraintes lin aires enti res puis par une tape de r solution de contraintes Un sch ma synth tisant cette d marche est propos en figure 4 15 67 CHAPITRE 4 RESOLUTION DE CONTRAINTES D ALLOCATION Un outil supportant cette approche a t impl ment permet d assister le concepteur
149. et la recherche d une allocation correspond une solution du syst me de contraintes Cette recherche consiste donc r soudre le syst me et extraire les r sultats pour visualiser l allocation trouv e Cette m thode est constitu e de plusieurs tapes une premi re consiste transformer le fichier de description de notre syst me cr dans la section pr c dente en un fichier d crivant le syst me de contraintes utilisable par le solveur SATZOO Le formalisme utilis par SATZOO est le formalisme ILP Pour une r solution du syst me par ce solveur l ensemble des contraintes cr doit tre en in quations lin aires accept es par le solveur La partie description du syst me ne correspond pas un ensemble de contraintes mais elle permet de d finir l ensemble des variables qui vont tre manipul es par le solveur tant donn que SATZOO n accepte que des in quations chaque quation utilis e pour la description du syst me doit tre adapt en un ensemble d in quations pour ainsi tre utilis par SATZOO Par exemple pour d crire une connexion entre la fonction de calcul d alarme de d gagement et les commandes de vol il faut d finir la variable f_cnx_ClAlarmComp_CommandeVol gt 1 L application de cette r gle sur l ensemble des variables utilis pour la description de notre syst me permet ainsi de d finir un premier ensemble d in quations Les in quations ajouter pour o
150. etrouver allou es sur une m me res source coloc F x F gt 0 1 coloc fi f2 1 f et fa sont placer sur une m me ressource idpt correspond la relation d ind pendance entre deux fonctions Elle permet de pr ciser que deux fonctions ne doivent pas se retrouver allou es sur une m me ressource F x F gt 0 1 idpt fi fa 1 f et f2 sont placer sur des ressources diff rentes set_alloc correspond pour une fonction donn e l ensemble des ressources autorisant une allocation set_alloc F gt P R set alloc fi r1 rn fi doit tre allou e une ressource parmi r1 Tn Les variables u cnr est contenu dans la fermeture r flexive sym trique et transitive de la relation cnr et correspond la relation de connexion entre ressources utilis es Ainsi lorsque cnz ri ro 1 alors r est connect ra Ceci signifie que nous ne consid rons pas forc ment que l interconnexion des ressources de l architecture mat rielle est fig e Nous recherchons les connexions qui doivent tre utilis es 54 4 3 LE DOMAINE DES VARIABLES UTILISEES alloc est la relation que nous souhaitons tablir entre les ressources et les fonctions alloc F x R gt 0 1 alloc f r 1 4 3 Le domaine des variables utilis es Comme pr sent pr c demment lors de la d claration des diff rentes variables le domaine des valeurs est l ensemble des bool ens E
151. ette raison que nous n avons pas proc d un tat de l art pr alable En revanche nous avons suivis les travaux sur des sujets similaires de fa on pouvoir placer et comparer notre approche Dans la suite de ce chapitre nous d crivons quelques travaux qui nous ont sembl particuli rement pertinents 8 2 1 Analyses de mod les AADL Beaucoup de syst mes avioniques critiques sont aujourd hui con us l aide de langages de type ADL Architecture Description Language Dans un but de standardisation et de normalisation de la conception de syst mes avioniques la communaut avionique a d fini un langage commun AADL 1 qui demeure en perp tuelle volution Ce langage est constitu d une multitude de concepts de mod lisation mais ces concepts ne sont pas organis s de mani re d crire des mod les formels En effet l interpr tation des diff rents concepts n tant pas formalis e la seule solution actuelle pour valider des mod les de ce langage consiste les transformer dans un langage formel C est une fois que la description AADL est traduite dans un langage formel que des analyses de s ret de fonctionnement peuvent tre effectu es Par exemple des mod les d crits avec AADL peuvent tre traduits en r seaux de Petri l aide de r gles de transformation Dans ce contexte les travaux d Ana Elena Rugina RKK06 Rug05 se basent sur le langage source AADL tendu avec l annexe AADL Error Model Annex SA
152. existants permettant de manipuler des mod les AltaRica SOMMAIRE 2 1 INTRODUCTION A LA MOD LISATION ET LA VERIFICATION DE SYST MES 10 SIE Mod lisation d ai Systane oo a da dh dus ha 10 2 1 2 Expression des exigences que le mod le doit v rifier 11 2 1 3 V rification automatique par exploration du mod le Model Checking 12 2 2 MOD LISATION ET V RIFICATION DE LA S CURIT DES SYST MES A RONAUTIQUES 13 2 2 1 Exigences de s ret verifier lt lt o aaa oos 4 o RR UR RR ns ee 13 222 Langages de mod lisation a acess a 44 RR ER eee ins aa 40 40 47 Be 14 2 2 3 Pr sentation d taill e du langage choisi AltaRica Data Flow 19 2 2 4 Analyses et outils disponibles pour le langage AltaRica 24 CHAPITRE 2 TECHNIQUES POUR LA MODELISATION ET LA VERIFICATION 2 1 Introduction la mod lisation et la v rification de syst mes Pour v rifier qu un syst me pr sente un comportement attendu une premi re approche consiste construire ce syst me puis observer son comportement face diff rents stimuli tests du syst me Ce type d approche pr sente deux inconv nients majeurs Tout d abord il n cessite de disposer du syst me r el et donc d tre en fin du cycle de d velop pement du syst me Par cons quent en cas de test non conforme a
153. fail error amp SM alloc fail error Par cette constatation l architecture mat rielle devient acceptable 48 3 5 BILAN 3 5 Bilan Dans ce chapitre nous avons tout d abord montr que le langage AltaRica permet de d crire les architectures fonctionnelles et mat rielles ainsi qu un mod le global repr sentant une allocation de l architecture fonctionnelle sur l architecture mat rielle C est sur ce dernier que des analyses de s ret de fonctionnement peuvent tre tablies afin de prendre en compte l impact des pannes de l architecture mat rielle sur les fonctionnalit s du syst me Description Description fonctionnelle mat rielle Mod le Mod le fonctionnel architecture Mod le global R sultats d analyse Fic 3 23 D marche pour la mod lisation Nous avons montr sur l exemple simple du COM MON que le choix de cette allocation d termine la satisfaction des exigences du syst me Dans cet exemple le nombre restreint d exigences et de composants des architectures autorise l obtention manuelle d une allocation satisfaisante Cependant d terminer une allocation dans le cadre d un syst me plus complexe s av re tre une t che difficilement r alisable et sans aucune garantie de r sultat C est pourquoi nous proposons dans le chapitre suivant une m thode de d finition automatique d allocation bas e sur le principe de r solution de contraintes 49 CHAPIT
154. fety cases for integrated flight systems Dans IEEE Aerospace Conference IEEE 1999 A BONDAVALLI I MURA ET K S TRIVEDI Dependability modelling and sensiti vity analysis of scheduled maintenance systems 3rd European Dependable Computing Conference EDCC 3 pages 7 23 1999 S BRLEK ET A RAUZY Synchronization of constrained transition systems Dans Proceedings of the First International Symposium on Parallel Symbolic Computation pages 54 62 World Scientific Publishing 1994 R E BRYANT Graph based algorithms for boolean function manipulation IEEE Trans Computers 35 8 677 691 1986 B BERTHOMIEU ET F VERNADAT Time petri nets analysis with tina Dans QEST 06 Proceedings of the 3rd international conference on the Quantitative Evaluation of Systems pages 123 124 Washington DC USA 2006 IEEE Computer Society M Bozzano A VILLAFIORITA O AKERLUND P BIEBER C BOUGNOL E BODE M BRETSCHNEIDER A CAVALLO C CASTEL M CIFALDI A CIMATTI A GRIF FAULT C KEHREN B LAWRENCE A LUDTKE S METGE C PAPADOPOULOS R PASSARELLO T PEIKENKAMP P PERSSON C SEGUIN L TROTTA L VA LACCA ET G ZACCO Esacs an integrated methodology for design and safety analysis of complex systems ESREL 2003 A CIMATTI E CLARKE F GIUNCHIGLIA ET M ROVERI Nusmv a new symbolic model checker 2000 149 BIBLIOGRAPHIE CHD 04 Cle07 Coo71 CPR04 DAS85 DPS 08 EC97 EH8
155. fonction d faillante a pour cons quence que la valeur r elle repr sent e par cette donn e n est plus dans l intervalle des donn es acceptables Une telle repr sentation des donn es permet de visualiser l impact d une donn e erron e sur les fonctions l utilisant tant donn que le SdT est constitu d un ensemble de fonctions s changeant des donn es il est important d observer le comportement global du syst me en cas 87 CHAPITRE 6 LE SYSTEME DE SUIVI DE TERRAIN SDT D UN AVION DE CHASSE de pr sence d une donn e n ayant pas une valeur attendue lost Comme d fini pr c demment dans le chapitre 3 il existe une d faillance sur les fonctions qui les emp che de produire leur r sultat Cette valeur permet d observer l influence d une absence de donn e n cessaire pour le syst me Value erroneous correc Time FIG 6 5 Abstraction de la valeur d une donn e Dans la suite de ce chapitre lorsque ce type sera utilis dans les composants AltaRica il sera repr sent par le domaine suivant 1 domain FailureType correct erroneous lost Une fois que l abstraction des donn es chang es est effectu e il faut identifier le niveau d abs traction n cessaire pour la mod lisation des fonctions et autres composants du syst me Le niveau d abstraction choisi pour cette analyse est celui d fini dans le chapitre 3 Les diff rents composants du syst me peuvent ains
156. gn process of hard real time systems with constraint programming Dans Third Taiwanese French Conference on Information Technology TFIT 2006 pages 317 331 Nancy France 2006 P E HLADIK CAMBAZARD A M DEPLANCHE ET N JUSSIEN Solving a real time allocation problem with constraint programming J Syst Softw 81 1 132 149 2008 150 BIBLIOGRAPHIE K B96 KSB 04 KSBC04 LaB07 Lap96 Lew06 LM8S McM98 MLMEP 05 Pag04 PBRO3 Pet81 PL 00 Pnu77 Poi00 PR99 Rau Rau02 RKK06 Rug05 RY97 K KANOUN ET M BORREL Dependability of Fault Tolerant Systems Explicit Modeling of the Interactions between Hardware and Software Components Proc IEEE Interna tional Computer Performance Dependability Symp IPDS 96 49 252 61 1996 C KEHREN C SEGUIN P BIEBER C CASTEL C BOUGNOL J P HECKMANN ET S METGE Advanced simulation capabilities for multi systems with altarica Dans International System Safety Conference 2004 KEHREN SEGUIN BIEBER ET CASTEL Analyse des exigences de s ret d un syst me lectrique par model checking Dans Actes du Congr s de Ma trise des Risques et de S ret de Fonctionnement pages 492 497 Bourges France Octobre 2004 LABRI ARC AltaRica Checker http altarica labri fr 2007 J C LAPRIE Guide de la s ret de fonctionnement 1996 C padues ISBN 2854283821 B Lewis The sae architecture a
157. hacun des syst mes critiques composant un avion soit con u en consi d rant les contraintes de fiabilit Pour pr ciser les notions de s curit et de fiabilit d un syst me des exigences lui sont associ es et caract risent son taux de d faillance acceptable en probabilit Par exemple une fonctionnalit indispensable pour le bon d roulement d un vol se verra associ e une exigence dont le taux de d faillance acceptable sera suffisamment faible pour que la d faillance soit consid r e non atteignable au cours des heures de vol effectu es dans la vie d un avion Les taux de panne des composants constituant un syst me ne permettent g n ralement pas de garantir le taux global de d faillance du syst me Par cons quent le m canisme de redondance des composants du syst me est souvent utilis pour diminuer son taux global de d faillance Ce m canisme consiste recourir plusieurs composants mat riels identiques pour supporter une m me fonction Finalement pour r pondre des exigences fonctionnelles caract ris es par une probabilit de d faillance une allocation des fonctions sur une architecture physique doit tre d finie Cette allocation doit garantir en tenant compte i des taux de pannes associ s chacun des composants mat riels et ii des impacts relatifs des pannes entre composants du fait de leurs relations que le taux de d faillance global du syst me est acceptable Dans le but de garantir la
158. he mapping manager to be able to create and store mappings and to generate failure sets e optional attribute in normal font this information is not compulsory for the mapping manager but 1t could be necessary for the Geometrical or Functional tools An optional attribute is not analysed by the mapping manager so you can add attributes with any name you want as long as it is different from the names of the compulsory attributes Optional attributes are stored in the mapping files and they are included in the failure set files generated 138 Component and Failure Mode List The proposed format for imported component list consist of a ailmode item for each pair component associated failure mode found in the Geometrical or Functional model Attribute component is the name of the component and attribute fm is the name of the failure mode Other attributes were discussed during ISAAC Paris meeting they are optional The value of attribute internal is an internal name for the component that is not displayed in the mapping manager but that is useful for the functional world tools especially for Prover implementation line Attribute description can be used to include a textual description of the failure mode Attribute zone can be used to store information about the zone where an equipment is installed Two examples of Component Lists lt failmodes name Geometrical gt lt failmode component G HP EDP TConnection fm impacted descrip
159. i subir plusieurs d faillances fail error et fail lost Ces d faillances per mettent d illustrer le comportement erron d une fonction ainsi que la perte de ladite fonction dans notre cas nous consid rons qu une perte de fonction correspond la non production de la donn e associ e L automate correspondant aux diff rents changements d tat d une fonction section 3 2 en page 33 est rappel dans la figure suivante correct fail lost fail error bn _ i fail lost Ce niveau d abstraction doit tre appliqu l ensemble des l ments composant le syst me Sd Pour cela il suffit de cr er pour chaque composant du syst me son correspondant en AltaRica L ana lyse des diff rents composants du syst me permet d identifier plusieurs familles de composants Les capteurs composants produisant des donn es Nous utilisons deux types de capteurs Capteur source Ce capteur n a pas d entr e et a une sortie unique Ce type de comportement est associ aux fonctions Radar TFTAPanel Rolll et Roll2 le code AltaRica associ ce composant a t d crit dans la section 2 2 3 Capteur boucl Ce capteur a une entr e qui est branch e sur la sortie du syst me SdT Ce type de composant est associ aux fonctions Navigation RadioAltimeter En l absence de d faillance ce composant propage sur son port de sortie ce qui est sur le port d entr e 88 6 3 MODELISATION DU SYSTEME Foncti
160. i une explosion donn e conduit une des siutations redout es qui ont t envisag es par les analystes de s ret de fonctionnement Comme cela est visible dans la figure 7 22 l interface du logiciel regroupe la fois la visualisation du mod le en 3 dimensions partie droite de la figure et la visualisation de la liste des l ments impact s Hitlist suivant un angle donn l angle est repr sent par la coupe de couleur marron dans la partie visualisation Generation of impacts burst animation Damaged systems OEOMETRY Hit list Frames 18 mue BLG BLG 2 BLG 3 BLG 4 NLG L H NLO RIH HYDRAULIC Data export PTU Yellow Y HP EDP TConnection Ayra burst W4 y Yellow Y Suction rsvy EDF Myre burst W4 i Yellow Blue E HP Distribution 4 tyre burrt Wa SERAT Veto HP Monito Blue Blue B HP Distribution 4 Ayre burst W4 Yellow reservoir Green G HP Distribution 2 Ayre burst W4 Blue EMP Green Green G HP Distribution 2JAyre burst W4 Damaged Systems Blue HP Manifold Blue Priority Valve Power transter Unit 1 45 00 Kappa 165 00 Kappa Step 2 00 Thetat 0 00 Theta2 0 00 Theta Step 2 00 Green reservoir Green G HP Distribution 2 Kappa IN 125 00 OUT 131 00 Green HP Manifold Yellow Y HP EDP TConnection Kappa IN 127 00 Kappa OUT 135 00 Yellow Y Suction rsv
161. iables bool ennes 2 a a a a a a 4 5 2 Des variables bool ennes vers des in quations lin aires 4 6 R SOLUTION DU SYSTEME DE CONTRAINTES 16 1 Trop d allocations possibles o a ea u u b b oe ee biais E AN 52 54 55 55 59 59 60 62 65 67 51 CHAPITRE 4 RESOLUTION DE CONTRAINTES D ALLOCATION 4 1 Mod lisation et approche par contraintes D finition 4 1 Programmation par contraintes La programmation par contraintes consiste d crire un probl me en termes de variables et de contraintes satisfaire Chaque contrainte exprime une propri t devant tre v rifi e par un sous ensemble de variables Une contrainte est une condition logique sur un ensemble de variables La mod lisation d un probl me de satisfaction de contrainte ou CSP Constraint Satisfaction Pro blem consiste identifier les variables et leurs domaines de d finition repr sentant les ressources et les fonctions du probl me ainsi que l ensemble des contraintes portant sur ces variables D finition 4 2 CSP Un CSP est mod lis comme un triplet X D tel que X est un ensemble de variables D est un ensemble de domaines tel qu un domaine D x soit associ avec chaque x E X C est un ensemble de contraintes sur les variables de X D finition 4 3 R solution d un CSP R soudre un CSP consiste trouver une ou toutes les solutions possible
162. ial du composant init d clare la situation nominale que le syst me doit aborder Des informations comme les probabilit s d occurrence associ es des v nements peuvent tre ajout es aux diff rents composants du syst me dans la partie extern Ces informations peuvent ensuite tre utilis es par des outils de traitement de coupes minimales comme Aralia par exemple La cr ation d un mod le AltaRica passe tout d abord par l application de ces r gles de conception pour chacun des noeuds de l architecture fonctionnelle Les connexions des diff rents noeud de cette architecture sont ensuite transform es en flux de donn es entre les composants AltaRica correspondants pour terminer la cr ation du mod le AltaRica Le code AltaRica de notre exemple et la s mantique qui lui est associ e sont repr sent s par la figure 2 5 19 CHAPITRE 2 TECHNIQUES POUR LA MODELISATION ET LA VERIFICATION RO 2 node Sensor state boolean for the state variable Status bool flow boolean for the output of the Captor capt out bool outi event failure fannie trans failure effect Status fail_error gt Status false assert behavior of the Captor capt_out Status edon fail_error a c Status Status true false Fic 2 5 Code Altarica et automate de comportement d un Capteur La d finition formelle d un mod le AltaRica est bas e sur un automate de mode
163. ible par l ajout de l allocation dans le mod le AltaRica est la si mulation du syst me dans une configuration architecturale r elle Cette simulation permet de visualiser l effet des d faillances mat rielles sur l architecture fonctionnelle tant donn une allocation De plus il est possible de v rifier que les exigences de s ret de fonctionnement satisfaites par l architecture fonctionnelle sont effectivement pr serv es apr s allocation sur l architecture mat rielle A priori cette v rification est inutile puisque les allocations fournies par le solveur pr servent les exigences de l architecture fonctionnelle Malgr ceci cette v rification peut tre int ressante dans le contexte de certification o l on appr cie de disposer de plusieurs moyens ind pendants pour obtenir certains l ments de confiance Cette v rification pourrait permettre de d tecter d ventuels probl mes lors de l identification des contraintes de s gr gation ou lors de la r solution des contraintes 5 3 Adaptation de l architecture mat rielle Nous pr sentons dans cette partie une am lioration de notre m thode de r solution de contrainte Lorsqu une architecture existante ne satisfait pas les exigences qui lui sont associ es il est souhai table de pouvoir proposer aux architectes une justification de la non satisfaction des exigences et de proposer une architecture minimisant les modifications apporter pour rendre l architectur
164. ichis par ces mod les d erreur De plus l auteur met en avant la n cessit de construire son mod le base d it ration En effet la construction d un r seau de Petri repr sentant un mod le AADL et un mod le d erreur n cessite plusieurs parcours successifs des mod les d entr e Ces it rations ne sont pas n cessaires dans le cas de la transformation d un mod le AADL en langage AltaRica comme cela est d fini dans DPS 08 Plus pr cis ment dans le cas de la transformation d un mod le AADL en un r seau de P tri une premi re it ration est n cessaire sur le mod le AADL pour mod liser les comportements des composants du syst me en pr sence uniquement de leurs propres fautes et v nements de r paration Par cons quent les composants sont mod lis s comme s ils taient isol s du reste du syst me Ensuite par des it rations successives le mod le est compl t en introduisant les d pendances entre les composants Le mod le AADL de s ret de fonctionnement est mis jour chaque it ration en prenant en compte les nouvelles d pendances identifi es Une fois le mod le AADL de s ret de fonctionnement global cr e il est ensuite traduit en RdPSG r seaux de Petri stochastiques g n ralis s pour y v rifier des propri t s La diff rence avec notre approche est dans le choix du langage En effet le langage AltaRica contient l ensemble des composants constituant le syst me lui aussi direc
165. idp evi ev F evi F ev gt F failure count gt 2 o event event est une paire de d faillances apparaissant dans la partie droite de la formule En utilisant ces hypoth ses ainsi qu une hypoth se suppl mentaire sp cifiant que seules les t ches peuvent subir une d faillance nous pouvons prouver que l exigence de s ret est respect e par le mod le COM MON 5 2 De l hypoth se d ind pendance vers la contrainte de s gr gation La validation des exigences de s ret de fonctionnement sur un mod le de syst me n est possible que sous certaines hypoth ses Comme nous l avons vu pr c demment un ensemble d hypoth ses sur l ind pendance de fonctions est n cessaire pour v rifier ces exigences Les hypoth ses d ind pendance que nous avons identifi es dans la section pr c dente nous indiquent par exemple que la fonction ne doit pas tre allou e sur la m me ressource que la fonction fa si l on souhaite v rifier certaines propri t s Nous proposons donc de traduire ces hypoth ses en contraintes directives de s gr gation afin de n obtenir lors de la r solution du syst me de contraintes que des allocations pr servant les exigences de s ret La d marche ainsi propos e est sch matis e par la figure 5 4 Elle reprend les d marches tablies dans les chapitres pr c dents cf 3 23 et 4 15 en y ajoutant une m thode d int gration On peut lire le sch ma de la fa on suivante
166. igure 2 4 Un mod le AltaRica permet de d crire des syst mes r els et peut tre traduit dans plusieurs formalismes de plus bas niveau permettant diff rents types d analyses comme illustr par la figure 2 4 Syst me de transitions Model checking gt Simulation a gt stochastique calculs de EN disponibilit Chaine de Markov 4 ES 2 2 e e S oo 1 E 4 mplicants premiers Formule bool enne LA 4 FIG 2 4 Atelier AltaRica Nous pr sentons ci apr s plus en d tails ce langage et les outils qui lui sont associ s Les industriels int ress s par le langage AltaRica Dassault System et EADS APSYS ont adopt ce langage pour leurs outils de mod lisation qui sont respectivement Cecilia OCAS et SIMFIA Le langage AltaRica utilis par ces outils est une restriction du langage d origine en vue de faciliter la compilation Le nombre de variables autoris es est fini les variables d tat appartiennent 4 des intervalles finis d entiers et les flux ne sont plus bidirectionnels On a galement une simplification de la notion de priorit entre v nements Dans cette th se nous nous int resserons la version Data Flow utilis e au sein de l outil OCAS que nous avons utilis pour r aliser nos mod les et certaines analyses Cette version all g e du langage est galement utilis e par la ToolBox d Arboost Technologies au
167. il m a beaucoup profit lors de mes pr sentations Je pense galement Virginie qui par ses histoires savait nous donner un bon fou rire pour la journ e A nsi que tous ceux qui prenaient le temps de venir partager un moment bavard dans le bureau Bruno Charles Chritiane Claire Fr d ric Guy Josette Jean Loup et Jean Yves Et merci Jacques Cazin pour son accueil dans le d partement Puis un laboratoire c est aussi une ambiance cr e par ces jeunes locataires les th sards Je pense Christophe pour notre amiti pendant et apr s la th se depuis Balma jusqu a Menecy un grand merci pour avoir tent de venir assist ma soutenance et m avoir mis dans un tat de panique 15 minutes avant le d but de ma soutenance cause d une Velsatis Je pense galement Alex qui fut un adversaire redoutable Tower defense Matthieu qui a su construire la map du CERT Thomas qui restera toujours le stagiaire casqu Julien Sophie H Sophie L et St phanie et les nouveaux arrivants C dric et Romain toujours partant pour faire une pause Les physiciens d en face qui ont galement particip la bonne humeur de toutes les pauses je pense Domingo avec qui on a r ussi pas longtemps faire d couvrir le Mus et ainsi d tr ner les parties endiabl es de coinche Je pense Maud et ric fervent d fenseur des Bretons Je pense enfin Flo R my et H l ne pour les tournois de coinche reste Manu mon p
168. impact d une allocation sur la s curit d un syst me un second souhait serait de disposer d outils qui g n rent des allocations qui seraient conformes aux exigences de s curit du syst me tudi Notre objectif principal est d assister les analyses CCA par l utilisation des techniques de m thodes formelles Nous aurons donc deux sous objectifs conformes aux pr occupations des ing nieurs proposer un moyen pour v rifier automatiquement qu une allocation est s re proposer un moyen pour g n rer automatiquement des allocations s res Pour le premier sous objectif notre d marche consiste mod liser l aide d un langage formel AltaRica dans notre cas les architectures fonctionnelles et mat rielles du syst me ainsi que l allocation des fonctions sur les composants de l architecture mat rielle Nous construisons deux mod les le mod le fonctionnel qui est restreint l architecture fonctionnelle et un mod le global qui d crit galement l architecture mat rielle et l allocation Il faut galement formaliser les exigences de s curit que le syst me doit v rifier Il est ensuite possible de v rifier automatiquement la tenue de ces exigences pour les deux mod les construits Finalement nous proposons de comparer les r sultats des v rifications pour les deux mod les de fa on d terminer si l impact de l allocation est acceptable du point de vue de la s curit CHAPITRE 1 I
169. ion rsvg EDP EDPg rsvg G rsvg rsvg G HP NPriority Distribution NPdistg Nws LandingGear SlatsFlaps G HP T PV PTU NPDistribution G HP PV TConnection PTU PVg Npdistg G HP Distributionl G HP Distribution2 G HP Distribution3 Pdistg NormBrakes RevEng1 Yawdamperl FlapsR Rudderg spoilerl Stabilizer elevator1 aileronR spoiler5 Y HP PV PTU PVy PTU Y PV PVy Y ManifoldHP Y HP PTU HPManifold Y HP T EDP EMP PTU Y HP TConnection Y Suction T rsvy EMP EDP Y Suction rsvy TConnection Y HP HP Manifold T PV Y HP Manifold T PV Y HP HP Manifold PV Y HP T EDP EMP PTU HPManifold EDPy EMPy PTU PVy Pdisty Y EDP EDPy Y EMP EMPy Y rsvy rsvy Y Suction rsvy EDP Y Suction rsvy EMP Y HP T EMP EDP Y HP EMP TConnection Y HP EDP TConnection rsvy EDPy EMPy Y HP T NP Distribution NPdisty Y HP Distributionl Y HP Distribution2 Y HP Distribution3 Pdisty YawDamper2 RevEng2 FlapsL spoiler2 AltBrake elevatorR spoiler4 B PV PVb B EMP EMPb B Suction rsvb EMP B Suction rsvb RAT B HP T RAT EMP B HP RAT TConnection B HP EMP TConnection B Suction T rsvb RAT EMP B Suction rsvb TConnection rsvb RATb EMPb B RAT RATb B rsvb rsvb B HP NPriority Distribution NPdistb CSMG Slats B ManifoldHP B HPManifold PV B HP TConnection HP Manifold EMPb RATb PVb Pdistb B HP Distributionl B HP Distribution2 B
170. iter que ces donn es aient un long chemin parcourir on entend par chemin le parcours des donn es dans les diff rentes ressources mat rielles n cessaires pour connecter ces fonctions L action de rapprocher les ressources h bergeant ces fonctions ou bien le fait de choisir l allocation de ces fonctions sur une m me ressource est important pour le concepteur Afin de simplifier cette d marche une nouvelle contrainte permet de sp cifier les diff rents regroupements de fonctions possibles allouer sur une m me ressource La contrainte correspondante pour imposer l allocation de deux fonctions sur une m me ressource est la suivante Vf fa F Yr E R coloc fi f2 gt alloc f1 r alloc f2 r 4 5 Allocation L imposition d une certaine allocation une fonction f peut se traduire en une affectation de la variable correspondante alloc f ri Par cons quent la contrainte permettant d imposer le choix de l allocation d une fonction f sur une ressource r s exprime de la fagon suivante alloc f r 1 Exclusion A l inverse certaines ressources peuvent ne pas avoir un degr de fiabilit suffisant pour autoriser l allocation d une fonction dite critique En effet lorsque l architecture mat rielle le permet plusieurs ressources ayant des caract ristiques diff rentes peuvent tre mises disposition Suivant l importance et le degr de fiabilit de la fonction le concepteur peut souhaiter inter
171. ivers ponts entre la s ret de fonctionnement et les m thodes formelles Nous avons choisi ce langage pour notre d marche pour l ensemble des raisons suivantes AltaRica est bas sur les automates contraintes FP93 et sp cifie un syst me comme un en semble de variables contraintes par des formules L volution de ces variables est d finie par les tiquettes des transitions Il permet ainsi de combiner la description d un comportement 17 CHAPITRE 2 TECHNIQUES POUR LA MODELISATION ET LA VERIFICATION fonctionnel et dysfonctionnel d un syst me l aide de contraintes sur les diff rentes variables caract risants ses composants La repr sentation dysfonctionnelle du comportement d un syst me est simplifi e gr ce l intro duction de transitions mod lisant la d faillance des composants Ce langage permet d effectuer des analyses quantitatives ou qualitatives partir du m me mod le selon que l on prend en compte les lois de probabilit associ es aux transitions Sa capacit r aliser des mod les compositionnels et hi rarchiques lui permet de mod liser des syst mes complexes Les mod les AltaRica peuvent tre dit s de mani re graphique par diff rents outils fournis par les industriels partenaires du projet et ils peuvent aussi tre dit s et manipul s directement par le formalisme de d finition du langage Les principes de l atelier AltaRica sont r sum s dans la f
172. l faut respecter certaines exigences Par exemple lorsqu une situation est qualifi e catastrophique alors il faut au minimum des combinaisons de 3 d faillances pour y parvenir De m me la probabilit associ e la pr sence d une telle situation est de 107 par heure de vol La correspondance entre les exigences qualitatives portant sur le nombre de pannes et quantitatives portant sur la probabilit d occurrence d une situation suivant la classification des situations est d crite par le tableau suivant 13 CHAPITRE 2 TECHNIQUES POUR LA MODELISATION ET LA VERIFICATION Probabilit s de pannes gt 103 10 lt 10 77 lt 1079 Cons quences interdit interdit interdit interdit interdit interdit Simple Double Double Triple Nombre de pannes Exigence Qualitative Lorsque le syst me tudi a un comportement dynamique li par exemple des actions de reconfi guration il faut habituellement examiner non pas un tat mais une s quence d tats pour d terminer si la situation redout e est atteinte Dans ce cas nous avons recours aux op rateurs de la logique temporelle pour formaliser la situation redout e 2 2 2 Langages de mod lisation Les principaux langages de mod lisation utilis s dans la s ret de fonctionnement sont des langages permettant d observer l impact de la d faillance de l un de ses composants sur l ensemble du syst m
173. lise l envoi d un message de f vers fi L architecture mat rielle est d finie par un graphe R r_cnx caract ris par l ensemble R mri rg Tn de m ressources connect es entre elles par les arcs r cnr C R x R on supposera dans la suite que cette E H relation est sym trique Comme pour l architecture pr c dente un arc rjj r cnz ri rj repr sente l change de donn es entre les ressources r et r Cette architecture mat rielle permet de repr senter une architecture de diff rentes ressources de calcul communicantes entre elles par un r seau La relation d allocation est repr sent e par alloc qui pour une fonction f de F et une ressource de R vaut 1 si et seulement si f est allou e sur r alloc F x R 40 1 alloe F r 1 Exemple Une relation d allocation possible de l architecture fonctionnelle sur l architecture mat rielle de la figure pr c dente est donn e dans la figure suivante alloc fi ri alloc fa r3 alloc fs ra alloc fa ri Fic 3 1 Exemple d une relation d allocation Cette allocation permet de repr senter la r partition des diff rentes fonctions sur les ressources Lorsque nous tudions s par ment le modele d architecture fonctionnelle du modele d architecture mat rielle nous supposons que chaque fonction est implicitement allou e sur une ressource unique totalement ind pendante n ayant aucune interaction avec les autres ressources Ce
174. ll de la figure 6 2 En effet il est indispensable pour le bon d roulement de ce d gagement que l avion soit horizontal sinon il pourrait tre inop rant ou m me conduire la perte de l appareil 84 6 2 DESCRIPTION DU SYSTEME Il existe une autre mode dit manuel les ordres de pilotage sont envoy es sur les crans de visualisation et c est au pilote de suivre ou non ces ordres Finalement il existe un mode dans lequel toutes les protections alarme li e une altitude dangereuse et commande de d gagement automatique sont inhib es b Roulis c Tangage Fic 6 2 Mouvements possibles de l avion 6 2 Description du syst me 6 2 1 Architecture fonctionnelle Le r le du syst me consid r est de maintenir une altitude minimale en fonction d un plan de vol d cid l avance par le pilote Cette altitude varie suivant le terrain survol par l appareil L ensemble des fonctions utilis es par le syst me est sch matis par la figure 6 3 Afin de s adapter constamment au relief du terrain le syst me est dot d un Radar que nous consid rons par la suite comme un capteur fournissant en permanence un flux de donn es permettant de lui fournir des images du terrain mage Terrain Les donn es produites par ce capteur sont compar es aux Donn es terrain donn es pr alablement enregistr es dans une base de donn es propre la mission nomm e BD Terrain pour v rifier que l appareil suit la
175. loa 6 MES IN 7 De ve 8 Ail 2 atiet E 9 IND SOL e al a 10 02 bool out 11 02 rev am 110 7 3 MOD LISATION DE L ARCHITECTURE FONCTIONNELLE DU SYST ME HYDRAULIQUE 12 ILA e ias 13 revs bool OUE 14 state 15 SENDO 16 loci e 17 mom loool e 18 li 19 P2 load E 20 event 21 fail_Loss 22 update 23 trans 24 S true fail Loss gt S false 25 S true update gt P21 nom not A1 and A2 and I2 nom 26 DiD mom g Gow A2 Ai 27 P21 rev not A1 and A2 and O1rev 28 Pi2_rev not A2 and 1 and 02 rev 29 assert 30 01 nom S and P21 nom 31 Aaa sand Pio nom 32 Ii rev P12 rev 33 I2 rev P21 rev 34 init 35 S true 36 P12 rev false 37 P12 nom false 38 P21 rev false 39 P21 nom false 40 edon La composition de l ensemble de ces composants permet de construire le mod le AltaRica du syst me hydraulique Ce mod le est construit l aide de l outil C cilia OCAS et est repr sent par la figure suivante encl NPdistq E HI SlatsFlaps ny4 FlapsR P Rudder Pdistg Rudderg scanitizery ES spoileri 3 rSvEDPY EDFy YanDenperz seabsiizerg HI RevEng2 9 elevator _sileronR_ _spoilers
176. location n Fic 6 9 Autres solutions possibles du syst me Suivant les choix tablis partir de nouveaux crit res d optimisation le concepteur peut pr f rer une allocation plut t qu une autre Par exemple comme visible dans la figure pr c dente l allocation n permet une r partition plus quitable des fonctions sur les ressources Une fois obtenue une allocation il est possible d tendre le mod le de l architecture fonctionnelle avec des synchronisations qui repr sentent l effet des d faillances mat rielles sur les composants fonc tionnels Le mod le obtenu peut tre utilis pour affiner l analyse Par exemple en cherchant valuer l impact quantitatif des d faillances mat rielles sur la probabilit d occurrence d une situation redout e Ceci a t r alis pour le syst me SdT et d crit dans l article 3507 6 8 Bilan Nous avons d velopp un outil permettant de g n rer automatiquement et de visualiser un ensemble d allocations de fonctions sur des ressources satisfaisant un ensemble de contraintes Cet outil utilise des contraintes qui sont d riv es partir de la mod lisation AltaRica de l architecture fonctionnelle d un syst me Cette approche a t tendue pour traiter avec plus de d tail les architectures de r seaux distribu s au sein des avions civils L approche a t appliqu e par l ON RA et l IRIT l tude du placement des fonctions d un syst me de d tection d incendie sur une a
177. lv u sinon Vv S Voy y Y a D finition 2 4 la synchronisation Soit A D S un automate de mode et rect r vecteurs de synchronisation X est le sous ensemble de Y qui contient les v nements pr sents dans les vecteurs de synchronisation la synchronisation de A par les e est un automate de mode e1 e D S F dom EX U fei er 9 I avec Ve EN X s dom S et I dom F si s I e est d finie alors 5 s I e est aussi d finie et s I e El s 1 e V e e1 eg s dom S et I dom F si s I e1 0 s I ey sont d finies et compatibles deux deux alors o s I ei 0 5 1 1 0 s T ex Le langage AltaRica propose une notation sync permettant de construire des vecteurs de synchro nisation Le vecteur ainsi cr porte sur un ensemble de transitions de type v nement Nouvelle Garde affectation Rappelons que les v nements sont d clenchables lorsque la condition bool enne repr sent e par la Garde est vraie La synchronisation d v nements d automates de mode n autorise pas le d clenche ment individuel des diff rents v nements synchronis s il ne permet que le d clenchement simultan Par cons quent une synchronisation n est d clenchable que lorsque toutes les gardes des v nements synchronis s sont vraies L outil Cecilia OCAS propo
178. milar to a safety assessment file where names of functional components are replaced with names of geometrical components that are mapped to them lt cutsets failsets Safety Results of the Hydraulic Functional Model extended with tyre burst information failmodes Functional gt lt cutset original_size 2 name a_cut_set_name gt lt failset name a_fail_set_name gt failmode world Geometrical component Y EDP fm impacted description Yellow Engine Driven Pump relevant yes failmode world Geometrical component B HP distribution 1 fm impacted description Blue High Pressure Distribution line first part relevant no failmode world Geometrical component B HP distribution 2 fm impacted description Blue High Pressure Distribution line second part relevant no failmode world Geometrical component B HP distribution 3 fm impacted description Blue High Pressure Distribution line third part gt lt failset gt lt cutset gt lt cutsets gt A textual format is also available for Geometrical cut set files The file has 5 columns separated by commas Cutset_Name failset world component failure mode 2 MapManager Operations 21 MapManager GUI overview 141 ANNEXE A MANUEL D UTILISATION DU MAPPINGMANAGER List of mappings Mapping Manager 1 4 4 06 07 14 E D xl
179. move mapping buttons apping name entry Automatic mapping button T429 b hp d3 impacted TA29 b hp d4 impacted T429 9 hp edp engl tconnection hpM impacted TA29 g hp edp eng2 tconnection hpM impacted gt FailSet lt CutSets Check Save Exit Buttons to create name and remove a mapping 2 3 1 Create a mapping To create a new mapping click on the New button then a new mapping called map_untitled_ This new mapping should appear in the mapping list To create a new mapping with a name selected by the user enter a mapping name in the mapping name entry and type on the RETURN key The new mapping name should appear in the mapping list 2 3 2 Add components to a mapping Select a mapping by double clicking on its name in the mapping list Then add components from either side by double clicking on them Their names should appear on the list of mapped items and their names should be coloured in Purple in the component lists It is also possible to select several components from one side and add all of them at a time by right clicking 2 3 3 Remove components from a mapping Select a mapping by double clicking on its name in the mapping list Then remove components by double clicking on their names in the list of mapped items Their names should disappear from the list of mapped items and their names should no longer be coloured in Purple in the component lists 143 ANNEXE A MANUEL D UTILISATION DU MAP
180. mps r els r partis embarqu s pour la g n ration automatique d applications formellement v rifi es PhD thesis Ecole Nationale Sup rieure des T l communications December 2006 A VINCENT Conception et r alisation d un v rificateur de mod les AltaRica PhD thesis LaBRI Universit Bordeaux 1 d cembre 2008 S YAMANE Verification system for real time specification based on extended real time logic Dans RTCSA 95 Proceedings of the 2nd International Workshop on Real Time Computing Systems and Applications page 192 Washington DC USA 1995 IEEE Computer Society 152
181. n effet nous souhaitions un moyen simple pour exprimer une relation d finie pour chaque variable Par exemple tant donn que le probl me qui nous int resse est un probl me d allocation l utilisation de variables bool ennes permet d affirmer pour chaque fonction si oui ou non elle est allou e une ressource alloc f1 r1 0 signifiant que la fonction f n est pas allou e sur la ressource r1 De plus l avantage de la mod lisation partir de variables bool ennes est que cela permet de construire facilement notre probl me de contraintes comme un probl me SAT En effet un probl me SAT consiste d terminer si une formule construite partir de variables bool ennes admet ou non une solution c d s il existe une attribution de valeur chacune des variables qui satisfait la formule Nous verrons dans la suite comment construire ce probl me SAT partir des contraintes 4 4 Les contraintes Les diff rentes contraintes utiles notre mod lisation peuvent tre regroup es en 2 cat gories des contraintes sur les connexions autoris es et des contraintes sur le placement des fonctions sur les ressources Ces contraintes sont ensuite enrichies par des directives d allocations issues des choix de conception Les contraintes de placement Elles concernent le positionnement des fonctions sur l ensemble des ressources 1 Toutes les fonctions doivent tre allou es Cette contrainte est due la n cessit
182. nalysis amp design language aadl a standard for engi neering performance critical systems ERTS 06 January 2006 C LIN ET D C MARINESCU Stochastic high level petri nets and applications IEEE Trans Comput 37 7 815 825 1988 K L McMILLAN The SMV language Mars 1998 disponible a http www cad eecs berkeley edu kenmcmil psdoc html JR M L MCKELVIN EIREA PINELLO KANAJAN ET A L SANGIOVANNI VINCENTELLI A formal approach to fault tree synthesis for the analysis of distributed fault tolerant systems Dans EMSOFT 05 Proceedings of the 5th ACM international conference on Embedded software pages 237 246 New York NY USA 2005 ACM C PAGETTI Extension temps r el d AltaRica PhD thesis Ecole Centrale de Nantes April 2004 T PETIT C BESSIERE ET J C REGIN D tection de conflits pour la r solution de probl mes sur contraints Dans 9emes Journ es nationales sur la r solution pratique de probl mes NP complets JNPC 03 pages 293 307 Amiens France 2003 J LYLE PETERSON Petri Net Theory and the Modeling of Systems Prentice Hall PTR Upper Saddle River NJ USA 1981 P PETTERSSON ET K G LARSEN UPPAAL Bulletin of the European Association for Theoretical Computer Science 70 40 44 2000 http www uppaal com A PNUELI The temporal logic of programs Dans 18th IEEE Symp pages 46 57 Foundations of Computer Science 1977 POINT AltaRica contribution Vunification de
183. nce fail lost qui permet de repr senter la perte totale de la ressource perte de l alimentation lectrique d t rioration interne de la ressource etc Une fois que cette d faillance apparait la ressource n est plus utilisable elle ne communique plus et par cons quent ne fournit plus de donn es La d faillance fail error quant elle repr sente une perte partielle de la ressource Lorsqu une ressource subit cette d faillance toutes les donn es qui sont utilis es ou manipul es par cette ressource seront consid r es comme corrompues erron es L v nement update permet de revenir un tat de fonctionnement correct 38 3 3 MODELISATION DE L ARCHITECTURE MATERIELLE correct fail_lost fail_error R NN cd fail lost update Fic 3 10 Comportements possibles des ressources Le code AltaRica correspondant une ressource mat rielle est le suivant 1 node ress 2 state 3 SECO RTS CTO ron 4 event 5 errors Sal Lost Wiecleise gt 6 trans 7 not 9 lost fail lost gt S lost 8 S correct fail error gt S error 9 S error update gt S correct 10 init 11 S true 12 edon Ce premier mod le nous donne le comportement souhait face aux d faillances mais il ne donne pas le comportement d aux interconnexions Les connexions entre les ressources ne sont pas repr sent es dans le code AltaRica car elles varient en fonction de l archite
184. ne plus En cas de d faut d alimentation lectrique des pompes lectriques l APU peut fournir de l nergie lectrique ces pompes Auxiliary Power Unit 103 CHAPITRE 7 SYSTEME HYDRAULIQUE D UN AVION DE TYPE A320 engl HS PTU Pes eng2 elec elec2 V gt EMPb gt 3NPdistb rsvb LI 3 RAT gt Pdistb Blue Fic 7 2 Architecture du syst me Hydraulique 7 2 2 Les exigences v rifier Les diff rentes exigences que nous souhaitons valider sur ce syst me concernent les diff rentes combinaisons possibles de perte des lignes hydrauliques Nous consid rons plusieurs situations risques La perte totale de la puissance hydraulique est une situation consid r e du niveau le plus critique car elle concerne l ensemble des lignes hydrauliques tant donn que de nombreux syst mes sont en relation directe avec cette source de puissance la perte de l ensemble des lignes hydrauliques pourrait engendrer une situation hautement dangereuse Ainsi pour qualifier cette situation nous choisissons la cat gorie la plus critique CAT Comme vu dans le chapitre 2 1 2 l exigence qualitative qui en d coule est qu il ne faut pas qu une panne simple ou double nous m ne cette situation Et l exigence quantitative fixe un taux d
185. nnes de priorit qui permettent d isoler les consommateurs non prioritaires et d alimenter uniquement les l ments critiques e D un PTU Power Transfert Unit qui lorsqu il y a une diff rence de pression entre les syst mes Jaune et Vert permet d alimenter le syst me ne fournissant pas de puissance en utilisant la puissance hydraulique du syst me qui en d livre le plus Le syst me bleu poss de deux pompes une pompe lectrique que l on notera EMPb et la RAT En cas de perte des deux r acteurs ou bien en cas de perte totale de la g n ration lectrique un syst me de secours appel RAT situ sous l avion se d ploie automatiquement et alimente en puissance hydraulique le circuit bleu Le syst me vert poss de une pompe m canique not e EDPg li e au r acteur n 1 En cas de d faillance de cette pompe et uniquement si la vanne de priorit du syst me jaune est ouverte le PTU alimente automatiquement le circuit vert en fournissant une partie de la puissance du circuit jaune Le circuit jaune poss de deux pompes une pompe lectrique not e EMPy ainsi qu une pompe m canique aliment e par le r acteur n 2 not e EDPy De m me que pour le circuit vert en cas de panne de ces deux pompes et si la vanne de priorit du circuit vert est ouverte le PTU alimente le circuit jaune en fournissant une partie de la puissance du circuit vert En cas de panne de r acteur la pompe m canique associ e ne fonction
186. nnexion entre les ports des noeuds AltaRica repr sentant les quipements reli s par ce tuyau Les connexions entre les composants fonctionnels qui nous int ressent permettent de propager l information de pr sence de fluide entre lesdits composants Aucun comportement AltaRica et par cons quent aucune d faillance n est associ ces connexions Or la plupart des composants impact s par les risques particuliers sont ces tuyaux Nous avons fait le choix pessimiste d associer l endommagement d un de ces tuyaux la d faillance simultan e de tous les composants du mod le AltaRica qui lui sont connect s Ainsi la perte du tuyau G Suction rsvg EDP reliant le r servoir vert la pompe verte est reli e avec la perte de rsvg et de EDPg De m me la perte du tuyau Y Suction rsvg EDP reliant le r servoir vert la pompe moteur jaune est reli e avec la perte de rsvy de mais aussi de la pompe moteur EMPy L allocation des composants du mod le AltaRica sur le mod le IRIS relie donc un ou plusieurs composants g om triques avec un ou plusieurs composants du mod le AltaRica L allocation choisie est d crite dans le tableau suivant 123 CHAPITRE 7 SYSTEME HYDRAULIQUE D UN AVION DE TYPE A320 Mod le IRIS G PV Mod le AltaRica PVg G ManifoldHP G HP TConnection HPManifold G HP TConnection PTU G HP PTU TConnection G HP T EDP PTU G HP EDP TConnection G HP Manifold PV EDPg PVe PTU G EDP EDPg G Suct
187. non seulement s re mais aussi optimis e Un crit re d optimisation int ressant se rait celui de la facilit d atteindre les composants de l avion pr sentant le plus fort taux de pannes et donc les plus sujets des activit s de maintenance Les activit s de maintenance repr sentant un co t tr s lev sur l exploitation d un avion de ligne le crit re de rapidit de maintenance est un crit re non n gligeable Il pourrait tre ais ment pris en compte dans notre analyse en injectant des contraintes suppl mentaires dans notre syst me de contraintes d allocation afin que les composants les plus sujets aux pannes soient dispos s dans les zones facilement accessibles de l avion Citons l exemple d un avion sur lequel une simple op ration de maintenance d applications logicielles n cessite le d montage de la structure avion et notamment le d montage des ailes Ce type d allocation des composants dans l avion pr sente un co t consid rable l exploitant Par cons quent le crit re de l accessibilit des l ments susceptibles de n cessiter des activit s de maintenance est un crit re d optimisation l gitime dans le choix d une allocation spatiale Common Cause Analysis 135 CHAPITRE 8 CONCLUSION 136 ANNEXE A MANUEL D UTILISATION DU MAPPINGMANAGER C 137 ANNEXE A MANUEL D UTILISATION DU MAPPINGMANAGER MapManager User Manual August 24th 2006 ONERA 1 A tool for
188. ntes SE sida ra EE ER Lae de m eRe Bee OR Ee me Perpa DER C Oy cae A PE ee eee ee eee Ge ed 83 1 Utiliser og SA RA we x 409 cR cE bod Re Dac Encore phis ISA conan a a ER A Manuel d utilisation du MappingManager 69 70 70 71 75 77 80 81 83 84 85 89 86 87 87 91 91 92 94 96 96 96 99 101 102 102 103 104 105 105 112 118 120 122 127 128 130 131 131 132 132 134 134 134 135 135 137 Bibliographie 149 Table des figures 1 1 2 1 2 2 2 3 2 4 2 5 2 6 2 7 2 8 2 9 3 1 3 2 3 3 3 4 3 5 3 6 3 7 3 8 3 9 3 10 3 11 3 12 3 13 3 14 3 15 3 16 3 17 3 18 3 19 3 20 3 21 3 22 3 23 4 1 4 2 4 3 4 4 4 5 4 6 4 7 Cycle de d veloppement selon PARP 4754 6 repr sentation graphique des composants AADL 15 Exemple de Reseaux de P tri P T 16 Exemple de franchissement de transitions d un r seau de Petri P T 17 Atelier ARICA MMC 18 Code Altarica et automate de comportement d un Capteur 20 Composition d automates de mode 21 Connexion d automates de mode 22 Exemple de repr sentation d un arbre de d faillances 25 Transformation d un automate de mode en un arbre de d faillances 26 Exemple d une relation d
189. ode commun qui sont susceptibles d affecter plusieurs fonctions r alis es par un syst me Par exemple deux fonctions dont les d faillances doivent tre ind pendantes ne doivent pr senter aucune nouvelles d faillances de mode commun les impliquant toutes les deux Par cons quent une fonction redond e ne doit tre impliqu e dans aucune d faillance de mode commun impliquant ses fonctions de redondance pour accroitre la s curit et donc r duire le risque de d faillance L utilisation d un quipement commun comme par exemple une source d alimentation lectrique par plusieurs fonctions est une source de d faillances de mode commun En effet la d faillance de l quipement commun va entrainer la d faillance des diff rentes fonctions qui l utilisent Une autre source de d faillances de mode commun est li e l installation dans l avion des qui pements d un syst me L impact sur les quipements de l clatement d un pneu ou d un moteur est calcul lors de l analyse PRA Particular Risks Analysis Dans ce cas on suppose que toutes les fonctions associ es aux quipements impact s par un d bris de pneu ou de moteur tombent en panne simultan ment CHAPITRE 1 INTRODUCTION Allocation of Aircraft Functions Systems System Level Failure FHA Sections Condition amp Effects Architectural Safety Requirements Failure Condition Effects Classification Separation
190. on 2 flow 3 Ini FailureType in 4 In2 FailureType in 89 CHAPITRE 6 LE SYSTEME DE SUIVI DE TERRAIN SDT D UN AVION DE CHASSE 5 Oui Beamdilmcin o 2 Oia 6 state 7 Status FailureType 8 assert 9 Out case 10 Ini erroneous and In2 erroneous erroneous 11 Ini correct and In2 correct p 12 else ostoi 13 edon Nous avons suppos pour cette tude que la fonction de consolidation n tait pas soumise des d faillances Le comportement de cette fonction est le suivant Si les deux entr es sont erron es alors la fonction produit une donn e erron e Si les deux entr es sont correctes alors la fonction produit une donn e correcte dans tous les autres cas la fonction est capable de d tecter qu au moins une des deux entr es est perdue ou incorrecte dans ce cas la fonction ne produit pas de r sultat Une fois que la correspondance entre chaque l ment du syst me avec un composant AltaRica est faite il ne reste plus qu interconnecter les composants AltaRica entre eux tout en respectant les connexions d j tablies entre les l ments du syst me Ces interconnexions vont ainsi permettre d obtenir un mod le fonctionnel d crivant le comportement global du syst me ayant la particularit de pouvoir tre test en pr sence de d faillances Une repr sentation graphique du Syst me SdT en AltaRica est propos e par l utilisation de l outil Cecilia
191. on de calcul ce composant permet a partir de plusieurs donn es d en produire une nouvelle Ce composant est associ aux fonctions VerAccComp ClAlarmComp et CommandeVol Fonction de consolidation ce composant permet de calculer une donn e consolid e a partir de deux donn es provenant de sources diff rentes Ce composant est associ ConsRollComp Flux de donn es ce composant permet de transporter des donn es chang es par des fonctions ce composant est associ toutes les flux de donn es du syst me SdT Ce regroupement de composants en diff rentes familles permet de factoriser les composants AltaRica utiliser et ainsi construire une biblioth que d l ments utiliser Sachant que les fonctions n utilisent pas le m me nombre de donn es pour le calcul de leur donn e elles sont regroup es selon le nombre de donn es qu elles utilisent Par exemple la fonction de calcul d une Acc l ration verticale VerAccComp requiert 3 donn es TerrainInfo SHeight et Speed pour calculer l ordre de Pitch renvoyer aux commandes de Vol Par contre la fonction calculant l alarme de d gagement n utilise que les donn es Alt et Vspeed Par cons quent m me si ces fonctions poss dent le m me niveau d abstraction du point de vue de leur comportement fonctionnel elles sont distingu es par des interfaces diff rentes Il est donc n cessaire de leur associer des composants diff rents Le code AltaRica pour
192. onn s dans cette zone Ce comportement permet de retrouver les d faillances et leurs effets du composant ress pr sent pr c demment En effet la d faillance correspondant la perte totale des quipements pr sents dans la zone repr sente bien l influence de la d faillance fail_lost et la d faillance qui influence le dysfonctionnement des quipements correspond bien aux effets provoqu s par fail_error Le composant AltaRica correspondant poss de autant de flux de sortie qu il a de connexions avec les autres zones par exemple un port 0 N pour repr senter sa connexion avec la zone du nord un port O_W pour rep senter sa connexion avec la zone situ e l ouest et il renvoie sur ses sorties l information d un ventuel impact Une repr sentation graphique pour un tel composant est donn e par la figure 3 17 42 3 3 MODELISATION DE L ARCHITECTURE MATERIELLE Fic 3 17 Exemple de repr sentation d une zone Le code AltaRica d un tel composant peut s crire ainsi 1 node Zone 2 flow 3 5 0 15 5 9 54 0 10 OLDE ou correct error LOs 4 sub 5 z ress 6 assert 7 ONE 6225 8 ORS SE 9 SETS 10 DEW 11 OSU 255 12 OR DE 20975 edon 1 node ress 2 state 3 S fal error 4 event 5 ages UD dar 6 trans 7 Jou lose le Fallos SEE ost 8 S correct failierror gt S error 9 S error u
193. ons l approche propos e une tude de cas de taille industrielle un syst me de g n ration et de distribution hydraulique d un avion civil Dans ce chapitre nous validons plus particuli rement les techniques de mod lisation et de v rification d allocation dans le cas particulier de l installation des quipements d un syst me au sein d un avion Enfin dans le chapitre de conclusion apr s un bilan des travaux effectu s dans cette th se nous comparons notre approche avec les travaux similaires existants Nous terminons en examinant quelques perspectives ouvertes par ce travail L CHAPITRE 2 TECHNIQUES POUR LA MOD LISATION ET LA V RIFICATION Ous commen ons par pr senter l int r t de la mod lisation et de la v rification formelle N de propri t s sur des mod les avant de d tailler chacune des tapes n cessaires la mo d lisation la formalisation des propri t s v rifier et enfin la v rification de ces propri t s sur le mod le Nous d clinons ensuite chacune de ces tapes dans notre domaine de la v rifi cation de propri t s de s ret de fonctionnement Nous formalisons le type de propri t qui nous int ressent puis abordons les principaux langages de mod lisation utilis s pour faire des analyses de stiret de fonctionnement avant de nous focaliser sur la d finition du langage AltaRica que nous avons choisi d utiliser dans nos travaux Nous terminons en listant les outils d analyse
194. onstruire le syst me de contraintes globales s ap pliquant notre syst me Une fois le syst me de contraintes complet nous utilisons l outil SATZOO pour traiter sa r solution Lorsqu une solution existe l outil SATZOO renvoie cette derni re sous forme d une valuation de l ensemble des variables du syst me correspondant l allocation trouv e 6 7 2 Visualisation de l allocation Pour simplifier la repr sentation du syst me une application d di e la visualisation des allocations propos es par SATZOO a t impl ment e Integer Linear Programming 96 N NMN 6 7 RECHERCHE ET VISUALISATION D ALLOCATION Cette application permet de visualiser rapidement une solution d allocation des fonctions sur les res sources mat rielles Lorsque SatZoo propose plusieurs solutions pour un m me syst me l application permet de faire d filer ces diff rentes allocations possibles afin de choisir celle pr sentant le plus d in t r t En effet suivant le crit re d optimisation choisi pour orienter le choix de la meilleure solution il se peut que plusieurs solutions aient la m me optimisation mais poss dent des allocations diff rentes Il est important que la s lection d finitive d une allocation soit r serv e aux personnes en charge de la r alisation du syst me Par cons quent lorsque plusieurs solutions sont disponibles il faut les pr server pour de nouvelles analyses manuelles de s lection
195. ont allou es sur une m me ressource Les composants de la voie MON 55 et MON sont eux aussi regroup s Les composants Interrup et Equals doivent pouvoir r cup rer des donn es provenant des deux voies distinctes Une premi re architecture v rifier est constitu e de trois ressources de calcul toutes connect es un m me bus Fic 3 19 Premi re Architecture pour le COM MON L allocation que nous souhaitons v rifier doit respecter plusieurs directives Celles que nous avons choisies sont les suivantes allocation du groupe correspondant la voie COM 51 et COM sur la ressource Sc allocation de la fonction Equals sur la ressource Rc allocation du groupe correspondant la voie MON 55 et MON sur la ressource Spy allocation de la fonction Interrup sur la ressource Rm Cette allocation peut tre illustr e par la figure suivante FIG 3 20 Une allocation possible pour le COM MON Cette architecture n est pas valable car il est facilement compr hensible que faire transiter toutes les donn es par une m me ressource de type Bus n est pas une bonne solution En effet le comportement erron de ce centralisateur de donn es suffit rendre inutiles les m canismes fonctionnels mis en place par l architecture fonctionnelle Ce comportement erron est atteint en pr sence de la d faillance Bus_alloc_fail_error 46 3 4 MODELISATION DE L ALLOCATION node Main e
196. ont directement appliqu es lors de la d claration des variables pour r duire les diff rentes combinaisons possibles En effet lors de la d claration des variables n cessaires notre pro bl me il est possible d instancier certaines variables afin de limiter les possibilit s d allocations Ainsi les directives d allocations allocation et exclusion sont directement appliqu es lors de l instanciation des variables Elles permettent ainsi de minimiser certaines variables d allocation du syst me en les transformant en constantes Nous avons d velopp un outil qui partant d une description de l architecture fonctionnelle et de l architecture mat rielle lorsque celle ci est disponible du mod le produit un ensemble de contraintes lin aires enti res pouvant tre trait es par un solveur de contraintes par exemple SATZOO Un descriptif d taill du fonctionnement de l outil est donn par la figure 4 6 Model ENT format 1 Fonctionel G n rateur de Contraintes Contraintes d Allocation Directives Visualisation Solveur de des Allocations Mod le Ar ILOGSolver LP Sk SatZoo Fic 4 9 Outil pour la recherche et la visualisation d allocations Voyons pr sent comment cet outil fonctionne sur l exemple du COM MON du chapitre pr c dent Les informations n cessaires et suffisantes extraire du mod le pour construire le syst me sont 62 4 6 RESOLUTION DU SYSTEME DE CONTRAINTES
197. ortie d un autre composant Be ee ee BAA node Main node A node B flow o bool out flow i bool in edon edon FIG 2 7 Connexion d automates de mode Pour que cette connexion soit valide il est n cessaire que ces variables soient ind pendantes c est dire que les variables d entr e n interviennent pas dans les calculs de la valeur de la variable de sortie Cette connexion doit tre d finie dans la rubrique assert du noeud p re Par exemple dans la figure 2 7 la connexion entre le noeud A et B est d finie dans la partie assertion du noeud Main La d finition formelle de la connexion d automates est nonc e ci apr s D finition 2 3 Soit A D Si FP F dom Xi Gi Li un automate de mode o F et i1 in telles que et i1 ip soient ind pendants et dom o C dom i1 dom o dom iz Soient Fi Fin i ip s dom S et I dom FI Notons I la valuation de telle que ofi 0 iy def si u Fi Is ofi ofi u a s I o sim n o dom F est une extension quelconque de la valuation F F sup Ff L automate de mode A 13 igp sont connect s o est l automate de mode Aofi o in D 8 F dom E 6 0 avec et o tels que Vs dom S I
198. part Il faut donc r it rer nos analyses pour tre s r que de nouveaux sc narios ne violent pas nos exigences 7 5 1 Nouvelles analyses Nous effectuons les analyses des exigences du syst me hydraulique avec le mod le qui contient les d faillances de cause commune calcul es par le MAPPINGMANAGER O Puis nous comparons les r sultats avec ceux obtenus avant la prise en compte de l allocation spatiale de fa on d terminer si l allocation est acceptable Nous avons tudi la hit list comprenant les trajectoires associ es aux clatements des 4 pneus du train d atterrissage central Les r sultats suivants ont t obtenus avant allocation apr s allocation Er t mm Observateur simple double proba simple double proba T 4 4 2 d44 4 4 Pdistb 12 0 4 8 e 4 14 0 7 1 e 4 NPdistb 13 1 5 8 e 4 15 1 8 1 e 4 Pdisty 1 222 1 0 e 4 12 304 4 9 e 4 NPdisty 13 23 4 0 e 4 27 23 8 6 e 4 Pdistg 1 232 1 0 e 4 13 297 5 1 e 4 NPdistg 3 218 3 0 e 4 15 279 7 0 e 4 T 4 4 2 2 d44 4 4 YBPhyd 0 12 4 8 e 8 0 168 3 5 e YBNPhyd 0 170 2 4 e 7 0 406 7 1 e 7 7 5 VERIFICATION DE L ALLOCATION SPATIALE GYPhyd 0 201 1 1 e 7 10 299 3 8 e 4 GYNPhyd 0 243 2 3 e 7 10 350 3 8 e 4 GBPhyd
199. pdate gt S correct 10 init 11 S correct 12 edon Ces composants mod lisant les diff rentes zones d un avion ainsi que les connexions permettant de les relier facilitent la repr sentation d un avion sous la forme d un graphe de zones adjacentes Un exemple de graphe est donn par la figure suivante Fic 3 18 Repr sentation possible des zones d un avion 43 CHAPITRE 3 MOD LISATION ET ANALYSE DE L ALLOCATION 3 4 Mod lisation de l allocation Lorsque nous mod lisons en AltaRica la relation d allocation nous souhaitons observer le compor tement de l architecture fonctionnelle en pr sence de d faillances mat rielles Nous construisons tout d abord un mod le global bas sur les d faillances des composants de l architecture fonctionnelle et des composants de l architecture mat rielle Ces d faillances n ont ce stade de la mod lisation aucune liaison La relation d allocation permet donc de relier ces diff rentes d faillances pour illustrer l in fluence des architectures dans un mod le commun En effet les seules d faillances observables taient des d faillances l mentaires sur les fonctions qui composent notre syst me En ajoutant la relation d allocation notre mod le nous construisons un mod le global enrichi par des relations entre les d faillances des mod les des architectures fonctionnelles et mat rielles La relation d allocation permet de repr senter l
200. ponent B HP Distribution 2 fm impacted description MBlue High Pressure Distribution Tine second part gt lt failmode component B HP Distribution 3 fm impacted description Blue High Pressure Distribution line lt failmode component Y EDP fm impacted description Yellow Engine Driven Pump gt lt failmodes gt 125 CHAPITRE 7 SYSTEME HYDRAULIQUE D UN AVION DE TYPE A320 lt failmodes name Functional gt lt failmode component EDPy fm fail_Loss internal MA320 Hyd EDPy description Yellow Engine Driven Pump gt lt failmode component Pdistb fm fail_leakage internal MA320 Hyd Pdistb description Blue Priority distribution gt lt failmodes gt Grace cet outil il est possible de faire correspondre n l ments g om triques avec m l ments fonctionnels Nous avons choisi d utiliser le format xml pour repr senter une allocation Dans l exemple suivant nous supposons que la liste des composants du monde g om trique est charg e dans la partie gauche de l outil et elle est appel e Geometrical De m me la liste des composants fonctionnels est charg e dans la partie droite et est appel e Functional Ce fichier est constitu d une s rie d allocations map Chaque allocation comprend tous les noms des composants mis en relation Pour chaque composant plusieurs champs doivent tre renseign s le champ component donn
201. ptimisable selon ses propres crit res La d finition des contraintes d allocation ne constituant pas une tape du processus actuel de d veloppement d crit par PARP 47696 nous nous sommes ensuite int ress s la d duction de ces contraintes d allocation partir de l expression des exigences de s ret de fonctionnement Nous avons pour cela propos une m thode d interpr tation des exigences de s ret de fonctionnement en contraintes d allocation tenant compte la fois des classes de criticit des exigences et des composants du syst mes concern s par les exigences Cette g n ration automatique de contraintes d allocation depuis des exigences de s ret de fonctionnement nous permet ensuite de d finir une allocation satisfaisant les contraintes et par cons quent les exigences de s ret de fonctionnement Pour d finir une allocation nous proc dons de mani re it rative sur le nombre de ressources n cessaires pour atteindre la satisfaction de toutes les 131 CHAPITRE 8 CONCLUSION contraintes Nous optimisons ainsi le crit re nombre de ressources Nous avons ensuite mis en oeuvre les m thodes propos es sur deux tudes de cas de syst mes avioniques r els Nous avons appliqu la m thode int gr e de d finition d allocation satisfaisant des exigences de s curit sur un syst me de Suivi de Terrain d avion de chasse L allocation consid r e ici est l allocation de fonctions sur des r
202. qualitative 4 cette situation En revanche nous fixons un taux d occurrence inf rieur 107 par heure de vol pour cette situation 7 3 Mod lisation de l architecture fonctionnelle du syst me hydrau lique Les choix de mod lisation du syst me sont influenc s par les types d analyses que nous souhaitons faire sur ce dernier En effet l id e premi re tait de combiner deux outils de mod lisation IRIS et OCAS afin de proposer une analyse compl mentaire La mod lisation du syst me d di e aux ana lyses d impact tant d j effectu e il est important d extraire certaines informations utiles pour cette nouvelle mod lisation mod lisation fonctionnelle peut s agir par exemple des l ments mod lis s de leur nombre de leurs connexions etc Le choix des l ments consid r s du mod le d terminent le niveau de d tail obtenu pour le mod le fonctionnel Une fois tous les composants importants identifi s il faut leur associer un comportement suffisam ment abstrait afin d obtenir un mod le facilement analysable pour viter l explosion combinatoire tout en conservant un comportement proche du syst me r el 7 3 1 Mod lisation des l ments du syst me Hydraulique La mod lisation de ce syst me doit permettre de visualiser l influence d une panne sur le syst me global pour ainsi observer la r action du syst me face un composant d failant Pour cela nous associons aux diff rents composants un comportemen
203. r valuer l impact d une allocation sur la s curit d un syst me Nous montrons comment mod liser les architectures fonctionnelles et ma t rielles ainsi que les relations d allocation qui les relient Nous illustrons toutes les notions introduites dans ce chapitre sur l exemple simple de l architecture COMmand MONitoring Dans le chapitre 4 nous pr sentons une m thode de g n ration automatique d allocations Nous montrons comment mod liser sous forme de contraintes les architectures fonctionnelles mat rielles et les directives d allocation Les diff rents types de directives d allocation consid r es sont pr sent s dans ce chapitre A nouveau l architecture COM MON est utilis e pour illustrer l approche propos e Dans le chapitre 5 nous montrons comment d river les directives d allocation partir de r sultats d analyse obtenus sur la base d un mod le de l architecture fonctionnelle Nous tudions galement le cas o il n est pas possible de trouver une allocation s re et nous montrons comment modifier l architecture mat rielle de facon pouvoir trouver des allocations s res Dans le chapitre 6 nous appliquons l approche pr sent e dans les chapitres pr c dents au syst me de Suivi de Terrain d un avion de chasse Nous illustrons l ensemble des techniques propos es de fa on rechercher une allocation s re des fonctions de ce syst me sur une architecture mat rielle informatique Dans le chapitre 7 nous valid
204. r de la donn e est erron e 3 lost la valeur de la donn e n est pas produite Les volutions possibles de ces comportements peuvent tre mod lis es en AltaRica de la fa on suivante 1 node fonct 2 state s correct error lost 3 flow 4 Dont IOS tI Salat 6 event y fail error 8 JL 9 trans 10 MOT CSS los los gt BSOS 11 s correct fail error gt 3 error 12 assert 13 01 case 14 Corret 39 15 15 else s 16 Fe 17 init s correct 18 edon Nous obtenons de la m me mani re le code AltaRica des autres fonctions La traduction du syst me complet passe par la cr ation d un noeud Main qui permet d interconnecter les diff rentes fonctions Vaide de relations entre les variables de flux des composants AltaRica correspondants 34 3 2 MODELISATION DE L ARCHITECTURE FONCTIONNELLE node Main node COM node Interrup edon edon node Equals edon FIG 3 4 Repr sentation du noeud Main du COM MON Les connexions entre les diff rents noeuds du graphe fonctionnel doivent tre report es sur le mod le AltaRica Ainsi chaque arc du graphe doit tre repr sent par une liaison entre mod les AltaRica De plus le graphe fonctionnel tant orient les liaisons cr es doivent de m me orienter leur flux Finalement pour tout arc appartenant l ensemble f cnx des arcs entre les fon
205. rchitecture d un avion de type A380 BBC 08 99 CHAPITRE 6 LE SYSTEME DE SUIVI DE TERRAIN SDT D UN AVION DE CHASSE 100 L CHAPITRE 7 SYST ME HYDRAULIQUE D UN AVION DE TYPE A320 Ous appliquons au syst me hydraulique d un avion civil la technique de mod lisation et N validation de l allocation des quipements dans les zones d un avion qui a t pr sent e dans le chapitre 3 Cette technique de mod lisation se repose sur le couplage de mod les d crivant le m me syst me mais construits l aide de langages diff rents AltaRica pour la s ret de fonctionnement et TRIS Air00 pour l installation des quipements au sein de l avion SOMMAIRE Tal D MSECHE gt 5 44 Ds a Ds eee ATS a sl 102 7 2 PRESENTATION DU SYSTEME 4515303 4 40 90 8 Aa A 102 dl o DESCO acs v LL XXX 9 AEE ww 9 SS DNA HERE bee d A 103 TZA s Crises E Lu s ek ee ce Tee RD A D 104 7 3 MOD LISATION DE L ARCHITECTURE FONCTIONNELLE DU SYST ME HYDRAULIQUE 105 7 3 1 Mod lisation des l ments du syst me Hydraulique 105 732 Validation di mod le se o ayaat ysk EOS USUS OS nsn 112 7 2 4 Mod lisation g om trique escada ode kk ee 118 7 34 Les l ments impact s sous forme de Hitlist 120 7 4 MOD LISATION DE L ALLOCATION SPATIALE ia 4 2 4 44444 ia 4 4
206. re les composants est permise gr ce diff rents ports sur les composants Un port est un point d entr e et ou de sortie d un composant par o peuvent transiter des donn es data des v nements event ou m me des v nements associ s des donn es data event Une connexion permet de relier deux ports soit les ports de deux sous composants soit le port d un sous composant avec le port du composant le contenant Les v nements peuvent d clencher un changement de mode de comportement d un composant En effet les modes modes permettent de mod liser la reconfiguration du syst me Ces changements de modes permettent de repr senter des architectures dynamiques certains composants peuvent tre activ s ou d sactiv s en fonction du mode Le langage AADL est con u pour d crire des architectures statiques avec des modes op rationnels pour leurs composants N anmoins le langage de base peut tre tendu afin de permettre l utilisateur d ajouter des informations suppl mentaires l architecture Les mod les d erreur AADL sont une extension qui a pour objectif de permettre la r alisation d analyses qualitatives et quantitatives de s ret de fonctionnement Le AADL Error Model Annex AW05 d finit un sous langage qui per met la d claration de mod les d erreur qui seront instanci s et associ s chaque composant du syst me Ce langage permet d analyser l impact des choix architecturaux sur les exigences du s
207. repr sente dans un m me mod le l ar chitecture fonctionnelle et l architecture mat rielle partir du mod le global il est possible d effectuer de nouvelles analyses Par exemple il est possible de valider des exigences quantita tives ou des exigences qualitatives en prenant en compte l effet des d faillances des ressources mat rielles autoris par l allocation Description Description fonctionnelle mat rielle cr Directives mm Mod le Mod le fonctionnel architecture fifi Mod le global i R solution R sultats d analyse e e G e m m m ma Fic 5 4 Technique d obtention d une allocation Les exigences quantitatives permettent de d finir une probabilit de d faillance dangereuse pour une situation redout e Cette probabilit est calcul e en fonction de la probabilit associ e chacune des d faillances des ressources de l architecture mat rielle et en fonction de l allocation En effet 76 5 3 ADAPTATION DE L ARCHITECTURE MATERIELLE suivant l allocation choisie les combinaisons de d faillances mat rielles menant la situation redout e varient et par cons quent la probabilit d apparition de la situation redout e volue suivant le choix de l allocation analys e Ces exigences ne peuvent donc tre v rifi es qu une fois le choix de l allocation tabli Une deuxi me analyse rendue poss
208. respondants AIRBUS outil d velopp pendant la th se pr sente page 137 fichier correspondant aux r sultats des analyses du mod le IRIS cf section 7 3 4 122 10 gt 7 4 MODELISATION DE L ALLOCATION SPATIALE Nous disposons de deux listes de composants pour le syst me hydraulique l une provenant du mod le IRIS et l autre du mod le AltaRica Ces deux listes ne se correspondent pas une une en effet les deux mod les ne d crivent pas avec le m me niveau de d tail certains aspects Le mod le g om trique se focalise sur les quipements les plus encombrants comme les r servoirs ou les canali sations hydrauliques Il d crira avec beaucoup de d tail le cheminement du fluide depuis le r servoir jusqu aux consommateurs En revanche certains m canismes peu encombrants comme la valve de priorit peuvent ne pas tre d crits dans les mod les de pr installation Le mod le AltaRica se focalise sur les composants ayant une importance particuli re du point de vue de la s ret de fonctionnement soit parce qu ils sont la source de probl mes comme par exemple les fuites des consommateurs du syst me hydraulique soit parce qu ils contribuent renforcer la s ret du syst me comme le compo sant Power Transfer Unit Mais dans le mod le AltaRica du syst me hydraulique nous avons choisi de repr senter les diff rents tuyaux qui permettent le transport du fluide hydraulique par un simple lien co
209. rit de la ligne bleue Toutes les probabilit s calcul es sont galement acceptables ce qui permet de fixer comme objectifs de d veloppement pour les concepteurs des quipements du syst me hydraulique le taux d occurrence d une perte d quipement doit tre inf rieur 107 par heure de vol et le taux d occurrence d une fuite de l quipement doit tre inf rieur 10 par heure de vol Bien entendu il est possible qu un quipement ne puisse pas tenir cet objectif g n ral Il est ais de modifier le mod le AltaRica en tenant compte du taux de d faillance r el des quipements de fa on calculer nouveau les taux de d faillances pour valuer s ils sont acceptables 7 3 3 Mod lisation g om trique Le mod le g om trique correspond une repr sentation en trois dimensions du syst me hydraulique Cette repr sentation permet donc de visualiser le syst me tout en conservant certaines caract ristiques comme par exemple la taille des diff rents composants constituant le syst me ou la distance qui les s pare Ces caract ristiques sont importantes lors des choix d installation de ces composants dans l avion Par exemple des exigences li es aux interactions lectromagn tiques imposent une distance minimale entre quipements Un autre exemple d exigence recommande de ne pas installer de cables lectriques en dessous de canalisations hydrauliques Finalement certaines exigences d installation sont li es l
210. rmi les techniques classiques les plus utilis es pour l analyse de s ret de fonctionnement d un syst me la simulation et la m thode d analyse par arbres de d faillance sont les plus r pandues car elles sont simples mettre en oeuvre Les Arbres de D faillances L analyse par Arbre de D faillances AdD permet de repr senter sous forme arborescente les di verses combinaisons possibles d v nements qui conduisent la r alisation de l v nement redout repr sentant le sommet de l arbre Cette m thode est d ductive et la construction d un arbre de d faillances effectu e de mani re ascendante par combinaison de portes logiques et d v nements l mentaires qui m nent au sommet D finition 2 5 Un arbre de d faillance est d fini comme un 1 graphe orient ayant la propri t d arbre connexe et sans cycle dont les noeuds sont soit des op rateurs logiques soit des v nements le noeud racine est l v nement sommet not S v nement redout les noeuds terminaux feuilles sont des v nements de base notes bj La repr sentation graphique de l arbre permet de repr senter les niveaux successifs comme une condition logique sur les v nements du niveau inf rieur l aide d op rateurs logiques ET OU etc Un exemple de repr sentation d arbre de d faillances est propos en figure 2 8 L exemple repr sente la formule logique C A V B menant l v nement redout E 2
211. rue true o false L false I true true capt out dom capt out true false Un syst me tout comme son mod le est un assemblage de composants l mentaires Les com posants peuvent tre assembl s par connexion regroupement ou bien par synchronisation Voyons 20 2 2 MODELISATION ET VERIFICATION DE LA SECURITE DES SYSTEMES AERONAUTIQUES pr sent plus en d tails ces diff rents moyens d assemblage de composants d finis par les automates de mode Hi rarchie asynchrone d automates de mode La composition d automates de mode consiste placer plusieurs automates de mode dans un m me automate une m me vue afin de pouvoir ensuite les faire communiquer et interagir tant qu ils n interagissent pas entre eux les noeuds caract ris s par un automate de mode sont consid r s comme ind pendants Le r sultat d une composition d automates de mode est un automate de mode regroupant les d finitions de tous les automates de mode compos s cf figure 2 6 FIG 2 6 Composition d automates de mode La d finition formelle de cette composition est la suivante D finition 2 2 Soient A1 An n automates de mode avec D Si Fi F dom Xi i o li Supposons que leurs vocabulaires soient distincts Vi j 1 lt lt j lt n SUEFUES N S U FEP U Fett 0 La composition parall le de n automates A1 An est un automate de mode not
212. s autoris es par les contraintes Le probl me de satisfaction de contraintes CSP consiste trouver une affectation de valeurs l ensemble des variables appel e instanciation des variables telle que toutes les contraintes soient satisfaites Solutions possibles Fic 4 1 Solutions respectant les contraintes Exemple de programmation par contraintes Prenons l exemple de CSP connu du placement de plusieurs reines sur un chiquier que l on pourrait transcrire en un probl me d allocation de reines sur un chiquier tout en respectant un ensemble d exigences Le probl me des W Reines consiste placer n reines sur un chiquier n x n sans qu elles se menacent cf figure 4 2 Les contraintes associ es ce probl me sont que deux reines ne doivent pas se trouver sur la m me ligne sur la m me colonne ou sur la m me diagonale 52 4 1 MODELISATION ET APPROCHE PAR CONTRAINTES WY 777 777 Lp ERY Fic 4 2 Probl me des W Reines Une mod lisation possible du probl me consiste associer pour chacune des cases une variable prenant la valeur 1 si la reine est pr sente sur la case et la valeur 0 sinon On notera X la variable qui repr sente la case correspondante la ligne 4 et la colonne j de l chiquier Les contraintes sp cifient qu il ne peut y avoir plus d une reine sur une m me ligne sur une m me colonne ou sur une m me diagonale Le csP de ce probl me devient le suivant
213. s from the Geometrical or from the Functional world component is the name of the impacted component and fm is the failure mode associated to this component All optional attributes found in the component lists are stored in the mapping lt mapping name A320 Hydraulic Light left Geometrical right Functional gt lt map name Yellow Engine Driven Pump gt lt failmode world Functional component EDPy fm fail_loss internal MA320 Hyd EDPy description Yellow Engine Driven Pump gt lt failmode world Geometrical component Y EDP fm impacted description Yellow Engine Driven Pump gt lt map gt map name Blue Priority Distribution failmode world Functional component Pdistb fm fail leakage internalZ MA320 Hyd Pdistb description Blue Priority Distribution line failmode world Geometrical component B HP distribution 1 fm impacted description Blue High Pressure Distribution line first part gt failmode world Geometrical component B HP distribution 2 fm impacted description Blue High Pressure Distribution line second part failmode world Geometrical component B HP distribution 3 fm impacted description Blue High Pressure Distribution line third part gt lt map gt lt mapping gt Fail Set A fail set file contains several failure sets each failure set is made of a list of failure modes and a list of trajector
214. s de vol et seules des combinaisons d au moins deux d faillances peuvent conduire cette situation 1 Pitch erron non d tect Pas d alarme de d gagement lorsque l angle de tangage est erron Dans l tat actuel de mod lisation les diff rents sc narios qui nous m nent cette situation sont les suivants Number of minimal cuts 5 Non_detect Dut true ClAlarmComp fail_lost Navigation fail_error ClAlarmComp fail_lost Radar fail_error ClAlarmComp fail_lost amp TFTAPanel fail error C ClAlarmComp fail lost amp VerAccComp fail error C ClAlarmComp fail lost Rolli fail error amp Roll2 fail error Tous ces sc narios comportent au moins deux d faillances dont la d faillance de la fonction de calcul de l alarme de d gagement tant donn que cette situation est consid r e comme Catastrophique il ne faut pas que les sc narios impliquent moins de deux d faillances Il faut donc que les composants qui sont impliqu s dans un sc nario de deux d faillances soient ind pendants Nous d rivons donc les hypoth ses d ind pendance suivantes idpt ClAlarmComp Navigation idpt ClAlarmComp Radar idpt ClAlarmComp TFTAPanel idpt ClAlarmComp VerAccComp Le dernier sc nario est particulier puisqu il est de taille 3 il suffit donc que deux parmi les trois composants impliqu s dans ce sc nario soient ind pendant nous
215. s m thodes formelles et de la s ret de fonctionnement PhD thesis LaBRI Universit Bordeaux 1 January 2000 POINT ET A RAUZY Altarica constraint automata as a description language European Journal on Automation 1999 Special issue on the Modelling of Reactive Systems A RAUZY Altarica ToolBox Combava http www arboost com altarica page htm A Rauzy Mode automata and their compilation into into fault trees Reliability Engineering and System Safety 78 1 12 2002 A E RUGINA KANOUN ET KAANICHE Mod lisation de la s ret de fonction nement de syst me a partir du langage aadl Rapport LAAS 2006 A E RUGINA System dependability evaluation using aadl Dans liere Rencontres Jeunes Chercheurs en Informatique Temps R el RJCITR 2005 September 2005 A RAUZY ET Y DUTUIT Exact and truncated computations of prime implicants of coherent and non coherent fault trees within aralia Reliability Engineering and System Safety 58 1997 151 5406 18807 Tho06 Ver06 Vin03 Yam95 SAE AS5506 1 Architecture analysis and design language annex volume 1 Error Model Annex 2006 L SAGASPE ET P BIEBER Constraint based design and allocation of shared avionics resources Dans 26th Digital Avionics Systems Conference 2007 P THOMAS G n rateur de s quences et autres outils bas s sur un stepper Rapport Technique Dassault Aviation 2006 T VERGNAUD Mod lisation de syst mes te
216. s pour cette compilation un premier concernant les outils qui sont plus efficaces sur des mod les bool ens et un second sur la g n ration automatique d arbres de d faillances partir d une repr sentation de haut niveau rendant ainsi la maintenance plus ais e L algorithme naif possible pour d crire le principe fonctionne sur l ensemble des tats accessibles de l automate 1 La repr sentation hi rarchique du syst me est mise plat en un seul automate de mode 2 Le graphe des tats accessibles est calcul 3 Les diff rents chemins menant aux tats redout s sont calcul s 4 Les chemins sont transform s en branches d un arbre de d faillances c f figure 2 9 Une branche est la conjonction des d faillances qui apparaissent sur un chemin L arbre est la disjonction des formules qui correspondent aux chemins 25 CHAPITRE 2 TECHNIQUES POUR LA MODELISATION ET LA VERIFICATION B y b c FIG 2 9 Transformation d un automate de mode en un arbre de d faillances Actuellement il existe deux algorithmes qui optimisent l algorithme pr sent pr c demment celui d Antoine Rauzy d taill dans Rau02 et celui de Philippe Thomas auteur de l algorithme utilis par l outil OCAS pour son g n ra teur d arbre Mais malheureusement il n existe pas de publication pour nous informer sur son fonctionnement L analyse par arbre de d faillance est largement utilis e dans les tudes
217. s that were created The mapping manager detects unmapped items components that do not belong to any mapping empty mapped items components that belong to a mapping that contains no other component and multiple mapped items components that belong to several mappings If at least one of these situations is detected a pop up window is created that provides the list of unmapped empty mapped and multiply mapped items with an indication of the mappings that might have to be corrected A file called mapping_name log is automatically created that contains all these data when the analysed mapping is called saved 2 9 mapping_name xml The sanity check is also automatically performed whenever a mapping is Create Automatically mapping suggestions Mappings can be proposed automatically when sufficient information is provided in the component lists For instance we could consider that the component description includes an extra attribute zone that indicates in which zone of the aircraft the component is located This attribute can be used to group lt fail lt fail lt fail lt fail lt fail lt fail component failure modes together modes name a320_fx1_zone gt Imode component PVg fm fail loss zone WheelWell gt Imode component EDPg fm fail loss zone LeftWing gt mode component rsvg fm fail loss zone WheelWell1 gt Imode component NPdistg fm fail loss zone LeftWing gt Imode component P
218. s utilisons l allo cation qui a t mod lis e avec le MAPPINGMANAGER O L analyse de l allocation doit permettre pour chaque quipement impact dans la Hitlist de trouver son ou ses correspondants dans le mod le AltaRica L outil MAPPINGMANAGER C g n re automatiquement toutes les d faillances de causes communes qu il faut ajouter au mod le AltaRica Une fois la mise en correspondance des 2 mod les tablie l int gration des analyses d clatements consiste ajouter des synchronisations sur les v nements des composants AltaRica correspondants Pour chaque ligne histlistitem du fichier Hitlist Hl et pour chaque quipement im pact nous utilisons le fichier d allocation g r par le MAPPINGMANAGER pour identi flier le ou les composants correspondants aux composants g om triques Par exemple le histlistitem intitul fail tyre burst W4 Theta minusib5 9 Kappa 127 135 impacte les quipe ments G HP distribution 2 et Y Suction rsvy EDP L allocation pr sent e plus haut relie le com posant G HP distribution 2 avec les composants Pdistg NormBrakes RevEngi Yawdamperl FlapsR Rudderg spoileri Stabilizer elevatori aileronR et spoiler5 et le composant Y Suction rsvy EDP avec rsvy EDPy et EMPy Cette m thode construit pour chaque histlistitem un vecteur de synchronisation Vayne des v nements des composants AltaRica correspondants Par exemple un nouvel v nement global nomm fail_tyre_burst_W4_Theta_minus15_9
219. sant qu il soit un composant de calcul ou de communication poss de le comportement d une ressource ress d fini pr c demment Cette sp cification est possible en utilisant la notion de hi rarchie en AltaRica Elle permet d inclure dans un composant un composant d j d fini Dans la mod lisation de l architecture mat rielle nous souhaitons que la ressource informe les autres ressources connect es de son tat interne Ce comportement est possible en consid rant que la sortie du composant n est utilis e que pour renvoyer l tat de la ressource incluse 01 renvoie la valeur de ress S 40 3 3 MODELISATION DE L ARCHITECTURE MATERIELLE Ri Ii 01 Fic 3 13 Exemple de repr sentation d une ressource La connexion de vers Bus est repr sent e dans la figure 3 14 par une fl che bidirectionnelle Cette fl che permet d exprimer graphiquement que la connexion s effectue dans les deux sens de R4 vers mais aussi de Bus vers Lors de la mod lisation en AltaRica il faut donc ajouter pour chaque liaison entre les composants un port repr sentant une connexion entrante et un port repr sentant une connexion sortante Fic 3 14 Exemple de connexion entre les ressources Le code AltaRica correspondant aux ressources du groupe G1 est le suivant 1 node CPU1 2 flow 3 correct error losti 4 correcte error lost 5 sub 6 r ress 7 assert 8 01 case r s correct Ii 9 Glee 2 8
220. se deux autres types de synchronisation la Diffusion et la DCC D faillance de Cause Commune Le type de synchronisation Diffusion correspond a un broad cast sur les gardes de tous les v nements synchronis s et n est d clenchable que si au moins l une des gardes des v nements synchronis s est vraie Avec ce type de synchronisation seuls les v nements ayant leurs gardes vrai sont d clenchables Mais avec la synchronisation de type Diffusion il n est pas possible de tirer les v nements individuellement Le type de synchronisation DCC correspond aussi un broadcast sur les v nements synchro nis s mais avec ce type il est possible de tirer les v nements individuellement Afin d illustrer les diff rents types de synchronisation prenons un exemple deux v nements e_a et e_b sont synchronis s par un nouvel v nement nomm sync_ab Consid rons que pour chaque v nement il existe une garde g et une affectation A La garde d crit les conditions satisfaire pour tirer l v nement tandis que l affectation repr sente les actions effectuer sur les variables en cas d occurrence de l v nement Les deux v nements sont donc d finis de la mani re suivante g a l gt A g_b l e_b gt X_b Ab 23 CHAPITRE 2 TECHNIQUES POUR LA MODELISATION ET LA VERIFICATION Pour r sumer suivant le type de synchronisation consid r cel
221. ses de performances et de s ret de fonctionnement Ces derni res se basent sur la synth se d arbres de d faillance partir du mod le Ce langage est aujourd hui principalement employ pour la 133 CHAPITRE 8 CONCLUSION mod lisation de syst mes automobiles La principale restriction de cette m thode est qu elle ne s applique qu des mod les statiques par exemple la mod lisation des communications entre les ressources est unidirectionnelle et pour exploiter les arbres produits un certain nombre d abstractions est n cessaire Or le langage AltaRica permet la fois de mod liser les syst mes statiques et de mod liser des syst mes dynamiques lorsque leur comportement devient trop complexe En effet les diff rents outils d exploitation de mod les AltaRica permettent d extraire des coupes de d faillances menant une situation observ e partir de mod le statiques et dynamiques 8 2 2 D finition d allocation par r solution de contraintes Dans HCDJ06 CHD 04 HCDJOS les auteurs pr sentent une approche bas e sur la program mation par contraintes permettant de guider la d finition d une architecte de syst me temps r el dans l allocation de t ches p riodiques sur des process distribu s Tandis que dans le cadre de nos travaux les contraintes tudi es sont du type deux t ches doivent tre ind pendantes qui sont traduites en contraintes d allocation du type ind pendance entre les r
222. sfonctionnement de la fonction entrainant la production d une donn e incorrecte 33 CHAPITRE 3 MOD LISATION ET ANALYSE DE L ALLOCATION 2 L tat lost repr sente un dysfonctionnement qui m ne l absence de donn e Lorsque la fonction est dans cet tat elle n est plus capable de fournir de donn es De la m me mani re une repr sentation particuli re du type de donn es doit tre impos e dans la mod lisation En effet suivant les choix de mod lisation la repr sentation des changes d informations peut diff rer En AltaRica ces changes d informations sont mod lis s par des flux de donn es permettant une visualisation de la propagation de ces donn es dans le syst me Par exemple dans un syst me r el g n ralement les capteurs fournissent une donn e en fonction de leur mode de fonctionnement En effet un capteur fonctionnant correctement fournit en permanence une donn e correcte Si ce dernier tombe en panne soit il ne fournit plus aucune donn e soit il fournit des donn es erron es Nous avons choisi de ne pas repr senter la valeur r ellement produite par la fonction mais plut t d tudier une valeur abstraite qui d note l occurrence d une d faillance A partir de cette constatation nous avons mod lis en AltaRica cette valeur abstraite l aide d un type num r pouvant prendre 3 valeurs distinctes 1 correct la donn e n a pas subi de d faillance 2 erroneous la valeu
223. sment et CCA Common Cause Analysis Ces quatre analyses ne repr sentent en fait qu une m me analyse globale mais elles portent sur diff rents niveaux de maturit de la d finition du syst me FHA Cette analyse est initi e au tout d but du processus Elle identifie les diff rentes situations redout es dites FC Failure Conditions associ es aux diff rentes fonctions r alis es par les syst mes d un avion L ensemble de ces situations contr ler est construit partir des d faillances consid r es pour chaque constituant du syst me Dans un premier temps les seuls modes de d faillance consid rer sont la perte et le fonctionnement erron des constituants du syst me Ensuite chacune des situations redout es est class e selon sa gravit La d finition de la classification de gravit criticit est donn e par le tableau 1 1 Ces niveaux de criticit se d clinent depuis le niveau mineur impact peu cons quent sur le bon d roulement d un vol jusqu au niveau catastrophique Pour tre acceptable la probabilit d une d faillance du type catastrophique ne doit d passer 107 par heure de vol Classe Effet de la d faillance Prosa Objectif Catastrophic L avion ne peut voler de fa on s re perte de l avion de 10 9 CAT l quipage et des passagers Hazardous R duction importante des marges de s curit ou des fonctions HAZ augmentation trop importante de la charge de travail
224. source Pour cela nous ajoutons au syst me les contraintes suivantes coloc_S1i_COM 1 coloc_S2_MON 1 coloc_Interrup_Equals 1 Tl y ait une ind pendance entre COM et MON et par cons quent il y ait aussi ind pendance entre Sl et 52 63 CHAPITRE 4 RESOLUTION DE CONTRAINTES D ALLOCATION idpt_COM_MON 1 idpt_S1_S2 1 Partant de ce d but de syst me il suffit de le compl ter avec les diff rentes contraintes pour ainsi obtenir le syst me d quations lin aires Voyons pr sent comment construire les quations partir des contraintes nous ne traiterons pas l ensemble des fonctions mais nous nous focaliserons sur les quations construites partir de la fonction COM Placement set allocation COM allou e sur une seule ressource alloc_COM_SM alloc_COM_RM alloc_COM_SC 1 Ind pendance Pour l ind pendance entre COM et MON alloc_COM_SM alloc_MON_SM lt 1 alloc_COM_RM alloc_MON_RM lt 1 alloc_COM_SC alloc_MON_SC lt 1 Co localisation Il MEOW la localisation de COM Sl alloc_COM_SM alloc_Si_SM lt 0 alloc_COM_SM alloc_Si_SM lt 0 alloc_COM_RM alloc_Si_RM lt 0 alloc_COM_RM alloc_S1_RM lt 0 alloc_COM_SC alloc_S1_SC lt 0 c alloc_COM_SC alloc_Si_SC lt 0 Connexion Pour la liaison fonctionnelle entre Si et COM alloc_Si_SM allo
225. ssi appel Combava d Antoine Rauzy Rau Cette ToolBox rassemble plusieurs outils communs 4 OCAS et SIMFIA et permet en outre de faire du model checking L IRCCyN a aussi d velopp une extension temps r el d AltaRica Pag04 CPR04 bas e sur les automates contraintes temporis s qui se compilent en automates temporis s L outil Tarc permet de r aliser cette compilation Enfin le LaBRI d veloppe des outils bas s sur le langage d origine Le model checkeur V 18 2 2 MOD LISATION ET VERIFICATION DE LA S CURIT DES SYST MES AERONAUTIQUES utilise le formalisme des BDD afin d optimiser la v rification de formules de u calcul et il est maintenant int gr dans ARC LaB07 L utilisation du model checking permet de s assurer du parcours complet du graphe des tats accessibles 2 2 3 Pr sentation d taill e du langage choisi AltaRica Data Flow Concepts Pour la mod lisation du syst me en AltaRica certaines r gles de conception de composants sont d finies Les concepts utilis s ci apr s sont illustr s sur un exemple trivial de mod le repr sentant le comportement d un Capteur Un composant mod lis est repr sent par un noeud node caract ris par son nom Sensor dans notre exemple figure 2 5 Un noeud poss de au moins une variable d tat state dont la valeur d note le fonctionnement ou dysfonctionnement du composant La valeur de cette variable l tat initial est sp cifi e
226. st me Observons tape par tape ce sc nario pour d terminer les corrections apporter au syst me pour qu il puisse tenir les exigences de s ret de fonctionnement La figure 7 14 montre le syst me hydraulique apr s l occurrence d une fuite au niveau du consom mateur AltBrake ce composant est dessin en rouge pour indiquer qu il ne regoit plus de puissance hydraulique 3http www arboost com aralia page htm 113 CHAPITRE 7 SYSTEME HYDRAULIQUE D UN AVION DE TYPE A320 engl ng4 NPdistg mg 8 Wes NoruBr e gt rsvg EDPg ja e B 8 LandinaGear RevEr dor lt f s1ecsFleps Eee g Pdistg Y4 Flap Ruadery Rudde PA scapilizery 9 YanDanperz _RevEng2 rael spoiler AltBrake elevator spoilera O res e gt rsvEDPy EDPy B Stabili Y elevat ailen W spoil NPdisty Fic 7 14 Sc nario de perte des lignes Jaune et Verte tape 1 La figure 7 15 montre l effet sur le r servoir de la ligne jaune de la fuite du consommateur AltBrake Apr s l v nement rsvy update le r servoir commence baisser mais comme il n est pas totalement vide les consommateurs de la ligne jaune sont toujours aliment s en puissance hydraulique engl rev DP 4 H SlatsFlaps ny4 _ RevEng2 _FlapsL spoiler elevatorR PYY 4e NPdisty P spoiler4 Fic 7 15
227. st sujet des reconfigurations la g n ration de s quence peut prendre le relais et permet ainsi de visualiser les diff rentes s quences d v nements menant une situation redout e En ajoutant des lois stochastiques aux d faillances probabilit d occurrence d une d faillance pour mod liser la d t rioration d un composant au cours du temps il est possible de faire des simulations stochastiques sur les mod les AltaRica et ainsi de v rifier des propri t s quantitatives sur le mod le L ajout de ces probabilit s sur les d faillances permet aussi lors de la g n ration d arbre de d faillances d obtenir la probabilit d occurrence d une situation redout e Notons qu actuellement les outils industriels n int grent pas des outils de types Model Checking Vers d autres langages Des passerelles vers d autres langages ont galement t r alis es et autorisent l utilisation des outils de v rification et de validation disponibles pour ces langages Une passerelle vers le langage Lustre a t r alis e au LaBRI Gob02 et une passerelle vers le langage d entr e du v rificateur de mod les SMV a t r alis e ON RA Cert KSBC04 En effet apr s transformation du mod le AltaRica en un mod le SMV il est ensuite possible d utiliser les outils associ s ce langage La technique de model checking sur un mod le SMV CCGR00 a t utilis e dans cette th se 27 CHAPITRE 2 TECHNI
228. suivante pour exprimer le crit re 3 z min Uj i l Minimiser le nombre de connexions entre les ressources L utilisation de ce crit re permet d obtenir l architecture optimale du point de vue du nombre de connexions utilis es En effet l action de minimiser les connexions entre les ressources permet d liminer les connexions dites inutiles Ces connexions sont qualifi es d inutiles car elles ne supportent aucun change entre fonctions de Varchitecture fonctionnelle Lors de la conception d un avion les concepteurs cherchent sans cesse de nouvelles technologies afin de limiter le nombre quipements et de c bles utilis s pour faire un gain d espace et de poids au niveau de l avion Un crit re alternatif serait de minimiser le nombre de ressources utilis es mais il semble moins pertinent que celui que nous avons tudi En effet dans un avion le poids et l encombrement d un calculateur sont n gligeables devant le poids et l encombrement des c bles permettant d tablir les connexions entre quipements Par cons quent en minimisant le nombre de connexions utilis es nous esp rons proposer des architectures conduisant un poids de c bles le plus faible possible De plus le nombre de ressources de calcul est souvent contraint et peut donc tre pris en compte par notre recherche d allocation comme une constante Le fait de supprimer automatiquement les connexions non utilis es permet de proposer aux concep te
229. t _ lt alloc f r alloc f r f_enx f f V u_ena r r lt gt alloc f r V alloc f r v 5f enz f f V u_enz r r Comme cette derni re formule est en forme normale conjonctive on peut lui appliquer les r gles de transformation et ainsi obtenir alloc f r V 2alloc f r V 5f enz f f Vu_cnalr vrai 1 alloc f r 4 1 alloc f r 1 f enz f f u enz r r 21 lt 3 alloc f r alloc f r f enz f f u_ena r r gt 1 gt alloc f r alloc f r f enz f enx r r lt 2 Ainsi la contrainte pouvant s int grer dans notre syst me d quations lin aires est Vf F Vrr ER alloc f r alloc f r f enz f f u_ena r r lt 2 Toutes les fonctions doivent tre allou es 4 1 et Une fonction ne peut tre allou e qu une seule ressource 4 2 ces contraintes permettent d obtenir une nouvelle contrainte pour enrichir le syst me WER M alloc f r 1 fief Les traductions des contraintes sur les directives d allocation sont 1 set allocation 4 4 Vf EF 2 alloc T ri 1 r set alloc f 2 co localisation 4 5 coloc fi f2 gt alloc f1 r lt alloc fa r coloc fi f2 alloc f2 r alloc fi r coloc fi f2 alloc f r alloc fa r La traduction de cette contrainte revient donc traduire ces deux sous contraintes et la traduction
230. t ATA29 b hp d4 impacted ATA2S b hp d5 impacted ATA29 9 hp d1 impacted ATA29 9hp edp engl tconnectionhpM impacted ATA29 g hp edp eng2 tconnection hpM impacted ATA29 q suction tconnection edp enal impacted ATA2S g suction tconnection edp eng impacted ATA29 y hp di impacted Button area Open Save Exit Generate List of mapped components Main areas of MapManager GUI The mapping manager graphical user is divided in three main areas on the left side we find the list of components imported from the left side world on the right side is the list of components imported from the right side world and in the middle area is shown the mapping between left and right components The middle area is divided in three parts at the top is the list of mapping names then there is an area containing mapping operations create name remove and at the bottom is the list of mapped components that are currently being viewed At the bottom of the GUI there are several buttons that can be used to load save import or check files to generate failure sets and geometrical cut sets and to exit the application 2 2 Import component list To import a component list you first have to click on the Open button A dialog window will appear select the file including the components and click on the OK button related with the side where you want to import the list of components AE Select a file to load Browse Sele
231. t a mor Gril or 12 oie T3 s 9 edon 11 node Obs_Dual_Loss 12 flow 13 14 WA E ali 3 15 Q 8 lo il amp opis 16 assert mor G l ig edon Ces noeuds AltaRica sont utilis s pour construire les 8 observateurs suivants Perte Totale de l hydraulique prioritaire observateur Phyd et non prioritaire observateur NPhyd Perte de deux lignes hydrauliques lignes Bleues et Jaunes prioritaire observateur GBPhyd et non prioritaire observateur GBNPhyd Bleue et Verte prioritaire observateur YBPhyd et non prioritaire observateur YBNPhyd Jaune et Verte prioritaire observateur GYPhyd et non prioritaire observateur GYNPhyd De plus nous utilisons les sorties des noeuds Pdistb NPdistb Pdisty NPdisty Pdistg NPdistg pour observer les pertes des lignes hydrauliques bleue prioritaire et non prioritaire jaune prioritaire et non prioritaire et verte prioritaire et non prioritaire La figure 7 13 montre une configuration du mod le du syst me hydraulique dans laquelle la situa tion redout e perte des lignes bleues et jaunes non prioritaires est atteinte On voit que l observateur YBNPhyd est dessin en rouge alors que tous les autres observateurs sont dessin s en vert car les situa tions redout es correspondantes ne sont pas atteintes 112 7 3 MODELISATION DE L ARCHITECTURE FONCTIONNELLE DU SYSTEME HYDRAULIQUE M Revenge Pdjsty e
232. t de repr senter l impact des pannes mat rielles sur les d faillances de fonctions support es par les composants en panne De plus la mod lisation des flow repr sentant les connexions entre composants permet de repr senter ais ment la propagation soit d une panne au niveau mat riel soit d une d faillance au niveau fonctionnel Finalement un mod le AltaRica peut supporter l ensemble des informations n cessaires pour faire des analyses de s ret de fonctionnement afin d valuer les exigences qualitatives et aussi pour quantifier les probabilit s associ es diff rentes situations redout es Nous nous sommes ensuite attach s l laboration d une m thode de g n ration d allocation bas e sur la r solution de contraintes permettant de g n rer automatiquement lorsqu une solution existe une allocation garantissant que l ensemble de contraintes de d part est satisfait Les contraintes exprim es portent sur les relations d allocation et permettent par exemple d exprimer que deux fonctionnalit s doivent tre allou es sur deux ressources physiques distinctes contrainte d ind pendance La technique de g n ration d allocation par r solution de contraintes peut proposer lorsque plusieurs allocations v rifiant les contraintes existent non pas une solution mais un ensemble de solutions Il est ensuite du ressort d un architecte du syst me d analyser les diff rentes solutions et de choisir celle qui lui semble tre o
233. t sur des informations d finies par les l ments du mod le Dans le cas d un automate il peut s agir d une propri t du type l ensemble des tats repr sentant des situations non d sir es de l automate n est pas atteignable et dans le cas de mod les en trois dimensions il peut s agir de propri t du type Le composant X et le composant Y sont distants d au moins 20 cm Ensuite il est n cessaire de pr ciser dans quels cas cette propri t doit tre satisfaite Dans l ex pression en langage naturel de l exemple de propri t le mot toujours peut aussi tre interpr t par des valeurs probabilistes probabilit P satisfaite 1 ou encore probabilit P satisfaite gt 1 10 si une tr s faible probabilit inf rieure 107 de non respect de la propri t est jug e acceptable 2 1 3 V rification automatique par exploration du mod le Model Checking Une fois construit le mod le du syst me tudi et formalis es les propri t s il reste v rifier que le mod le satisfait les propri t s Pour cela nous nous sommes int ress s aux techniques fond es sur l exploration automatique du mod le le Model Checking Ces outils parcourent l espace d tats correspondant toutes les volutions du mod le du syst me et valuent les propri t s dans chacun des tats atteints L valuation des propri t s peut tre r alis e sur la base d un espace d tats complet et calcul au pr
234. t dans les moments difficiles elle a toujours su m pauler et s occuper de tout pour que je puisse consacrer le reste de mon temps bien terminer Je profite de ces quelques lignes pour la remercier de tout l amour qu elle a pu me donner A tous ceux que j oublie un grand merci Neke ondoren poza Guillaume et Papou Table des mati res I Introduction au domaine 1 1 Introduction 3 1 1 Contexte g n ral S curit et fiabilit des syst mes a ronautiques 3 1 2 Processus de d veloppement des syst mes a ronautiques critiques 4 LS Limites di processus actuel o e ecce sce do Roo MU dod Rod due 6 14 Objectifs de la th se et 7 i5 Plan de lecture de la th se a oos eoa doo dau vede ok Ree da 8 2 Techniques pour la mod lisation et la v rification 9 2 1 Introduction la mod lisation et la v rification de syst mes 10 ZILI Mod lisation d un syst me o sc o a 2 406 a RR uy RO 3 10 2 1 2 Expression des exigences que le mod le doit v rifier 11 2 1 3 V rification automatique par exploration du mod le Model Checking 12 2 2 Mod lisation et v rification de la s curit des syst mes a ronautiques 13 2 2 1 Exigences de s ret v rifier 13 2 2 2 Langages de mod lisation
235. t pneu ou moteur 5 V rification de la tenue des exigences de s ret de fonctionnement l aide du mod le tendu Dans la suite de ce chapitre nous verrons comment appliquer cette m thodologie sur le cas d tude utilis durant le projet ISAAC 7 2 Pr sentation du syst me Le syst me tudi correspond au syst me hydraulique de 20 Fic 7 1 Syst me Hydraulique de A320 Improvement of Safety Activities on Aeronautical Complex systems 102 7 2 PRESENTATION DU SYSTEME But Le r le du syst me hydraulique est de fournir la puissance hydraulique avec le niveau de s ret ad quat la fois aux l ments permettant le contr le de l avion en vol servo commandes becs et volets gouvernes etc et aux l ments utilis s au sol train d atterrissage syst me de freinage etc 7 2 1 Description Le syst me hydraulique de 1 A320 est compos des l ments suivants e Des pompes qui g n rent la puissance hydraulique n cessaire aux diff rents consommateurs a trois types de pompes celles aliment es par un courant lectrique appel es EMP Electric Motor Pump celles aliment es par les r acteurs appel es EDP Engine Driven Pump et celle aliment e par le dispositif de secours appel e RAT Ram Air Turbine De trois lignes de distribution Green Blue et Yellow qui transmettent la puissance hydraulique des r servoirs vers les consommateurs e De va
236. t propre face une ou plusieurs d faillances Ensuite nous devons identifier les informations qui vont circuler dans notre syst me En effet pour pouvoir tudier la propagation des d faillances dans le syst me il faut identifier les informations importantes qui vont transiter entre les composants et ainsi influencer leurs comportements Dans le syst me hydraulique tudi deux caract ristiques importantes des connexions doivent tre prises en compte Tout d abord la premi re caract ristique est la pr sence ou l absence de puissance dans une connexion Cette caract ristique est importante car nous tudions un syst me dont l objectif est de fournir une puissance un ensemble de composants utilisateurs Par exemple lorsqu une source de puissance subit une d faillance alors elle ne peut plus fournir cette puissance et par cons quent tous les composants connect s cette source doivent tre inform de l absence de puissance par leur connexion respective Cette caract ristique est repr sent e par un bool en associ chaque connexion des composants L absence de puissance est mod lis e par la valeur fausse et inversement la pr sence de puissance correspond la valeur vraie La seconde caract ristique importante des connexions est la pr sence ou l absence de fuite En effet le syst me est sujet des d faillances repr sentant diff rentes fuites qui vont influencer la puissance g n rale fournie par l
237. tement int gr dans le mod le Le comportement individuel des composants et le comportement global du syst me sont statiques c est dire qu ils sont directement d cris dans le mod le et ne n cessitent aucune interpr tation par diff rentes it ration sur le mod le Dans sa th se Thomas Vergnaud Ver06 pr sente une mani re diff rente de traduction de mod le AADL en r seaux de Petri Il faut noter que son objectif n est pas l analyse de s ret de fonctionnement L auteur se base cette fois sur une notion d finie directement par le langage AADL pour exprimer le comportement des composants En effet l utilisation du langage AADL autorise la notion de modes de composant Les modes permettent de mod liser la reconfiguration d un composant en fonction d v ne ments pouvant tre d finis de fa on locale Ces v nements permettent de d clencher un changement de mode pour repr senter des architectures dynamiques de part l volution de leurs configurations Cette notion est aussi tr s proche de la notion de transition en AltaRica mais comme il n existe toujours pas de moyen pour exploiter ces mod les l auteur pr sente une technique de transformation des mod les AADL utilisant la notion de modes en r seaux de Petri pour les analyser Dans MLMEP 05 les auteurs utilisent le langage de mod lisation MOC FTDF Model of Computation Fault Tolerant Data Flow partir desquels il est possible d effectuer des analy
238. the management of Geometrical Functional mappings 1 1 Goal of the tool The goal of this tool is to manage mappings of components from the Geometrical world CATIA IRIS with components of the functional world StateMate SCADE The mapping is used to transform a list of impacted components from the Geometrical world into a group of simultaneously failed components in the functional world Conversely the tool can be used to transform safety assessment results obtained in the functional world as for instance a list of minimal cut sets into a list of impacted components from the geometrical world Functional World Geometrical World Geometrical 4 Components and Failure Mode XML Format Functional Components and Failure Mode XML Format Mapping Manager Mappin mus ED ISAAC XML CATIA XML IRIS TXT CATIA ALA TXT Mapping XML Format Fail sets XML Fomat Safety Assessment Results XML Format Geometrical cut sets XML Format 1 2 Formats Formats for Hit Lists Mapping files and Fail sets were defined as a result of ISAAC WP2 and were modified during ISAAC Paris meeting Nov 2005 Formats for Safety Assessment results and Geometrical cut sets were defined during ISAAC Turin meeting March 2006 In the following we make a distinction between e compulsory tag or attribute in bold font this information is compulsory for t
239. tilis s pour d crire les syst mes ce qui ne facilite pas la compr hension par les concepteurs des sys t mes des sc narios critiques trouv s par les analystes de s curit 1 4 OBJECTIFS DE LA THESE ET DEMARCHE Des projets de recherche r cents BV 03 ont montr qu il tait possible de rem dier aux limites que nous venons de mentionner en utilisant les m thodes formelles pour mod liser et analyser la s curit des syst mes a ronautiques Ces techniques permettent de cr er des biblioth ques de composants r utilisables ceci contribue diminuer l effort et la dur e consacr s la production des mod les g n rer les arbres de d faillances et valuer la tenue des exigences qualitatives automatiquement partir d un mod le du syst me tudi ceci permet d valuer et de comparer rapidement la s curit de plusieurs solutions d architectures pr senter les mod les sous une forme proche des diagrammes utilis s par les sp cialistes des syst mes et simuler sur ces mod les les sc narios les plus critiques ceci am liore le dialogue entre les analystes de s curit et les concepteurs des syst mes Ces nouvelles techniques contribuent essentiellement simplifier les analyses PSSA et SSA En revanche elles assistent assez peu l analyse CCA de recherche des modes communs de d faillance Or des volutions r centes des architectures a ronautiques renforcent l importance de l
240. tion This T connection links the Green Engine Driven Pump with the High Pressure Pipe gt lt failmode component B HP Distribution 1 fm impacted description Blue High Pressure Distribution line first part tribution 2 fm impacted description Blue ne second part i failmode component B HP Dis High Pressure Distribution 11 S i failmode component B HP Distribution 3 fm impacted description Blue High Pressure Distribution line third part failmode component Y EDP fm impacted description Yellow Engine Driven Pump lt failmodes gt lt failmodes name Functional gt lt failmode component EDPy fm fail_loss internal MA320 Hyd EDPy description Yellow Engine Driven Pump gt lt failmode component Pdistb fm fail_leakage internal MA320 Hyd Pdistb description Blue Priority distribution gt lt failmodes gt Hit List The tool deals with a generic format described in the following as well as with Proprietary formats IRIS textual format CATIA XML and textual formats A hit list contains several hitlistitem parts each hitlistitem contains the list of impacted components Futhermore an hit list item may contain information related with the trajectories that caused it The tag trajectorydetails is used to store information such as trajectory angles The attribut
241. trajectoire voulue tant dans le mode Automatique le syst me contr le aussi la vitesse de l appareil Le sys t me re oit plusieurs donn es des quipements de Navigation pour conna tre sa position ainsi que ses diff rentes vitesses vitesse dans le plan vertical VS et horizontal VZ afin de conserver la vitesse la plus lev e Ce composant Navigation constitue un des l ments les plus critiques car il fournit les diff rentes donn es n cessaires pour calculer les ordres de pilotage Ce composant renvoie aussi des donn es permettant d analyser la position de l avion par rapport au plan horizontal CCS Cette position permet le calcul de l angle de tangage appliquer afin de franchir les diff rents obstacles dus au terrain Les autres donn es n cessaires au syst me sont fournies par le Radio Altim tre RA et le SdT Leradio altim tre est une sonde permettant de connaitre tout moment la hauteur de la structure par rapport au sol HRS Cette donn e permet donc de contr ler l altitude r elle de l appareil et est importante lors du calcul du d gagement Le P SdT est un appareil de saisie permettant au pilote de renseigner diff rents param tres propres une mission HS HO Dans ce mode Automatique le syst me SdT calcule en permanence des ordres de pilotage en profondeur DOLONGI l aide de diff rentes fonctions d laboration Elaboration ordre terrain Elaboration ordre altitude El
242. type de mod lisa tion de la relation d allocation permet d analyser et de v rifier des propri t s du mod le d architecture fonctionnelle sans se soucier de l architecture mat rielle utilis e pour supporter le syst me Dans la suite de ce chapitre nous utilisons un exemple tr s simple baptis COM MON pour illustrer les notions pr sent es La figure 3 2 propose une repr sentation du mod le COM MON 32 3 2 MODELISATION DE L ARCHITECTURE FONCTIONNELLE alarme Fic 3 2 Mod le COM MON Ce mod le est compos de 2 fonctions s par es l une appel e COM Commande et l autre MON Monitoring qui effectuent un calcul identique a partir de leurs entr es Une comparaison est effectu e partir des r sultats fournis par ces fonctions Dans le cas o les fonctions ne produisent pas des valeurs identiques un m canisme doit interrompre le transfert des sorties de la fonction COM vers l ext rieur 3 2 Mod lisation de l architecture fonctionnelle La repr sentation de l architecture fonctionnelle est comme nous l avons d finie pr c demment faite partir d un graphe orient repr sentant les diff rentes fonctions du syst me ainsi que leurs interactions interconnexions La mod lisation en AltaRica consiste traduire chaque noeud de F en un composant AltaRica et chaque arc qui repr sente une communication entre deux noeuds en connexion de variables de flux entre deux composants L int r t de l
243. u comportement du r servoir peut s crire de la fa on suivante 1 node rsv 2 flow 3 icone 1 3 private 4 1 out 5 1 6 state 7 S full medium empty 107 CHAPITRE 7 SYSTEME HYDRAULIQUE D UN AVION DE TYPE A320 8 event 9 updates 10 11 trans 12 not S empty fail_Loss gt S empty 13 O rev false and S full update gt S medium 14 false and S medium update gt S empty 15 assert 16 O nom not S empty 17 init 18 S full edon 3 Les pompes elles sont lectriques EMPy et EMPb et m caniques EDPg et EDPy et ont le m me comportement pour nos analyses si une pompe est activ e qu elle est aliment e en nergie l entr e A est vraie qu elle n est pas en panne la variable d tat S est vraie et qu il y a du fluide hydraulique l entr e I nom est vraie alors la pompe produit de la puissance hydraulique la sortie O nom est vraie et sinon elle n en produit pas Une pompe peut subir le mode de d faillance perte v nement fail_loss dans ce cas la pompe ne produit plus de puissance hydraulique De plus la pompe propage dans tous les cas la pr sence d une fuite d un composant en aval entr e O rev est vraie aux composants connect s en amont sortie I rev est vraie S true S false and A 0 nom false fail_Loss
244. u elle appara t et de plus elle doit d clencher la premi re synchronisation pour impacter les fonctions actives allou es cette ressource Ainsi cette nouvelle d faillance introduite par cette nouvelle synchronisation ne doit tre possible que lorsque la garde de la ressource l autorise Voyons pr sent comment exprimer en AltaRica un tel comportement face aux d faillances Consi d rons que chaque composant poss de une d faillance fail error Nous souhaitons ajouter notre Ne Broadcasting d signe une m thode de diffusion de donn es partir d une source unique vers un ensemble de r cepteurs 44 3 4 MODELISATION DE L ALLOCATION mod le une d faillance suppl mentaire qui repr sente la d faillance simultan e des deux t ches lors de la d faillance de la ressource Comme vu pr c demment il faut ajouter dans un premier temps une d faillance synchronisation Fx1_fail_error afin d exprimer le comportement erron simultan ment de Fx1_1 et Fx1_2 et dans un second temps il faut synchroniser cette derni re avec la d faillance de Ress Cette nouvelle d faillance correspond un nouvel v nement nomm Ress_alloc_fail_error Pour permettre la synchronisation de tous ces v nements il faut d finir un l ment interm diaire permettant de rassembler les fonctions en un m me composant a_Fx1 Puis il faut ajouter cet l ment une nouvelle d faillance permet tant de synchroniser la perte simultan
245. une fonction de calcul n ayant que 2 donn es a traiter est le suivant 1 node Function_2in 2 flow 3 Ini FailureType alia LE 4 In2 FailureType E 5 Out FailureType 6 state Status FailureType 8 event 9 evil Ios B 10 init 11 Status correct 12 trans 13 Status correct eT 3905999 29 Status lt erroneous 14 not ost e rani ost gt Steele 15 assert 16 Out case ile Status correct and Ini correct and In2 correct 18 Status correct and Ini correct or In2 correct erroneous 19 Status erroneous erroneous 20 Status lost Rosita 21 else erroneous 22 edon La fonction de calcul est soumise deux types de d faillances l erreur est mod lis e par l v nement fail_error la perte est mod lis e par l v nement fail_lost L assertion d crit son comportement en pr sence des d faillances correct un r sultat incorrect sinon si elle est en erreur elle produit un r sultat erron et sinon si elle est perdue elle ne produit pas de r sultat si elle n a subi aucune d faillance et que toutes ses entr es sont correctes elle fournit un r sultat sinon si elle n a subi aucune d faillance et qu une de ses entr es n est pas correcte elle fournit Le comportement de la fonction de consolidation est donn par le code AltaRica suivant 1 node Function_Consolidati
246. une m thode qui permettant de produire automatiquement des directives d ind pendance qui sont n cessaire pour respecter les exigences de syst me Cette m thode est applicable dans le cas des mod les statiques par analyse des sc narios g n r s par les outils Elle est aussi appliqu e dans le cas des mod les dynamiques en se fondant sur la technique de model checking Cette m thode permet de relier l approche mod lisation du chapitre 3 avec l approche g n ration de contraintes propos e dans le chapitre 4 1 Finalement nous avons voqu une extension possible l approche qui cherche proposer des solutions alors que le syst me de contraintes initial ne permet pas de produire une allocation 80 TROISIEME PARTIE MISE EN APPLICATION DE LA METHODE PROPOSEE L CHAPITRE 6 LE SYST ME DE SUIVI DE TERRAIN SDT D UN AVION DE CHASSE D d velopp e a t valid e sur un syst me qui contribue au pilotage automatique d un avion militaire Il s agit pr cis ment du syst me de suivi de terrain not SdT par la suite li au projet CARLIT labor par l ON RA Apr s une br ve pr sentation de ce syst me et des diff rents l ments le constituant nous pr sentons nos choix de mod lisation ainsi que les diff rentes tapes permettant la v rification des exigences que ce syst me doit garantir Coeur Avionique ReconfigurabLe InT gr SOMMAIRE 6 1 DESCRIPTION DU SYSTEME DE SUIVI
247. ur effectuer des analyses de s curit sur des syst mes industriels Nous justifions ensuite notre choix du langage de mod lisation AltaRica avant de pr senter les analyses que proposent les outils manipulant ce type de mod le 2 2 1 Exigences de s ret v rifier Nous nous int ressons aux exigences de s ret de fonctionnement et plus particuli rement aux exigences de s curit innocuit au sens safety qui visent viter les d faillances catastrophiques c est dire selon Lap96 celles pour lesquelles des cons quences sont inacceptables compte tenu du risque encouru par les personnes ou les biens Les exigences qualitatives de s curit auxquelles nous nous int ressons sont de la forme En pr sence de X pannes le syst me n atteint jamais un certain tat redout Lorsque les sp cifications du syst me le permettent il est possible d ajouter des probabilit s d occurrence aux d faillances permettant ainsi la v rification d exigences de type quantitatif Elles sont g n ralement de la forme La probabilit que le syst me soit dans un tat redout doit tre inf rieure 107 Les tats redout s que nous souhaitons viter correspondent aux Failure Condition d crites dans VPARP 47696 Ces FCs sont class es suivant leur niveau de criticit Ceci permet de d finir les exigences quantitatives et qualitatives v rifier En effet suivant le degr s de criticit d une situation i
248. urs une solution poss dant d j de premi res caract ristiques int ressantes Ainsi le crit re de minimisation du nombre de connexions s crit c_min rr 7 L application de ce crit re l architecture COM MON revient rajouter au syst me l quation suivante min u_cnx_SC_SM u_cnx_RM_SC u_cnx_RM_SM L application de ce crit re sur l exemple du COM MON va permettre de rechercher une allocation poss dant le minimum de ressources de connexion n cessaires pour satisfaire l ensemble des contraintes En ajoutant ce crit re au syst me d quations lin aires cr pr c demment l outil SATZOO propose cette nouvelle allocation 66 4 7 BILAN u_cnx_SC_SM u_cnx_RM_SC u_cnx_RM_SM alloc_COM_SC alloc_MON_SM alloc_S1i_SC alloc_S2_SM alloc_Equals_SM alloc_Interrup_SM used_SM used_SC used_RM L analyse des r sultats se fait par l interpr tation du signe devant chaque variable En effet lorsqu une variable est pr c d e du signe cela signifie qu elle n est pas utilis e par le syst me Par exemple la derni re linge used_SM used_SC used_RM nous indique que parmi toutes les ressources RM n est pas utilis e et donc pas n cessaire Cette allocation est int ressante car elle respecte bien l ensemble des contraintes Par contre la diff rence qu elle poss de par rapport celle tudi e dans le chapitre pr c dent
249. uter un jeton chacune des places de sortie de la m me transition voir exemple figure 2 3 Extensions Plusieurs extensions du langage permettent d utiliser les r seaux de Petri sur des pro bl mes industriels comme les r seaux de Petri color s et hi rarchiques des l ments du r seau de Petri sont eux m mes compos s d un r seau de Petri LM88 Dans un r seau de Petri color on associe une valeur chaque jeton contrairement au r seau de Petri de base ou il n existe qu une sorte de jeton Cette distinction entre les jetons permet d observer la propagation d une panne dans un syst me par le d placement d un jeton particulier dans les places repr sentant les composants impact s du syst me Une autre extension int ressante concerne les r seaux de Petri Stochastiques Dans ces r seaux on associe chacune des transitions une variable al atoire repr sentant une condition pour le tir de cette transition Cette variable correspond au taux de d faillance du franchissement o un nombre al atoire va forcer arbitrairement le choix du chemin suivre La simulation du syst me par ce r seau va permettre de calculer la probabilit d occurrence d un v nement Pour effectuer ce calcul une simulation va comptabiliser le nombre de passage par une certaine place choisie et ce nombre va ensuite tre divis par le nombre total de simulation effectu Nous obtiendrons ainsi la probabilit que l v nement d fini par la plac
250. ux attentes des travaux tr s couteux de rework sur le syst me peuvent tre n cessaires Ensuite ce type d approche par test ne permet pas d obtenir de garantie absolue sur le syst me car 1 il est impossible d obtenir une couverture totale d un syst me d s qu il atteint un niveau de complexit important et 2 sachant qu il est tr s peu probable d observer des v nements pouvant impacter le compor tement du syst me panne mat rielle permutation de bit r sultant d un champ lectroma gn tique etc il est tr s improbable de pouvoir observer leur impact sur le syst me par test Finalement dans le cas de la conception de syst mes ayant des fonctions critiques cette approche de validation par tests s av re insuffisante Il est n cessaire de pouvoir d s la conception d un syst me critique orienter les choix de design et v rifier le plus t t possible que les choix de conception du syst me sont coh rents avec les objectifs vis s Pour ce faire une premi re tape de mod lisation du syst me est n cessaire Le but est de re pr senter par un mod le une vision abstraite de ce que sera notre syst me une fois finalis Il faut comprendre par vision abstraite que seules les informations ayant un impact sur le comportement que l on souhaite v rifier sont prises en compte 2 1 1 Mod lisation d un syst me Pour mod liser un syst me il est pratique de le d composer en un ensemble de
251. vt C Eon tad error lame Busta eq or edon node Bus Fx1 EVE fail_error sync Giger E lM MON all CTI ie Sil Raus error gt edon En effet la synchronisation des d faillances des diff rentes ressources manipulant les donn es v hi cul es par ce bus nous ram ne au cas du double erron pr sent dans la section 3 2 cette situation n tant pas acceptable pour une seule d faillance nous pouvons en d duire que cette architecture propos e ne suffit pas pour tenir cette exigence Apr s cette premi re constatation essayons avec une deuxi me architecture constitu e de deux ressources de communication Fic 3 21 Deuxi me Architecture pour le COM MON Parmi les ressources disponibles dans l architecture mat rielle on remarque que les ressources Sy et Ry sont connect es aux deux Bus Par cons quent afin de suivre les directives l allocation de la voie du composant Interrup se fera sur la ressource Sc et l allocation du composant Equals se fera sur la ressource Sy Les autres allocations se feront sur les ressources restantes savoir sont allou s sur la ressource Ro 5 et MON sont allou s sur Sm Une repr sentation possible de cette allocation est faite par la figure suivante A7 1 et COM CHAPITRE 3 MOD LISATION ET ANALYSE DE L ALLOCATION FIG 3 22 Une allocation
252. y EDP Kappa IN 127 00 Kappa OUT 135 00 Blue B HP Distribution 4 Kappa IN 127 00 Kappa OUT 133 00 Green Priority valve ial De let p Sharp Blue Reservoir 1000 300 0 Fic 7 22 Repr sentation du syst me Hydraulique par IRIS 7 3 4 Les l ments impact s sous forme de HitList Durant le projet ISAAC nous avons travaill en collaboration avec des quipes industrielles Airbus Alenia Dassault Aviation charg es de faire l analyse des risques particuliers clatement pneu et clatement moteur sur des maquettes num riques Chacune de ces quipes utilise des outils diff rents mais produisant le m me type de r sultats Le r sultat de ces analyses correspond une liste des quipements impact s pour un certain clatement 120 7 3 MODELISATION DE L ARCHITECTURE FONCTIONNELLE DU SYSTEME HYDRAULIQUE gt EN y ER L lt SPAT P min C Kmax Fic 7 23 Analyse d un clatement pneu suivant l angle Comme vu sur la figure 7 23 lors d une analyse d un risque particulier comme un clatement pneu les d bris suivent un angle qui varie entre Kmin et Kmax Suivant les outils utilis s lors d une m me analyse il est possible de sp cifier un angle 0 qui coupl avec amp permet de repr senter la zone visualis e comme un c ne Fic 7 24 Analyse d un clatement pneu suivant langle theta Pour une paire d angles 0
253. y descriptions lt failsets name Impact on Functional Model of tyre burst analysis failmodes Functional gt lt failset name a_fail_set_name gt lt failmode component EDPy fm fail loss internal MA320 Hyd EDPg description Yellow Engine Driven Pump failmode component Pdistb fm fail leakage lt trajectorydetails theta 5 kappa in 131 kappa out 145 lt trajectorydetails theta 4 kappa in 138 kappa out 145 trajectorydetails theta 3 kappa in 142 kappa out 145 lt trajectorydetails theta 2 kappa in 144 kappa out 145 140 lt failset gt lt failsets gt Safety Assessment Results A Safety Assessment result file contains several cutsets each cutset is made of a list of failure modes or failure sets The size of the cutset indicates the number of the failure modes or failure sets included in the cutset notice that a failmode that belongs to a failset is not counted lt cutsets failsets Safety Results of the Hydraulic Functional Model extended with tyre burst information failmodes Functional gt lt cutset size 2 name a_cut_set_name gt lt failmode component eng2 fm fail_loss gt lt failset name a_fail_set_name gt lt failmode component EDPy fm fail_loss gt lt failmode component Pdistb fm fail_leakage gt lt failset gt lt cutset gt lt cutsets gt Geometrical Cut Sets A Geometrical cut set file is si
254. yst me Rug05 15 CHAPITRE 2 TECHNIQUES POUR LA MODELISATION ET LA VERIFICATION R seaux de Petri P T Un r seau de Petri Places transitions est un moyen de mod liser le comportement des syst mes dynamiques v nements discrets se base sur une description des relations existantes entre des conditions et des v nements Un r seau de Petri est d fini par un graphe orient comportant cf figure 2 2 un ensemble fini de places P P1 P2 P3 Pm symbolis es par des cercles et repr sentant des conditions e une ressource du syst me ex une machine un stock un convoyeur e l tat d une ressource du syst me ex machine libre stock vide convoyeur en panne un ensemble fini de transitions T T1 T Ts Tn symbolis es par des tirets et repr sentant l ensemble des v nements les actions se d roulant dans le syst me dont l occurrence provoque la modification de l tat du syst me Place C Transition 1 un ensemble fini d arcs orient s qui assurent la liaison d une place vers une transition ou d une transition vers une place 1 Fic 2 2 Exemple de Reseaux de P tri P T Franchissement d une transition Une transition est franchissable lorsque toutes les places qui lui sont en amont ou toutes les places d entr e de la transition contiennent au moins un jeton e Le franchissement consiste retirer un jeton de chacune des places d entr e et rajo

Allocation sûre dans les systèmes aéronautiques : Modélisation

Contents

Download Pdf Manuals

Related Search

Related Contents

Allocation s&ucirc;re dans les syst&egrave;mes a&eacute;ronautiques : Mod&eacute;lisation

Contents

Download Pdf Manuals

Related Search

Related Contents

Allocation sûre dans les systèmes aéronautiques : Modélisation