Home

Outils d`analyse de modèles de systèmes interactifs ADEPT

1. on C powerStatus background 0 0 0 D 255 0 0 ee jeje je jeje ojo jo o e ojo o le ojo jeje FIGURE 6 10 La table topLogicTable du mod le VCR 1 lt Node location 19 80 beanClass javax swing JLabel foreground 0 0 0 visible True verticalAlignment CENTER verticalTextPosition CENTER opaque True enabled True y 80 x 19 text class gov nasa arc sgbe remote nodes BeanNode font Dialog PLAIN 11 size 71 5 height 5 width 71 horizontalAlignment LEADING toolTipText null horizontalTextPosition TRAILING textbf background 0 0 0 componentPostion 0 name powerStatusLabel gt En fait le bon tat initial de son HMI LTS est l tat pr sent la ligne 1266 qui est le m me que l tat erron mis part que la variable est bien initialis e dans celui la L tat pr sent la deuxi me ligne du fichier est donc l tat qui faisait penser une erreur dans la traduction automatique En tenant compte de cette erreur on se rend compte alors que la traduction du mod le VCR par l outil ADEPT2LTS donne de bons r sultats en terme de nombre d tats et de transitions et peut tre consid r e comme une r ussite Les r sultats complets de la transformation du VCR se trouve dans le r pertoire Modeles VCR de Vannexe CD ROM 57 BUN ro 6 5 Exemple du mod le Autopilot simp
2. Logique Cette derni re entit repr sente les l ments logiques comme l tat de l output d une table logique ou alors l appel une table logique sp cifique Les appels aux autres tables logiques se trouvent toujours dans les lignes d outputs des tables logiques et sous forme de valeurs de l l ment sp cial LOGIC Celui ci est similaire l autre l ment sp cial d j mentionn l l ment ACTIONS 2 1 3 Lecture des tables logiques Comme dit dans 8 une table logique consiste en une liste d inputs et d outputs le long de l axe Y et en une s rie de colonnes de paires situation comportement de l automate le long de l axe X Si une table logique devait tre traduite en langage parl la ligne INPUTS serait lue comme un if et la ligne OUTPUTS comme un then En dessous des ces deux lignes les lignes grises pourraient tre lues comme des and et les lignes blanches comme des or Il est important de noter que les outputs ne contiennent que des and ce qui signifie que pour un input bien d fini l output de la table sera toujours le m me et donc que le mod le est d terministe Voici par exemple comment la colonne 0 de la figure 2 2 devrait tre lue et comprise IF state est on AND life est strictly bigger than O AND action produite est user click on the power button THEN state devient off AND powersStatus background devient 255 0 0 0 YO Ab w H H De
3. 0 0 0 qui est la valeur initiale de cette variable comme on peut le voir sur le fragment de code sgb d crivant le composant powerStatusLabel ci dessous 56 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 topLogicTable ACTIONS C fastForwardButton mouseClicked e e e D C playButton mouseClicked ele C rewindButton mouseClicked ele C stopButton mouseClicked C pauseButton mouseClicked o o e C recordButton mouseClicked ele D C tapePosition actionPerformed elo je elo C powerButton mouseClicked ele L topLogicTable outputState Stop Tape jeje je lele D D Play Tape elelelelele D el Fast Forward Tape ejejeje jeje D ele Rewind Tape elelelelele D ele Pause Tape elelelelele D D Record Tape D o V tapeRemaining gt 1 ele o lt 1 amp amp tapeRemaining gt 0 D D D D D D D lt 0 D D D D D D D V verPowerStatus off D D on elololololololo lo lolo lolo ol olo lo lololo D AAA L topLogicTable outputState Stop Tape D D ele e D D Play Tape D Fast Forward Tape Rewind Tape Pause Tape Record Tape V tapeRemaining 00390625 D D D 015625 D D 015625 D D C functionDisplay text Stop e D ele ele Play D F Forward Rewind Pause Record V verPowerStatus off
4. 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 situation behavior 67 1 0 o 0 n 0 011 AA 011 RI n n 68 0 0 N O A PF WV NH NN ON E GG po ob E Ne OO NAAR WN HK 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 39 40 41 42 43 44 45 46 47 48 49 Annexe B Fichier Light java public iseClicked r action Timer actionPe lifeTimer actionPerformed fadingTimer actionPerforme 69 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 73 74 ao F WN ro 0 lt O 1 a WN H 0 lt O Om PF D N ro hor KH O o Annexe C Fichiers texte du modele Light C 1 Lightstate txt C 2 Ligthtransitionaction txt C 3 Lighttransition txt 75 C 4 LightstateObservationAction txt Ch Lightmachine txt lifeTim fading an F WN ro 10 41 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 39 40 41 42 43 new new ga 06 n 07 76 0 0 4 DO Om WN H 0 W W WAON N N N N N N N N ND bb o kh bb bb P PODND P OO AN DA PF W NE O 0 4 o Dm hb D N H Annexe D Fichier de configuration du Light COMMAND COMMAND OBSERVATION ng 77 mod le
5. et ayant une extension mental fichierConfigurationtdfa mental Utilisation tdfa configGen Cette option associ e un nom de fichier permet l utilisateur de g n rer un fichier de configuration li au mod le pass en param tre Le fichier g n r portera le nom associ l option Utilisation configGen file name configMod Cette option associ e true ou false permet de d finir le mode dans lequel l utilisateur souhaite g n rer le fichier de configuration comme cel a t pr sent la section 3 6 Lors d une telle g n ration si cette option n est pas d finie le mode sera mis true par d faut Utilisation configMod truelfalse Voici un petit exemple de l utilisation de ces commandes sur le mod le Light La pre mi re ligne va donc g n rer un fichier de configuration nomm LightConf conf en mode true La seconde quant elle va effectuer les trois types de transformations sur le HMI LTS issu du mod le Light associ avec le fichier de configuration LightConf et montrer tout le processus vu que l option verbose v est pr sente Cette commande va donc g n rer trois fichiers texte repr sentant les mod les mentaux obtenus LightConfbisim mental LightConflearn mental et LightConftdfa mental De plus vu que la commande contient l option debug d cinq fichiers texte suppl mentaires vont tre g n r s repr sentant le mod le syst
6. 78 0 0 N O A bb W NH es aon F WN HO 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 Annexe E La classe ADEPT2LTS public cl HA AAA mr gu uf 79 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 new 81 simulate FAIL FAIL 82 V 0 4 OOF W N H e W o m W WW WWW W N N N N NN N N N N KH E HE R pa pao pao pao E H O 0 0 NAAR WN Ee 6 0 0 NO DG UOUN e O 0 So DG W N H O Annexe F Methode behaviors Creation new while br gt 0 83 84 0 lt O AP WN KR e e O vo Annexe G Mod le airspeedTargetSystemTable G 1 Autopilotstate txt G 2 AutopilottransitionAction txt G 3 Autopilottransition txt ON OTF W N ro o GA Autopilotbisim mental Annexe H Mod le F D H 1 FDstate txt 1 2 3 4 H 2 FDtransitionAction txt 1 2 3 H 3 FDtransition txt 0 lt o AP WN ro HA FDbisim mental 0 0 4 DO 1A W N ro 87 10 11 12 13 14 15 88 ao PF WN r ON DOF WN ro 0 lt O AM WN ro Annexe I Modele VTS 1 1 VTSstate txt 1 2 VTStransitionAction txt 13 VTStransition txt 89 0 0 Na AP o Hr
7. Reset 02 Reset 01 Cancel O3 Cancel 04 Start 02 Start 01 Ring 03 Ring 00 Ring 04 FIGURE 6 9 Repr sentation du mod le mental du CountDown 6 4 Exemple du mod le VCR Le mod le du Video Cassette Recorder dit VCR est un mod le pr sent dans 2 la page 220 Cependant la transformation qui va tre r alis e ici est differente de celle r alis e manuellement dans 2 qui porte sur une version modifi e et r duite du VCR La base du mod le est cependant la m me et poss de une seule table logique qui est la table topLogicTable pr sent e la figure 6 10 Lorsque le mod le est traduit en un HMI LTS on obtient un automate compos de 3134 tats et 25072 transitions Le mod le mental correspondant obtenu comporte quant lui 1 seul tat et 8 transitions lorsque aucune variable n est observable Ces r sultats sont tr s similaires ceux du fichier Archives vcrDemoSingle lts fournit en annexe CD ROM qui contient 3135 tats et 25073 transitions Ce fichier est en fait le r sultat de la traduction manuelle du mod le VCR r alis e par S bastien Comb fis Cependant si l on observe les r sultats qu il a obtenu on s aper oit que l tat initial de son HMI LTS que l on peut apercevoir la ligne 2 du fichier est en fait un tat erron En effet il poss de une variable powerStatusLabel background laquelle aucune valeur n est assign e or elle devrait tre de
8. le de cet outil est de g n rer un fichier Java qui va repr senter le mod le traduit et permettre sa simulation En effet comme d j mentionn auparavant ADEPT se base sur des objets du langage Java ce qui en faisait le langage le plus appropri pour permettre la simulation de l ex cution d un mod le De plus le seul moyen de r cup rer l automate repr sentant un mod le c est d ex cuter ce mod le et d ob server les tats qu il atteint et les transitions qu il effectue Le contenu de ce fichier Java g n r fait l objet d une tude plus pouss e et est d crit la section 3 2 La deuxi me tape est d crite dans la section 3 3 et consiste en la compilation du fichier Java Cette compi lation va g n rer une nouvelle classe dont le contenu pourra tre utilis par ADEPT2LTS gr ce au caract re r flexif du langage Java L appel au contenu de cette nouvelle classe est la troisi me tape du processus qui est d crite dans la section 3 4 ADEPT2LTS va en fait faire appel la m thode simulate de la classe g n r e car c est cette m thode qui simule le mod le et retourne les tats et transitions atteints par le syst me lors de cette simulation 17 Effectuer la traduction de la sorte permet de s parer un processus complexe en plusieurs processus plus simples et plus faciles comprendre De plus cela rend la d tection des erreurs plus facile lorsqu elles arrivent car chaque tape peut tre test
9. par la m thode Le code complet de la m thode simulate se trouve la fin de l annexe B 3 2 2 Structure Chacun des fichiers Java g n r s par la m thode write de l outil Translator poss de exactement la m me structure le m me squelette et ce par un souci de lisibilit et de coh rence entre les diff rents mod les traduits Tout d abord chaque fichier Java g n r commence par deux imports n cessaires l criture de fichiers et l utilisation de listes Ensuite chaque fichier est compos d une classe globale qui repr sente l ensemble du mod le et qui porte donc son nom public class Light Ensuite on d clare toutes les actions pouvant se produire dans le mod le Celles ci sont d clar es l aide d une num ration comme dans l exemple ci dessous montrant la d claration des actions du mod le Light De plus on y ajoute une action sp ciale appel e no action Cette action se produit justement lorsque aucune des actions du mod le n a lieu C est le cas notamment dans la colonne 4 de la topLogic Table du mod le Light La mani re dont cette colonne se traduit en code Java est donn e par apr s private enum Action POWER MOUSECLICKED power mouseClicked FADEOUT_MOUSECLICKED fadeDut mouseClicked LIFETIMER ACTIONPERFORMED lifeTimer actionPerformed FADINGTIMER ACTIONPERFORMED fadingTimer actionPerformed NO ACTION no action private final String actio
10. sgb ou un fichier texte repr sentant un automate lts Tout d abord pour pouvoir utiliser l outil jpf hmi il faut indiquer dans la variable d en vironnement CLASSPATH le chemin vers la classe principale de l outil jpf hmi build main ainsi que le chemin vers la librairie jargs jpf hmi jargs jar Ensuite il suffit de lancer la commande java JpfHmi nom du modele extension pour transformer le mod le pass en param tre Remarquez la n cessit de sp cifier l extension du fichier tant donn que l outil se base sur cette extension pour d terminer s il doit transformer le mod le avec la classe ADEPT2LTS ou la classe LTSLoader Si l utilisateur souhaite transformer un mod le ADEPT il doit veiller tout d abord g n rer un fichier de configuration associ ce mod le gr ce aux options L outil jpf hmi fournit d sormais l utilisateur diverses options relatives A la transformation d un mod le debug Cette option permet l utilisateur de g n rer ou non les fichiers texte pr sent s dans la section 3 5 et decrivant le HMI LTS obtenu apr s transformation du mod le ADEPT Utilisation debug d verbose Cette option permet l utilisateur de visualiser le d roulement de toutes les tapes du processus de traduction Utilisation verbose v config Cette option associ e un fichier permet de sp cifier le fichier de configuration que l outil ADEPT2LTS doit utiliser lors de la traduct
11. FIGURE 2 1 Capture d cran du mod le Light une fois ouvert avec ADEPT 2 1 2 Les entit s dans ADEPT Comme on peut le remarquer dans la figure 2 1 chaque l ment du browser systeme et la plupart de ceux des tables logiques sont pr c d s par une lettre majuscule Ceux qui ne le sont pas repr sentent simplement les valeurs que peut prendre l l ment dans lequel ils se trouvent Ces lettres repr sentent l entit laquelle appartient l l ment qu elles pr c dent Comme cela a d j t mentionn auparavant ces entit s sont au nombre de cinq et les particularit s de chacune d entre elles se trouvent ci dessous C Composant Cette entit repr sente les l ments visuels de l interface utilisateur comme par exemple les boutons ou les labels Ces l ments peuvent tre trouv s sous forme d actions mouseClicked mousePressed dans les lignes d inputs des tables logiques plus pr cis ment comme valeur d un l ment sp cial appel ACTIONS Ces actions appartiennent au premier des deux types d actions existant dans ADEPT les commandes Cela signifie que ce sont des actions sur lesquelles l op rateur un impact que c est lui qui les d clenche en cliquant par exemple sur l un des compo sants visuels Ces composants peuvent galement tre trouv s associ s l un de leurs attributs background text dans les lignes d outputs des tables logiques Cela permet aux table
12. Node name state propertyType String value off class gov nasa arc sgbe remote nodes PropertyNode gt lt Node gt lt Node name life propertyType int value 2 class gov nasa arc sgbe remote nodes PropertyNode gt lt Node gt lt Initial_Values gt lt PropertiesKey gt lt IndexedPropertiesKey gt lt Initial_Values gt lt Initial_Values gt lt IndexedPropertiesKey gt lt LogicsKey gt lt Table_Header Table_Name topLogicTable gt lt Table_Header gt lt Node outputState null name topLogicTable class gov nasa arc sgbe remote sgb nodes LogicRootNode gt lt Node name INPUTS class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node name state referenceNodeName state class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node propertyEditor sun beans editors StringEditor name on isValueNode true class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node gt lt Node propertyEditor sun beans editors StringEditor name fading isValueNode true class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node gt lt Node propertyEditor sun beans editors StringEditor name off isValueNode true class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node gt lt Node gt lt Node name life referenceNodeName life class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node propertyEditor sun beans editors IntEditor name gt 0 isValueNode true class gov na
13. Situation gt lt Table gt Au niveau des variables cela va donner ceci lt Var used true observable true max min gt state lt Var gt lt Var used false observable false max min gt life lt Var gt Finalement l enl vement du composant visuel powerStatus se fait de la m me mani re que l enlevement des variables De plus on peut galement modifier les actions vu que l action lifeTimer n aura plus lieu d tre mais ce n est pas obligatoire car elle n influence plus le comportement du mod le tant donn que les colonnes dans lesquelles elle interve nait ont t supprim es D s lors avec un tel fichier de configuration on obtient la table logique simplifi e repr sent e la figure 3 6 topLogicTable V state on e e fading e off e ACTIONS power mouseclicked ele fadeOut mouseclicked e fading T imer actionPerformed D V state on H fading e off e e FIGURE 3 6 Repr sentation de la table topLogicTable issue du mod le Light apr s simplification au moyen dun fichier de configuration Au niveau du fichier Java qui sera g n r on va pouvoir observer quelques changements notables En effet a chaque endroit du fichier ou la variable life ou le composant po werStatus apparaissaient initialement les m me lignes de code vont tre retrouv es mais sous forme de commentaires qu
14. V selectedSpeed Target V airspeed Target V selectedSpeed Target ele FIGURE 4 4 Une version r duite de la table airspeedTargetSystemTable issue du mod le Autopilot 4 2 1 Fichier de configuration Pour obtenir une telle table il faudra bien videmment manipuler le fichier de confi guration li au mod le Autopilot Donc la premi re tape sera de g n rer ce fichier de configuration et cela en mode false afin que rien ne soit utilis En effet le mod le Auto pilot est tellement vaste qu il est bien plus ais et rapide de renseigner ce que l on a besoin plut t que l inverse Ensuite il faut indiquer dans ce fichier les tables que l on souhaite 43 utiliser ainsi que les colonnes de celles ci Pour recr er la situation voulue il va en fait falloir utiliser six tables du mod le et non une seule Cette contrainte d coule directement de la limitation du principe des fichiers de configuration pr sent e dans 3 6 4 relative l utilisation de la table topLogicTable et du fait que le mod le Autopilot soit sous la forme d une structure ASF airpseed TargetSystem Table La premi re table utiliser est videmment la table que l on souhaite extraire De plus il faut utiliser ses colonnes 0 2 et 6 si l on veut obtenir la m me table que celle pr sent e la figure 4 4 topLogicTable La n cessit d utiliser cette table et
15. autres tables 32 e Variables Un deuxi me point f t de permettre a l utilisateur de choisir les va riables dites classiques qu il souhaitait conserver pour la transformation du mod le En plus de pouvoir enlever compl tement une variable l utilisateur peut galement modifier les variables en leur assignant une valeur maximale et ou une valeur mini male Il peut galement choisir quelles variables seront observables ou non c est dire quelles variables seront utilis es pour distinguer deux tats l un de l autre du point de vue de l op rateur e Composants De mani re un peu similaire aux variables la possibilit de limiter les composants visuels utilis s a t offerte l utilisateur En effet on peut retrouver dans diverses tables certains attributs des composants visuels du mod le Ceux ci font partie des l ments qui d finissent l tat d un mod le et il paraissait d s lors utile de permettre leur limitation De plus il est galement possible de les rendre observables ou non comme pour les variables classiques e Outputs La possibilit de s lectionner quels outputs de tables logiques seront consid r s comme faisant partie des variables du syst me a aussi t donn e luti lisateur De ce fait ceux ci sont trait s de la m me mani re que les composants et les variables Il est donc galement possible de les rendre observables ou non Les outputs ont t s par s des tabl
16. ce qu elle fait Voici par exemple le noeud d crivant la fonction convertAirspeedTargetToMach appartenant au mod le Autopilot Le r le de cette fonction est de transformer une valeur exprim e en m s par une valeur en mach ComponentsKey Ce noeud contient tous les noeuds d crivant les l ments graphiques de l interface visuelle du mod le Ils appartiennent l entit composant CL Ces noeuds contiennent toutes les informations relatives au composant comme son nom son positionnement son type sa police d criture etc Voici par exemple le noeud d crivant le bouton power du mod le Light 11 ObjectsKey Dans ce noeud ci se trouve les noeuds d crivant les divers objets cr s dans 1 le mod le comme les timers Ceux ci appartiennent l entit objet O Voici le noeud d crivant l objet life Timer du mod le Light lt Node name lifeTimer jarEntry gov nasa arc beans TimerBean class class gov nasa arc sgbe remote nodes BeanNode delay 1000 repeats True initialDelay 1000 coalesce True beanClass gov nasa arc beans TimerBean jarURL Users combefis Documents ADEPTworkspace metadata plugins gov arc nasa adept SGBE jar gt PropertiesKey Ce noeud est la racine de tous les noeuds d crivant les variables classi 1 ques du mod le Tous ceux ci appartiennent l entit variable V et contiennentt le nom de la variable qu il repr sente ainsi que son
17. cette ligne est le return de la m thode cela entra nera galement une erreur de compilation 39 40 Chapitre 4 Le cas du pilote automatique A plusieurs reprises auparavant le mod le Autopilot a t mentionn Celui ci est en fait un mod le cr par les chercheurs de la NASA Ames repr sentant le pilote automa tique d un avion de type Boeing 777 Une illustration de ce mod le lorsqu il est ouvert dans ADEPT est pr sent dans la figure 4 1 qui a t tir e de 2 Le pilote automatique d un avion est un outil tr s complexe ce qui rend le mod le Autopilot assez difficile comprendre et surtout tr s vaste En effet les tables logiques d crivant ce mod le sont au nombre de 39 et le fichier sgb le repr sentant contient plus de 2500 noeuds 8600 Adept 1 0 34 777 sgb LCT_v3 sgb Eclipse Users combefis Documents ADEPTworkspace Fir TET Q G 7 l E hd gt Y Determinism Situations Stat or ES E Adept 1 0 34 gt 7 System Browser 23 Of Lor v3 5gb 88 DIR 9 Error Log Add fy LET v3 Add gt gt E Y Root o 1 2 3 4 5 6 7 s8 9 T topLogicTable C TopContainer Y aircraftAutomationObjects Y Lateral TL lateral360Corrections L lateralFeedbackTable L lateralHdgTrkUnitsSys L lateralinterfaceAction L lateralNavigationSyste L lateralSystemTable lateralTargetFeedback lateral TargetSystemTz acBankAngle currentLateralMode hdgTrkUnits latera
18. cisions internes de logique prises par le syst me et les r ponses du syst me l utilisateur Cette structure particuli re est appel e la structure ASF en r f rence aux termes action system feedback Celle ci implique que 41 les tables du mod les soient s par es en trois familles de table les ActionTable les System Table et les FeedbackTable La figure 4 2 illustre bien le r le des diff rents types de table et les interactions qu il existe entre elles dans une telle structure Feedback tables FIGURE 4 2 Repr sentation de l ex cution des tables dans une structure ASF issue de 2 topLogicTable systemTable feedbackTable simulationinterfaceAction Table captalnsFdSystemTable lateralFeedbackTable alrspeedFeedback Table alrspeed TargetSystem Table lateral InterfaceActionTable alrspeedTargetFeedback Table alrspeedInterfaceAction Table cautionWamingLightTable ailrspeedSystem Table ISystem Table FIGURE 4 3 Structure des tables du mod le Autopilot issue de 2 42 Il est galement int ressant de remarquer que la plupart des tables du mod le Autopi lot sont subdivis es en trois grandes parties La premi re partie concerne les tables li es au comportement vertical de l avion c est dire son altitude le fait qu il descende ou qu il monte La seconde partie est compos e des tables d crivant la vitesse de l avion Fi nalement une troisi me grande par
19. dans la table airspeedTargetSystemTable Au contraire dans le fichier Java g n r manuellement les actions sont test es directement dans la table airspeedTargetSystemTable ce qui signifie qu une action sera consid r e comme ayant r ellement eu lieu seulement si elle satisfait l une des conditions de cette table Cette diff rence est la base du fait que la version g n r e automatiquement donne deux transitions suppl mentaires que sont les transitions 10 et 20 De plus on peut s apercevoir que la variable noActionPassed qui est cens e tre mise true lorsque l action qui satisfait la condition est l action no action a simplement t oubli e dans le fichier g n r manuellement Cette deuxi me diff rence explique les neuf transitions li es des tau pr sentes dans le fichier g n r de mani re automatique et pas dans celui g n r manuellement Ensuite toujours pour continuer le parall lisme avec ce qui a d j t fait dans 2 une transformation a t effectu e sur le mod le afin d en obtenir le mod le mental minimal 46 dont la repr sentation se trouve la figure 4 7 Les noms donn s aux tats sont ceux qui ont t obtenus par une transformation selon la technique de bismulation De plus ce processus a t r p t lorsque la variable selectedSpeed Target tait observable ce qui a donn la repr sentation visible la figure 4 8 De nouveau ces r sultats c
20. decrivant les diff rentes actions possibles de la table Ces noeuds contiennent le nom de l action ainsi qu une r f rence vers le noeud repr sentant le composant auquel l action s applique Le noeud LOGIC contient lui des noeuds faisant r f rence d autres tables du mod le Ces deux param tres ont la m me structure comme celle du noeud ACTIONS de la table topLogic Table du mod le Light ci dessous 1 code name ACTIONS class gov nasa arc sgbe remote sgb nodes SgbNode gt 2 lt Node featureName power mouseClicked name power mouseClicked referenceNodeName power class gov nasa arc sgbe remote sgb nodes SgbNode gt 3 lt Node featureName fadeOut mouseClicked name fadeQut mouseClicked referenceNodeName fade0ut class gov nasa arc sgbe remote sgb nodes SgbNode gt 5 lt Node gt TopLogicTable Ce noeud a pour unique fonction d indiquer que le prochain noeud sera le noeud d crit ci apres celui ci portant le nom par d faut de Node Node Ce noeud contient tous les noeuds d crivant le browser syst me qui a t voqu dans la section 2 1 1 Ces noeuds peuvent soit repr senter un dossier contenant divers sous noeuds soit directement un l ment du mod le comme un composant une variable une table etc Ces noeuds contiennent un nom une r f rence vers le noeud repr sentant l l ment ainsi qu un flag bbKey indiquant l entit laquelle l l ment appartient ComponentsKey Prope
21. l auteur a m lang les diff rentes interpr tations de no action Par exemple si l on jette un coup oeil au bout de code ci dessous repr sentant les ligne 937 939 du fichier Java on peut apercevoir une condition repr sentant les inputs de la colonne 8 de la table lateralTargetSystem Table figure 6 11 Comme on peut le voir l auteur du code utilise directement les outputs de la table lateralInterfaceAction Table comme actions ce qui permet d eviter de devoir faire appel cette table mais qui n est pas possible de faire avec les fichiers de configurations voir section 3 6 4 Cependant cela ne change rien au probleme En effet cette condition est la cons quence d une autre interpretation de l action no action L auteur l interpr te ici comme signifiant que n importe quelle action en cours du mod le pourrait satisfaire pour se trouver dans la situation 8 sauf les deux qui sont mises dans la condition Or no action signifie qu il ne doit y avoir aucune action en cours pour satisfaire cette situation Ce qui est trange c est que dans le fichier Java on retrouve tant t l une des interpr tations tant t l autre Scenario 8 else if action Action NO_ACTION else if action Action USER_ROTATES_LATERAL_TARGET_SELECTOR_KNOB_CLOCKWISE 44 action Action USER_ROTATES_LATERAL_TARGET_SELECTOR_KNOB_COUNTERCLOCKWISE lateralTargetSystemTable L laterallnterfaceActionTable o
22. pour transformer un mod le systeme en un mod le mental minimal respectant la propri t de full control e 3DFA le mod le mental est construit selon une une approche bas e sur un Three Valued Deterministic Finite Automaton Ce processus se d roule en trois tapes La premi re est ce que l on appelle une 3NFA compl tion La seconde tape est une d terminisation de l automate tandis que la derni re tape est elle une minimisation de ce dernier e Bisimulation le mod le mental est construit par un m canisme de r duction du mod le syst me Ce processus se d roule en deux tapes La premi re est une tau compl tion du mod le c est dire que les transitions tau sont remplac es La deuxi me tape est la r duction proprement dite e Learning dans cette derni re approche le mod le mental est construit de mani re incrementale tat par tat Finalement la structure de jpf hmi nous permet galement de voir que cet outil four nit trois m canismes diff rents pour importer les HMI LTSs ainsi qu un autre pour les exporter e SC2LTS Premi rement les mod les peuvent tre import s depuis un statechart d fini dans son format standard XMI e LTSLoader jpf hmi contient galement une classe LTSLoader dont le r le est d importer un HMI LTS depuis un fichier texte lts contenant la liste des tats et des transitions du mod le D autre part le LTSLoader permet d expor
23. type et sa valeur initiale Voici par exemple le noeud repr sentant la variable state du mod le Light lt Node name state propertyType String value off class gov nasa arc sgbe remote nodes PropertyNode gt LogicsKey Ce noeud contient tous les noeuds decrivant le comportement du mod le c est dire le contenu des tables logiques Toutes les tables sont d crites par un noeud servant d ent te et un noeud racine contenant tous les noeuds d crivant les diff rents l ments de la table Voici par exemple l ent te et la racine de la table topLogic Table tir e du mod le Light lt Table_Header Table_Name topLogicTable gt lt Node outputState null name topLogicTable class gov nasa arc sgbe remote sgb nodes LogicRootNode gt Ensuite dans le noeud racine on retrouve des noeuds sp ciaux servant distinguer les inputs les outputs les goals ou la cat gorie de comportement Les parties relatives aux goals et aux cat gories de comportements ne seront pas tudi es car celles ci la mani re de l l ment sp cial PRIMITIVES n ont aucune influence sur l automate produit par un mod le ADEPT Voici donc les noeuds racines des inputs et des outputs lt Node name INPUTS class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node gt lt Node name OUTPUTS class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node gt Le noeud racine d une table contient galement divers noeuds
24. un num ro qui d finit quel tat visible observable l tat appartient Les tats visibles repr sentent la mani re dont l op rateur voit observe le syst me Par exemple si aucune variable du syst me n est observable on ne parle pas ici uniquement des variables dites classiques V alors tous les tats seront pr c d s d un 0 indiquant qu ils appartiennent tous 29 1 2 3 au m me tat observable En effet l op rateur ne peut distinguer aucun des tats vu qu il ne conna t aucune de leurs valeurs celles ci n tant pas visibles Au contraire si toutes les variables sont observables tous les tats seront pr c d s dun num ro different vu que l op rateur peut observer toutes les valeurs des diff rents tats Chaque tat est repr sent selon une semantique bien d finie element name element1 state elementN name elementN state Voici par exemple les deux premiers tats contenus dans le fichier Lightstate trt repr sentant les tats du mod le Light 0 state off life 2 powerStatus_ background 255 0 0 1 state on life 2 powerStatus_background 0 255 0 transitionAction Dans ce second fichier nous pouvons trouver une liste des actions oN ro effectivement utilis es durant la simulation du mod le que le fichier repr sente Le fichier contient simplement les noms des actions une action par ligne comme dans le fichier LighttansitionAction txt dont quelques lign
25. 3 fadeOut mC 5 fadingTimer aP 2 power mC 4 lifeTimer aP 7 fadeOut mC 10 fadingTimer aP 9 power mC 6 power mC 8 lifeTimer aP 11 tau FIGURE 3 5 Repr sentation de l automate issu du mod le Light D s lors que la d cision f t prise d utiliser des fichiers de configuration pour limiter la taille et la complexit des mod les sa guise il a fallu r fl chir sur les caract ristiques des mod les ADEPT qui allaient pouvoir tre utilis es ou non pour effectuer une analyse Afin de permettre l utilisateur d analyser un maximum de variantes d un mod le et donc de lui laisser un maximum de libert la totalit des l ments d un mod le peuvent tre mis de c t lors de la traduction de celui ci Le r le de certains l ments peut galement tre modifi e Tables Premi rement il est apparu primordial de pouvoir limiter les tables lo giques de choisir quelles tables logiques on souhaitait utiliser pour une analyse De plus il paraissait important de permettre l utilisateur de choisir les colonnes si tuations qu il souhaitait garder pour chaque table Donc l utilisateur peut d une part enlever certaines tables et d autre part modifier le comportement de celles qu il garde en enlevant les colonnes de son choix Il est important de noter que le fait d uti liser une table signifie que l on va galement utiliser son tat d output l int rieur d elle m me et dans les
26. D ND NN NN EH Goor ER D P A o NA WN H 1 4 VTSbisim mental 90 an WN H an F WN I ON ODO PF W N H e e e a nF WN ro Annexe J Modele CountDown J 1 CountDownstate txt J 2 CountDowntransitionAction txt J 3 CountDowntransition txt J 4 CountDownlearning mental 91 10 11 12 13 14 15 16 17 18 19 20 92
27. PT De plus ces actions sont cha cune li es une colonne de la table logique ce qui explique pourquoi il a fallu indiquer auparavant qu on souhaitait les utiliser Cette liaison entre les actions et l output dont on a besoin sont une illustration du fonctionnement d un mod le structure sous la forme ASF e airspeedTargetIncreaseTimer actionPerformed Cette action est directement li e l output user rotates Airspeed selector knob clockwise En effet la colonne 1 de la table airspeedInterfaceAction Table prend comme unique input cette action et donne ce dernier comme unique output ce qui permet de modifier les inputs de la table airspeedTargetSystemTable De plus m me si normalement cette action est li e un timer et est donc une observation il est n cessaire de l indiquer comme tant une commande car dans 2 on consid re que les actions prises comme input sont justement des commandes 1 lt Act used true type COMMAND gt airspeedTargetIncreaseTimer actionPerformed lt Act gt airspeedTargetDecreaseTimer actionPerformed Cette action est directement li e l output user rotates Airspeed selector knob counterclockwise En effet la colonne 4 de la table airspeedInterfaceAction Table prend comme unique input cette action et donne ce dernier comme unique output ce qui permet comme pour l action pr c dente de modifier les inputs de la table airspeedTargetSystem Table De plus pour les m me
28. TS A a oan ea ua ee 1 2 VTStransitionAction txt 1 3 VTStransitiontxt 2 2 2220 oo cie NAG AA LA CV TSbisimimental u a at sous devos Sg een Nas ann al Modele CountDown J 1 CountDownstate txt J 2 CountDowntransitionActiontxt J 3 CountDowntransition txt 51 51 53 59 56 58 59 61 63 65 69 75 75 75 75 76 76 77 79 83 85 85 85 85 86 87 87 87 87 87 89 89 89 89 90 J 4 CountDownlearning mental Chapitre 1 Introduction A notre poque il existe un grand nombre de syst mes automatis s qui ne cesse de cro tre Ce faisant les gens sont de plus en plus contraints d utiliser ces syst mes infor matiques et d interagir avec eux De ce constat est n e l analyse de l interaction homme machine ou HMI Human Machine Interaction qui avec le temps commence prendre une part importante dans la v rification du bon fonctionnement de ces syst mes automa tis s Celle ci est d autant plus importante dans la v rification des syst mes complexes o impliquant la mise en danger d amp tres humains comme les pilotes automatiques d avions ou les appareils m dicaux Avec l volution de ce type d analyses plusieurs approches et divers outils permettant de r aliser de telles analyses ont vu le jour C est par exemple le cas de l outil ADEPT qui permet de mod liser et de simuler l ex cuti
29. U C L Universit Catholique de Louvain Universit cat h O I q ue Ecole Polytechnique de Louvain de Louvain Outils d analyse de mod les de syst mes interactifs ADEPT M moire pr sent en vue de l obtention du grade de Promoteur Prof Charles Pecheur master 120 cr dits en sciences informatiques Co promoteur S bastien Comb fis option Lecteur Prof Peter Van Roy r seau et s curit par Pierre Nauw Louvain la Neuve Ann e 2013 2014 Table des matieres 1 Introduction 2 Contexte 2 1 ADEPT N Ss 604 oe e Le dans 2 1 1 Description de l outil 2 1 2 Les entit s dans ADEPT 2 1 3 Lecture des tables logiques 2 1 4 Les fichiers SGBs 2 2 JPE HMI ip ga oa pra 2 2 1 Description de l outil 3 ADEPT2LTS 3 1 3 2 3 3 3 4 3 9 3 6 Translator 3 1 1 Premi re tape le SGBParser 3 1 2 Deuxi me tape Le tri 3 1 3 Trosi me tape le Java Writer Fichier Java 2 2222 2200 3 2 1 Methode simulate 3 2 2 Structure 3 2 3 R gles de traduction d une table logique Compilation du fichier Java Appel la m thode simulate Fichiers texte Fichiers de configuration 3 6 1 Structure 3 6 2 Exemple du mod le Light simplifi 3 6 3 Generation des fichiers 3 6 4 Limitations 4 Le cas du pilote automatique 4 1 4 2 Structure Tr
30. aduction d une table 4 2 1 Fichier de configuration 4 2 2 R sultats 5 Manuel d utilisation 17 18 19 21 22 22 22 23 26 29 29 29 31 34 35 37 38 41 41 42 42 45 49 6 7 Evaluation 61 Exempledumod leF D ESS 6 2 Exemple du mod le VTS 6 3 Exemple du mod le CountDown 6 4 Exemple du mod le VCR 6 5 Exemple du mod le Autopilot simplifi 6 6 Performances de l outil Conclusion Bibliographie A B QO 7 H J Fichier Light sgb Fichier Light java Fichiers texte du mod le Light Cil Tashtstater RL a anar sn Kar gen Fie ge behets aa ees C 2 Ligthtransitionaction txt C 3 Lighttransition txt C 4 LightstateObservationAction txt CO Lightmachine tb avi paio ND ed aken ge R Fichier de configuration du mod le Light La classe ADEPT2LTS M thode behaviors Creation Mod le airspeedTargetSystem Table G 1 Autopilotstate txt G 2 AutopilottransitionAction txt G 3 Autopilottransition txt G 4 Autopilotbisim mental Mod le F D Hal PDstatetkt enaar etten cae Dal Pele A ee Bn des H 2 FDtransitionAction txt H 3 FDtransition txt HA FDbisim mental Modele V
31. ariable expr gt variable expr Number variable number gt variable number v V cond V Number variable V variable gt variable variable v v Number variable expr gt variable expr La troisi me et derni re possibilit est que la condition porte sur une variables classique La traduction va alors d pendre du type de la variable et ensuite du contenu de la valeur que l on veut tester D une part si le type de la variable est String on va utiliser la m thode equals avec avec la valeur comme parametre pour d terminer si la condition est vraie ou fausse Ensuite si la variable est de type boolean on va utiliser le symbole pour comparer la valeur Finalement si le type de la variable est un nombre c est dire int double ou float on va galement utiliser le symbole pour tester une valeur qui est un nombre ou une autre variable Par contre si la valeur est une expression plus complexe contenant des symboles comme lt gt amp amp etc alors la condition sera simplement une concat nation de la valeur a l l ment OUTPUTS Dans la traduction Java d une table logique si les inputs d une colonne forme un if statement les outputs de cette m me colonne forment alors le corps de cet if statement c est a dire les op rations a effectuer si celui ci est valide Dans ce cas ci les bullets for
32. ate Finalement ce sont les attributs des composants C du mod le qui sont d clar s et initialis s Voici par exemple l attribut background du composant powerStatus tir du mod le Light 1 rivate 255 00 D sormais afin de pouvoir comparer les diff rents tats du mod les les uns par rapport aux autres il faut qu ils poss dent une methode equals qui va tester l galit de leurs attributs un un Voici par exemple cette m thode issue du mod le Light 0 lt o A PF W N E 24 10 11 12 0 lt O o PF WN E ON O A PF D N ro 0 0 JO Om WN H e e pb O 12 13 14 15 Ensuite il faut ajouter une m thode permettant d imprimer les tats Voici la methode toString nouveau extraite du mod le Light public Juste apr s cette derni re on retrouve une m thode fort semblable appel e stateOb servation Cette m thode permet de d finir quelles variables sont observables par un op rateur qui interagi avec le mod le Finalement on ajoute une derni re m thode cette sous classe State permettant de la cloner la m thode clone Voici celle issue du mod le Light public Ensuite et ce afin de pourvoir simuler le comportement du mod le chaque table va tre r crite en code Java sous forme d une m thode Chaque table sera une m thode et prendra comme param tre une action Action et un tat State Le contenu des tables logiques est t
33. auf dans le cas du mod le Autopilot pour lequel une seule a t r alis e Etats Noeuds Trad ms Sim ms Trans ms F D 4 2566 861 39 16 VTS 8 89 105 37 34 CountDown 6 96 108 42 31 VCR 3134 162 178 44 s 2s Autopilot 15 016 2566 964 50 m 15 s FIGURE 6 12 Performances de l outil JPF HMI Lorsque l on analyse ces r sultats on peut tout d abord se rendre compte que le temps n cessaire la transformation d un fichier sgb en un fichier Java semble d pendre princi palement la taille de ce fichier sgb et ce de mani re lin aire En effet plus le nombre de noeuds grandit plus le temps n cessaire la traduction semble lev mais sans que cela explose De plus m me si le mod le F D et le mod le Autopilot ont des tats diff rents cause de leur fichier de configuration ils se basent sur le m me fichier sgb ce qui explique leur similarit en terme de temps de traduction Cependant on peut voir que le fichier de configuration influence galement l g rement ce temps vu que le temps pour le mod le Autopilot est tout de m me plus lev Ensuite en terme de simulation on peut voir que le temps explose litt ralement quand le nombre d tats augmente qu il semble voluer de mani re exponentielle par rapport aux tats ce qui est plut t logique au vue de son r le Par contre pour la transforma tion les temps semblent plut t voluer de mani re
34. celui ci a t traduit par l outil ADEPT2LTS afin d en extraire un HMI LTS repr sentant son comportement L automate ainsi obtenu se compose de 8 tats et 20 transitions et est repr sent dans la figure 6 5 Dans cette re pr sentation push fait r f rence l action pushUp mouseClicked pull l action pull Down mouseClicked up upTimer actionPerformed et down a down T imer actionPerformed Des lors il etait possible d obtenir le mod le mental li au VTS ce qui a donn un auto mate 5 tats et 14 transitions repr sent la figure 6 6 Une fois de plus les r sultats obtenus gr ce l outil ADEPT2LTS sont les m mes que les r sultats obtenus manuelle ment qui sont pr sent s dans 2 la page 188 et dans 4 Les r sultats complets de cette valuation se trouvent l annexe I 53 16 pul 14 pull 12 down 11 push FIGURE 6 5 Repr sentation du mod le syst me du Vehicle Transmission System FIGURE 6 6 Repr sentation du mod le mental du Vehicle Transmission System 54 6 3 Exemple du mod le CountDown Le mod le CountDown a t tir de la page 75 de 2 Ce mod le repr sente un simple compte rebours pouvant monter jusqu deux avant d tre lanc Avant de pouvoir valuer ADEPT2LTS sur ce mod le il a d abord fallu le mod liser sous forme d un mod le ADEPT afin d en obtenir un fichier sgb Le r sultat de cette mod lisati
35. d crivant les dif f rents comportements du mod le Chacun de ces noeuds repr sente en fait une situation distincte autrement dit une colonne de la table logique Le premier noeud du fichier sgb repr sente la colonne 0 le deuxi me la 1 et ainsi de suite Ces noeuds contiennent un nom une petite description du comportement et une sp cification d crivant le contenu de la colonne qu ils repr sentent Ce que ces sp cifications re pr sentent concr tement fera l objet d une tude plus pouss e dans la section 3 1 1 Voici les noeuds des colonnes 0 et 1 de la table topLogic Table du mod le Light lt Node name situation specification 1 O 07 1 0 1 0 O O o O 1 0 1 0 0 1 O 0 behavior behavior class gov nasa arc sgbe remote sgb nodes Situation gt lt Node name situation specification 0 0 1 1 0 1 0 0 OJ 1 O 0 0 0 1 1 O O 0111 behavior behavior class gov nasa arc sgbe remote sgb nodes Situation gt 12 Apres cela si l on observe ce que contient le noeud racine des inputs on peut trouver les noeuds relatifs aux param tres de la table aux diff rents inputs Tous ces noeuds ont un nom et ont une r f rence vers un autre noeud d clar auparavant dans le fichier Si le param tre est une variable classique il fera r f rence au noeud repr sentant cette m me variables dans les PropertiesKey si le param tre est l output d une table alors il fera r f rence au noeud racine de la table ass
36. d ja voqu s a la section 2 1 4 les fichiers de configuration poss dent un noeud racine qui contient tous les autres noeuds d finissant la configuration lt AdeptConfig gt lt AdeptConfig gt Le premier sous noeud est le noeud lt Tables gt qui contient les noeuds d finissant quelles tables sont utilis es Ce noeud contient donc une liste de noeuds lt Table gt contenant chacun un nom un flag used servant d terminer s il faut l utiliser ou non et une liste de noeuds lt Situation gt Ces derniers noeuds repr sentent les colonnes de la table et poss dent galement un flag used ce qui sera le cas de chaque l ment du mod le repr sent par une balise dans le fichier de configuration Voici par exemple la repr sentation de la table topLogic Table du mod le Light et de ses deux premi res colonnes lt Tables gt lt Table name topLogicTable used true gt lt Situation used true gt 0 lt Situation gt lt Situation used true gt 1 lt Situation gt lt Table gt lt Tables gt Ensuite on retrouve le noeud lt Variables gt qui contient les noeuds relatifs aux variables dites classiques V Chacun de ces sous noeuds contient le nom de la variable laquelle il fait r f rence ainsi qu un flag observable indiquant si la variable est observable c est a dire si elle est visible de l op rateur De plus les noeuds contiennent des attributs max et min permettant de limiter
37. e r apFdAtInterfaceActionTable outputState no action D user toggles first officer fd switch ele L firstOfficersFdSystem Table outputState first officers FD on e first officers FD off e L firstOfficersFdSystem Table outputState first officers FD off e first officers FD on e FIGURE 6 2 La table firstOfficersFdSystem Table issue du mod le Autopilot La traduction de ce mod le gr ce l outil ADEPT2LTS donne un HMI LTS compos de 4 etats et 12 transitions dont la representation se trouve la figure 6 3a Dans cette repr sentation cptSwitch mC repr sente l action mcpCaptainsFdSwitch mouseClicked foS witch mC repr sente l action mcpFoFdSwitch mouseClicked cptOut repr sente l out put de la table captainsFdSystemTable et finalement foOut repr sente l output de la table firstOfficersFdSystem Table Notez que seules les transitions ayant des tats de d part et d arriv e diff rents ont t repr sent es Ensuite la transformation du mod le par bisimulation m ne au mod le mental repr sent dans la figure 6 3b Les r sultats d une traduction manuelle de ce mod le ont d j t pr sent s dans 2 la page 226 ce qui permet de juger de la validit des mod les syst me et mental obtenus avec la nou velle version de jpf hmi Les r sultats complets de ces transformations sont repr
38. e sinon la simulation ne pourra jamais atteindre cette derni re Une seconde limitation du principe des fichiers de configuration d coule du fait qu il n est pas possible de s lectionner soi m me quel input d une table fera office d action de transition dans l automate g n r En effet seules les actions d finies comme telle dans le mod le ADEPT peuvent tre utilis es comme transitions dans l automate le repr sentant Pour rappel ces actions sont soit des actions li es un composant visuel c est dire des commandes soit des actions associ es des timers c est dire des observations Une autre chose importante prendre en compte lorsque l on modifie un fichier de configuration c est que les flags used et observable sont en quelques sortes li s En effet si par exemple une variable est mise comme observable celle ci ne sera prise en compte que si le flag used est mis true galement Sans cela le fait de la rendre observable ne changera rien elle sera toujours consid r e comme non observable M me si rendre une variable non utilis e observable n aurait aucun sens une erreur est vite arriv e et cette mani re de faire permet d viter les erreurs de compilation pouvant appara tre dans le fichier Java Un ph nom ne pouvant se produire et pouvant poser quelques probl mes impr vus est le ph nom ne dit de la cascade Cela signifie que lorsque l on d cide de ne pas uti
39. e ce soit dans la m thode equals par exemple ou lors de leurs d clarations Il aurait bien sur t possible de choisir d enlever compl tement ces lignes de codes plut t que de les mettre en commentaire cela aurait pu raccourcir les fichiers Java qui peuvent parfois tre tr s longs Cependant la mise en commentaire de ces lignes permet de visualiser plus facilement les effets du fichier de configuration sur le mod le initial et facilite donc la mise en place du fichier de configuration souhait Dans les tables logiques le travail est un peu diff rent cause des conditions En effet dans celles ci l utilisation d une variable qui n est pas utilis e dans le fichier de configuration m ne au bool en true car celui ci ne modifie pas le r sultat de l expression test e dans la condition Voici par exemple la traduction en Java de la colonne 0 du mod le r duit 36 Noor D H ro Situation 0 if to state equals on amp amp true amp amp action Action POWER MOUSECLICKED to state off to powerStatus_background 255 0 0 actionPassed true Le r sultat de cette simplification du mod le Light donne lieu un automate poss dant trois tats et quatre transitions Une repr sentation de ce r sultat se trouve la figure 3 7 3 fadeOut mC 4 fadingTimer aP 2 power mC FIGURE 3 7 Repr sentation de l automate issu du mod le Light simplifie 3 6 3 Generation de
40. e inputs d une colonne repr senterait une condition c est dire une paire l ment valeur D s lors en se basant sur la figure 3 4 qui repr sente la structure g n rale d une table logique dans ADEPT chaque input de colonne prendrait une forme semblable celle ci if elementi valuel x amp amp element2 value2 x element2 value2 y amp amp amp amp elementn valuen x 26 Chaque bullet noire chaque condition est en fait un test sur une valeur dun l ment Chaque condition aura justement une forme qui sera d termin e par cet l ment et cette valeur qu elle repr sente Voici quelques r gles de traduction une bullet tant repr sent e par cond element value e cond ACTIONS C component event gt action Action COMPONENT EVENT cond ACTIONS O timer event gt action Action TIMER EVENT Si la condition porte sur la valeur d une action on teste simplement par rapport l quivalent de cette valeur dans l num ration Action pr sente dans le code Java g n r partir du mod le e cond L table outputState state value gt tableOutput table STATE VALUE Si la condition porte sur la valeur d un output d une table logique on teste simple ment par rapport l quivalent de cette valeur dans l num ration des tats d out puts possibles de la table String variable expr gt variable equals expr Boolean v
41. e repr sentation lorsqu elle est compar e celle donn e dans 2 nous donne la confirmation que le fichier de configuration cr est correct et fonctionnel 25 16 N 1 17 19 7 13 8 FIGURE 4 6 Repr sentation du mod le systeme li la table airspeed TargetSystem Table 4 4 La diff rence obtenue dans les r sultats au niveau des transitions du HMI LTS g n r s explique facilement lorsque l on est attentif au contenu du fichier Java qui avait t crit manuellement pour g n rer les r sultats obtenus dans 2 Ce fichier Java est disponible dans le r pertoire Archives first syst abstr lobs de l annexe CD ROM La raison de cette diff rence provient en fait de l utilisation de deux variables appel es actionPassed et noActionPassed Ces variables sont utilis es lors de la simulation d un mod le pour savoir si l action en cours s est r ellement d roul e c est dire si elle a satisfait l une des conditions d une des tables travers es Or dans le cas d un mod le structur sous la forme ASF une action satisfait toujours au moins une condition celle li e cette m me action dans les tables relatives aux actions Une action sera donc consid r e comme s tant vraiment produite m me si celle ci n aura fait que modifier l tat d output de la table airspeedInterfaceAction Table et qu elle n aura satisfait aucune condition
42. e s par ment L uti lisation dun fichier Java annexe lors de la traduction tait n cessaire pour permette de virtualiser le mod le et de l ex cuter afin de conna tre l automate d coulant de celui ci Des lors le seul moyen d acc der au contenu de ce fichier tait la r flexivit Une autre solution aurait pu tre d incorporer directement les algorithmes d analyses fournis par jpf hmi l int rieur du fichier Java g n r de sorte que les analyses voulues s effectuent pendant l ex cution du fichier Java Cependant cette solution ne permettait pas de conserver un certain parall lisme avec ce qui avait d j t fait qui consistait notamment distinguer clairement une phase d importation d un mod le et ensuite seulement une phase d analyse comme on peut le voir clairement dans la figure 2 8 FIGURE 3 1 Vue d ensemble de l outil ADEPT2LTS 3 1 Translator L outil Translator est une classe Java qui prend en entr e un fichier sgb d crivant un mod le ADEPT et qui g n re un fichier Java dont le but est de le simuler En effet pour conna tre les tats et transitions franchies par un mod le ADEPT il est n cessaire de simuler une ex cution de celui ci et d observer son comportement Comme cela est visible dans la vue d ensemble du fonctionnement de l outil donn la figure 3 2 l op ration de traduction se d roule en trois tapes distinctes Une fois de plus le travail de l outil a t divi
43. endre la mani re dont on g n re un HMI LTS lors de la simulation d un mod le car les techniques sont les m mes D abord on d clare les actions du mod les Action a0 new Action power mouseClicked ActionType COMMAND 30 Ensuite on trouve les d clarations des actions li es aux observations sur les tats 1 Action 00 new Action 00 ActionType STATE_OBSERVATION Pour en finir avec les actions on d clare l action sp ciale tau qui est utilis e 9 9 pour d signer qu il n y a aucune action utilis e no action 1 Action tau new Action tau ActionType TAU Apr s avoir d clar toutes les actions on initialise le HMI LTS LTS lt Extended State Transition gt et on y ajoute chacun des tats de l automate repr sentant le mod le Afin de former des tats enrichis on ajoute simplement une action sur l ob servation d un tat l tat non enrichi 1 LTS lt ExtendedState Transition gt system new LTS lt ExtendedState Transition gt 2 ExtendedState s0 new ExtendedState S0 00 3 system addState s0 Finalement on ajoute au HMI LTS chacune des transitions issues de l automate 1 system addTransition new Transition a0 s0 s1 2 system addTransition new Transition a0 sl s0 stateObservation Action Ce fichier contient simplement un nombre indiquant le nombre d actions li es aux observations sur les tats augment de un Si l on se base sur le fichier contenant
44. es pour permettre d utiliser une table et son out put normalement sans que celui ci soit consid r comme une variable du syst me et donc utilis pour tester l galit de deux tats Il faut tre attentif que dans ce cas ci c est tout ce que les outputs s lectionn s font ils ne sont pas responsables de l utilisation directe de ces outputs dans les inputs o outputs des tables qui eux d pendent directement des tables d clar es e Actions Le syst me de fichiers de configuration offre galement la possibilit de s lectionner les actions que l on souhaite utiliser ou non pour la transformation du mod le La limitation du nombre d actions dun mod le permet de r duire les possibilit s dans le comportement du mod le et donc les transitions de l automate obtenu apr s simulation de celui ci Cela peut donc galement limiter le nombre d etats atteints par cette simulation et donc forc ment le poids de celle ci en terme de m moire De plus il est galement possible de choisir comment l action doit tre interpr t e c est dire si elle doit tre vue par le syst me comme une commande ou comme une observation un v nement se produisant dans l environnement du mod le Il est important de noter que les actions initialement li es un composant visuel les commandes ne le sont plus ici Cela signifie que le fait de ne pas utiliser un composant n affecte en rien les actions du mod le e Fonctions Pou
45. es sont donn es en exemple ci dessous Vous noterez qu est pr sente galement l action no action qui comme cela a d j t voqu signifie qu aucune action n a lieu power mouseClicked fadeOut mouseClicked no action transition Ce fichier contient la liste de toutes les transitions qui sont franchies durant om WN E la simulation du mod le que le fichier repr sente Le fichier contient une transition par ligne Chaque transition contenue dans le fichier est repr sent e par un num ro d action un tat de d part et finalement un tat d arriv e selon la s mantique sui vante action number starting state number finishing state number Le nombre assign un tat renseigne la position de celui ci dans le fichier state Le m me syst me est en vigueur pour les num ros correspondants aux actions et au fichier transitionAction Voici par exemple quelques une des transitions contenues dans le fichier Lighttransition txt issu du mod le Light Il est important de noter que le tau est en fait l identifiant de l action no action 0 0 1 0 1 0 1152 tau 6 7 machine Ce fichier contient du code Java Ce code Java s il est ex cut permet de 1 generer le HMI LTS lie au mod le repr sent Chaque fichier machine a la m me structure dont voici quelques extraits provenant du fichier Lightmachine tat issu du mod le Light L observation de ces fichiers permet de mieux compr
46. et gt Chacun des fichiers de ce type poss de une structure commune comme celle pr sent e ci dessous lt AdeptProject gt lt DstPanelElement gt lt JarFileURLKey gt lt JarFileURLKey gt lt MethodsKey gt lt MethodsKey gt lt ComponentsKey gt lt ComponentsKey gt lt ObjectsKey gt lt ObjectsKey gt lt PropertiesKey gt lt PropertiesKey gt lt IndexedPropertiesKey gt lt IndexedPropertiesKey gt 10 10 11 12 13 14 15 AdeptProject Ce noeud repr sente la racine du fichier sgb Ils contient tous les autres noeuds qui eux d criront le mod le ADEPT DstPanelElement Ce noeud ci repr sente la description du conteneur principal de l in terface utilisateur c est dire le panel de fond de cette interface Il contient diverses informations relatives ce panel comme sa hauteur sa largeur sa couleur de fond etc JarFileURLKey Ce noeud contient d autres noeuds servant indiquer o trouver les librairies import es et utilis es par le mod le ADEPT MethodsKey Ce noeud ci est le noeud racine de tous les noeuds d crivant les fonctions d finies dans le mod le Ces noeuds font r f rence des l ments appartenant l entit fonction F pr sent e dans la section 2 1 1 Chacun de ceux ci contient le nom de la fonction qu il repr sente le type de la valeur qu elle renvoie le code java du corps de celle ci et parfois une petite description de
47. euds sera transform en une instance de la classe Table Ensuite chaque instance de cette classe Table contient quatre listes d instances de la classe LogicNode behaviorCategory outputs goals inputs dont le but est de s parer les l ments d une table en fonction de leur r le dans celle ci Cette classe LogicNode repr sente en fait un element de la table logique que ce soit une variable V un composant C un output d une table L ou m me un des l ments sp ciaux comme ACTIONS et LOGIC Il existe galement une cinqui me liste compos e d instances de la classe Behavior Node qui repr sentent les noeuds d crivant le contenu des colonnes de la table logique des diff rentes situations possibles Cependant cette premi re traduction n est pas suffisante car lors de cette tape les in formations ne sont pas tri es ni modifi es mais simplement recopi es sous une autre forme et n cessitent donc d tre tri es avant d tre pass es l outil JavaWriter Cependant cette forme est plus compr hensible indique clairement o se trouve telle ou telle information et rend finalement les informations plus facilement accessibles Ci dessous se trouve une illustration de la simplification et de la clarification des moyens d acc s aux informations contenues dans un fichier sgb Cet exemple met en place une comparaison entre les lignes de codes utilis es pour r cup rer la valeur init
48. fichier sgb Les mod les issus du fichier sgb le plus vaste Autopilot sgb ont m me un rapport temps nombre de noeuds inf rieur aux autres mod les De plus au fur et mesure que le nombre d etats dun mod le augmente le temps n cessaire a la traduction devient minime voir n gligeable par rapport aux temps obtenus pour les deux autres phases Finalement objectif de d part de l outil ADEPT2LTS qui tait de traduire un mod le ADEPT au format sgb en un automate semble atteint la validit de celui ci ayant t prouv e dans la plus grande partie des mod les test s 62 Bibliographie The automation design and evaluation prototyping toolset adept users guide version 1 0 19 S bastien Comb fis A Formal Framework for the Analysis of Human Machine Inter actions PhD thesis Universit catholique de Louvain November 2013 S bastien Comb fis Dimitra Giannakopoulou Charles Pecheur and Michael Feary Learning system abstractions for human operators In Proceedings of the International Workshop on Machine Learning Technologies in Software Engineering MALETS 11 pages 3 10 New York NY USA 2011 ACM Sebastien Combefis and Charles Pecheur A bisimulation based approach to the ana lysis of human computer interaction In Proceedings of the 1st ACM SIGCHI sympo sium on Engineering interactive computing systems EICS 09 pages 101 110 New York NY USA 2009 ACM Sebastien Combefis Dimitra Gianna
49. hier de type XML ayant une extension sgb repr sentant l ensemble du mod le et de ses l ments Ces fichiers font l objet d une tude plus pouss e dans la section 2 1 4 ae Applications Raccourcis Syst me Zei d amp 9 C mar 18 mars 17 22 root Adept 1 0 35 myproject light sgb Eclipse 0 X File Edit Navigate Search Project Adept Run Window Help WE TEST i be Determinism gt vn om ee ns SE E lt gt Plug in Development F3 Adept 1 0 35 7 System Brow 8 gt O 7 light sgb X x User Interface Editor 23 kahi gt 5 Add 0 1 2 3 4 5 Add gt gt TL OOO H topLogicTable o 5 v amp Root VIstate 7 E topLogicTable on e e power Pa t8 fading ee C topContainer off fadeOut Y C fadeout V life seou C power gt 0 eee C powerstatus 0 O fadingTimer CRETIONS liferi C power mouseClicked ee EE Olfadeout mouseclicked D V life O lifeTimer actionPerformed k V state fadingTimer actionPerformed E OUTPUT TU IM state on fading off ee 7 Prop amp Nod 8 vite 1 e C powerStatus background 255 0 0 ee 0 255 0 PRIMITIVES O lifeTimer start O lifeTimer stop O fadingTimer start O fadingTimer stop e topLogicTable 23 4 T In eclipse Bo te de r ception p workspace EJ myproject S Adept 1 0 35 mypro Ki
50. iale de la variable state issue du mod le Light Parseur DOM traditionnel Element Document getDocumentElement getChildNodes item 5 getChildNodes item 0 getAttribute value SGBParser SGBParser getPropertiesKey get 0 getValue 20 3 1 2 Deuxieme tape Le tri Cette seconde tape aura pour but de trier les informations r cup r es via l outil SGB Parser de recoller les morceaux en quelque sorte Par exemple afin de virtualiser les tables logiques de la meilleure mani re qu il soit pour les pr parer l criture dans le fichier Java il va falloir r cup rer des informations plac es divers endroits dans la structure de don n es g n r e par la classe SGBParser Pour stocker toutes les informations dont l outil JavaWriter aura besoin pour g n rer le fichier Java la classe Translator va utiliser toutes une s rie de listes et de classes repr sentant certains l ments En fait Translator va uti liser exactement quatre classes annexes e LogicTable Cette classe a pour but de virtualiser une table logique Celle ci est pr sent e un peu plus en d tails ci apr s e Logic Variable Cette classe repr sente une variable logique du mod le V dans une table Celle ci poss de quatre attributs le nom de la variable son type sa valeur initiale ainsi qu une liste des op rations qui lui sont applicables dans la table e LogicElement Cette clas
51. ichier Java Une description complete du fichier Java g n r ainsi que de certaines r gles de traduction utilis es se trouvent dans la section 3 2 3 2 Fichier Java Ce fichier Java est donc le r sultat de l appel la m thode write de la classe Transla tor Cette m thode va utiliser les informations tri es au pr alable lors de la phase de tri et les passer l outil JavaWriter afin de g n rer le fameux fichier Java dont la structure est d taill e la section 3 2 2 La m thode write consiste en une succession d appels aux diff rentes m thodes de la classe Java Writer telles que writeActions writeVariableDe clarations etc Chacune des ces m thodes est en fait responsable de la g n ration d un l ment de la structure du fichier Java Une de ces m thodes la m thode writeSimulate a notamment pour but de g n rer la m thode simulate d crite dans la section 3 2 1 Une autre m thode importante la m thode write Table est responsable de la traduction des tables logiques et donc du comportement du mod le en code Java Cette op ration est a la fois la t che centrale et la plus complexe de la traduction C est pourquoi elle a fait l objet de l tablissement de plusieurs r gles de traduction d crites dans la section 3 2 3 3 2 1 M thode simulate La m thode simulate d un fichier Java virtualisant un mod le ADEPT est donc la m thode qui est appel e afin g n re
52. ient les noeuds associ s aux actions du mod le Chacun des noeuds contient simplement le nom de l action A laquelle il se rapporte un attribut action Type permettant de sp cifier le type de l action et donc si celle ci doit tre interpr t e comme une commande ou une observation Par d faut dans le fichier le contenu des attributs action Type est mis sa valeur de base c est dire que les actions sur les timers O sont des observations et que les actions sur les composants visuels C sont des commandes Voici par exemple un morceau de la partie relative aux actions issue du mod le Light Pour finir on retrouve le noeud lt Functions gt qui contient les noeuds relatifs aux fonc tions F du mod le Voici par exemple le d but de la partie relative aux fonctions tir e du mod le Autopilot L entierete du fichier de configuration li au mod le Light se trouve l annexe D 3 6 2 Exemple du mod le Light simplifi Afin d illustrer le fonctionnement des fichiers de configuration le mod le Light va tre simplifi sous une forme plus l g re c est dire en enlevant la variable life du mod le ainsi que le composant visuel powerStatus et les colonnes 3 et 4 de la table topLogic Table Au niveau du fichier de configuration on obtient ceci pour les tables logiques et les situations colonnes 39 Y lt Situation used true gt 5 lt
53. illustre le mod le VTS 6 2 ou dit du Vehicle Transmission System 6 4 Ensuite on retrouve l exemple du mod le CountDown 6 3 suivi du mod le VCR ou dit du Video Cassette Recorder Pour finir l exemple complexe du mod le Autopilot simplifi a galement t illustr 6 5 Les r sultats complets de chacune de ces valuations se trouvent dans le r pertoire Modeles de l annexe CD ROM 6 1 Exemple du mod le F D Le mod le F D est donc une petite partie tr s simple du mod le Autopilot dont le comportement est d crit par deux tables captainsFdSystemTable fig 6 1 et firstOffi cersFdSystemTable fig 6 2 Cependant comme pour l exemple d extraction d une table donn la section 4 2 il faut trouver et utiliser la table contenant les actions qui permettent de modifier les inputs des deux tables du mod le F D Ces actions sont mcpCaptainsFd Switch mouseClicked et mcpFoFdSwitch mouseClicked qui sont contenues dans la table apFdAtInterfaceAction Table captainsFdSystemTable L apFdAtInterfaceActionTable outputState no action D user toggles captains fd switch e o L captainsFdSystemTable outputState captains FD on e captains FD off e L captainsFdSystem Table outputState captains FD off e captains FD on e FIGURE 6 1 La table captainsFdSystem Table issue du mod le Autopilot 51 firstOfficersFdSystem Tabl
54. int double ou float et que la valeur contient un nombre positif ou n gatif alors on lui assignera 28 ce nombre Finalement si la variable est un nombre et que la valeur contient une expression complexe commen ant par un symbole tel que ou n tant pas suivi dun chiffre alors on concat ne simplement l expression la variable dans le code Java Le code complet du fichier Light java se trouve l annexe B 3 3 Compilation du fichier Java Cette op ration est donc la deuxi me tape de la traduction apr s la g n ration du fichier Java par l outil Translator Elle consiste en la compilation de ce programme Java g n r gr ce la m thode Runtime getRuntime erec Cette m thode permet d ex cuter la commande pass e en param tre Dans notre cas la commande va compiler le fichier Java li au mod le et placer le fichier class r sultant l ou se trouve le code source de la classe JpfHmi son emplacement ayant t obtenu au pr alable gr ce au caract re r flexif du langage Java De plus un m canisme permettant d afficher les erreurs de compilation ventuelles a t ajout afin d informer l utilisateur en cas de probleme Le code source de cette deuxi me tape se trouve dans la classe ADEPT2LTS dont le code source se trouve annexe E 3 4 Appel la m thode simulate Cette troisi me et derni re tape consiste donc en l appel la m thode simulate vo qu e dans la section 3 2 1 e
55. ion du mod le ADEPT vers le HMI LTS quivalent Si cette option n est pas sp cifi e le fichier de configuration utilis par d faut est celui portant le m me nom que le mod le traduire Utilisation config c file name bisim Cette option permet l utilisateur d indiquer l outil qu il souhaite effectuer une transformation du HMI LTS ou mod le syst me obtenu vers son mod le mental par la m thode de bisimulation r duction Le r sultat de cette transformation est stock dans un fichier texte portant le nom du fichier de configuration associ bisim et ayant une extension mental fichierConfigurationbisim mental Utilisation bisim 49 learn Cette option permet l utilisateur d indiquer l outil qu il souhaite effectuer une transformation du HMI LTS ou mod le syst me obtenu vers son mod le mental par la m thode de learning Le r sultat de cette transformation est stock dans un fichier texte portant le nom du fichier de configuration associ learn et ayant une extension mental fichierConfigurationlearn mental Utilisation learn tdfa Cette option permet l utilisateur d indiquer l outil qu il souhaite effectuer une transformation du HMI LTS ou mod le systeme obtenu vers son mod le mental par la m thode de Le r sultat de cette transformation est stock dans un fichier texte portant le nom du fichier de configuration associ tdfa
56. is dans l annexe H 1 cptSwitch mC 4 cptSwitch mC 8 foSwitch mC 1 1 foSwitch mC 2 foSwitch m cptSwitch mC foSwitch mC 10 cptSwitch mC a Mod le syst me b Mod le mental FIGURE 6 3 Repr sentation du HMI LTS li au mod le F D 52 6 2 Exemple du mod le VTS Ce mod le est bien connu car il est pr sent dans divers articles notamment 2 et 4 dont il a t tir La premiere tape pour pouvoir tester la nouvelle version du jpf hmi sur ce mod le tait de mettre ce syst me sous forme dun mod le ADEPT exploitable par ADEPT2LTS La table logique qui a t construite via l outil ADEPT pour repr senter ce systeme est compos e de seize colonnes et de huit diff rents tats d output Une repr sentation de celle ci se trouve a la figure 6 4 topLogic Table ACTIONS pushUp mouseClicked ejoj ojo pullDown mouseClicked ele up Timer actionPerformed ojo olo downTimer actionPerformed D D D e e L topLogicTable outputState Low1 D e Low2 D e e Low3 D e Medium e e e Medium2 ele e Highl D D High2 e e e High3 D e topLogicTable outputState r Lowl e Low2 D e Low3 e e Medium1 D e Medium e e High1 ele e High2 D e e High3 e FIGURE 6 4 La table topLogicTable venant du mod le VTS Une fois le mod le VTS obtenu
57. isable par les algorithmes de Poutil jpf hmi Comme d j dit pr c demment cet outil poss de d j un dispositif per mettant l extraction d un HMI LTS partir d un fichier texte lts contenant les tats et les transitions du mod le repr sent Pour ce faire jpf hmi utilise une classe appel e LTS Loader contenue dans la package gov nasa jpf hmi models util qui contient une m thode pour importer un HMI LTS et une autre pour en exporter un D s lors pour conserver une certaine coh rence avec ce qui avait d j t cr une classe ADEPT2LTS a t ajou t e dans le m me package De plus cette classe a t structur e de mani re semblable la classe LTSLoader dans le sens o elle contient elle aussi une m thode loadLTS qui renvoie un HMI LTS Par contre la comparaison s arr te l car ajouter la possibilit de retraduire un HMI LTS en un fichier sgb de mani re analogue la m thode saveLTS n aurait aucun sens et semble fort complexe La transformation d un fichier sgb en un HMI LTS exploitable par l outil jpf hmi est repr sent e la figure 3 1 et se d roule en trois grandes tapes e Traduction du fihcier sgb en un fichier Java simulant l automate e Compilation de ce fichier Java e Appel la m thode simulate du fichier Java permettant la simulation du mod le La premi re tape est g r e par un outil appel le Translator dont le fonctionnement est d crit dant la section 3 1 Le r
58. it l appel la m thode li e la valeur si celle ci indique une fonction le contenu de la variable li e la valeur si celle ci indique une variable ou alors on lui assigne un String contenant la valeur si celle ci est une expression e simt variable F function gt variable function stmt variable V variable2 gt variable variable2 stmt String variable expr gt variable String expr stmt Boolean variable expr gt variable expr stmt Number variable number gt variable number V V V V V V stmt Number variable expr gt variable expr Finalement la derni re possibilit est que l l ment soit une variable classique D s lors la traduction va d abord d pendre du type de la valeur et ensuite du type de l l ment String Boolean ou Number Tout d abord si la valeur est une fonction alors on assignera simplement la variable l appel cette m thode Ensuite si la valeur est elle m me une autre variable on assignera l l ment le contenu de la variable indiqu e dans la valeur Il faut d s pr sent regarder au type de la variable indiqu e en l ment Si celle ci est un String alors on lui assignera un String contenant l expression indiqu e comme valeur Si c est un Boolean on lui assignera simplement la valeur de l expression Si la variable est de type
59. kopoulou Charles Pecheur and Michael Feary A formal framework for design and analysis of human machine interaction In 2011 IEEE International Conference on Systems Man and Cybernetics IEEE 2011 Jean Michel DOUDOUX Developpons en java 38 dom document object model http www jmdoudoux fr java dej chap dom htm Michael Feary Automatic detection of interaction vulnerabilities in an executable specification In Proceedings of the 7th international conference on Engineering psy chology and cognitive ergonomics EPCE 07 pages 487 496 Berlin Heidelberg 2007 Springer Verlag Michael S Feary A toolset for supporting iterative human automation interaction in design Technical Report 20100012861 NASA Ames Research Center March 2010 Dimitra Giannakopoulou Neha Rungta and Michael Feary Automated test case generation for an autopilot requirement prototype In SMC pages 1825 1830 IEEE 2011 Oracle Javadoc http docs oracle com javase 7 docs api 63 64 Na 0 FPF WN H 10 11 12 13 14 15 16 17 18 19 20 21 22 23 Annexe A Fichier Light sgb rStatus nog D I 41 11 ents v nasa arc s nog fade0ut 65 gbe remot E ida Grande de Lucida Grande LEADING HSH 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 lt
60. l d velopp a galement montr qu il tait difficile de tester l effi cacit de ce genre d outil Pour les petits mod les on peut tre certain de la validit de ADEPT2LTS car les r sultats collent avec ceux des traductions manuelles et il sont ais ment v rifiables mentalement Cependant pour les plus grands mod les il est impossible de certifier la validit des automates obtenus tant ceux ci sont vastes De plus la validit des automates obtenus par traduction manuelle des grands mod les n est pas elle m me prouv e 61 En terme de performances temporelles la seule partie sur laquelle l impl mentation de l outil ADEPT2LTS pourrait avoir un impact est celle relative la traduction dun mod le en un fichier Java En effet les parties li es la simulation du mod le et la transformation de l automate obtenu sont directement issues de ce qui avait d j t r alis dans la version initiale de jpf hmi Or au vue des r sultats obtenus la section 6 6 le temps n cessaire la traduction semble lev par rapport aux temps de simulation et de transformation pour de petits mod les Cela indique qu une am lioration en terme de performances temporelles serait certainement possible et b n fique pour l outil Par contre si Pon regarde les r sultats obtenus avec des mod les plus vastes on s apercoit que le processus de traduction semble bien r agir par rapport au nombre de noeuds contenus dans le
61. lAutoflightintent lateralAutoflightReque lateralDirection lateralFlightplanLegM lateralFlightplanLegTy lateralFlightplanNavig lateralFlightplanTarge Ml lateralFlinhtnlanTarne lt I lt I lt I lt I lt I lt I lt I lt I lt I lt IEI a Proper XF Noder CO Property Value name lateralSystemTal description outputState Hold Selected L FIGURE 4 1 Capture d cran du mod le Autopilot une fois ouvert T Behavior Category FEE isNominal True o e 0 e e e False eee goal task V simulationStatus paused running eee lateralinterf e outputState user presses elector knob eee user presses HOLD button e user presses LNAV button e lateralSystem outputState Capture and eral Target Hold Selected Lateral Target Capture and plan Target eee V selectedLateralTargetError gt 179 lt 179 84 s rror gt 179 gt 179 m alrspeedTargetSy verticalSystemTable lateralSystemTable 23 11 Navigator 23 EE val gt settings bin gt dot gt images gt jar v sgb 4 1 Structure Rc Problems 7 Logic Deb Package E 7 Situation lt o Y HOSE TRK HOG 4180 ALTITUDE 5000 CLB Init Em avec ADEPT Les tables du mod le sont structur es de sorte pouvoir facilement distinguer les actions effectu es par l utilisateur sur l interface les d
62. les tats du mod le state txt et sur celui conte nant les transitions transition txt on peut construire une repr sentation dun mod le sous forme de diagramme comme celui de la figure 3 5 Cette repr sentation est issue de l analyse des fichiers texte se trouvant dans l annexe C et repr sentant l automate obtenu de la traduction du mod le Light 3 6 Fichiers de configuration Lorsque l on souhaite effectuer une analyse sur un mod le ou en r cup rer le mod le mental on pourrait vouloir analyser le mod le dans son enti ret ou alors simplement une partie de celui ci De plus dans certains cas comme le mod le Autopilot il est tout simplement impossible de g n rer un HMI LTS tant le mod le est vaste et complexe En effet la simulation de celui ci est beaucoup trop co teuse en terme de m moire pour le mat riel notre disposition D s lors il a fallu trouver une solution pour permettre de limiter la traduction dun mod le une partie de celui ci Une des solutions aurait pu tre d obliger l utilisateur r duire lui m me le mod le directement dans ADEPT mais cela n aurait pas t pratique du tout Une bien meilleure solution f t de permettre l utilisateur de joindre un fichier de configuration au mod le qu il souhaite analyser Ces fichiers de configuration se retrouve sous la forme d un fichier XML dont l extension est conf et dont la structure est d taill e dans la section 3 6 1 31
63. les valeurs que peut prendre une variable lors de la simulation du mod le Voici par exemple la partie relative aux variables du fichier de configuration issu du mod le Light lt Variables gt lt Var used true observable true max min gt state lt Var gt lt Var used true observable true max min gt life lt Var gt lt Variables gt De mani re un peu similaire aux variables on retrouve un noeud lt Components gt qui contient les composants visuels du mod le Cependant ceux ci ne poss dent pas d attributs max et min Voici la partie relative aux composants visuels du fichier de configuration tir du mod le Light lt Components gt lt Comp used true observable true gt powerStatus lt Comp gt lt Components gt 34 UR WN ro a no F W N ro oO F WN E a nF WN ro On retrouve ensuite un noeud lt Outputs gt qui contient les noeuds d finissant les outputs des tables logiques devant tre utilis s comme variables du mod le Pour rappel on ne parle pas ici uniquement des variables dites classiques V mais bien de l ensemble des l ments utilis s pour tester l galit de deux tats du mod le Tout comme les variables et les composants ces noeuds poss dent un flag observable Voici par exemple le d but de la partie relative aux outputs des tables logiques issue du mod le Autopilot Le noeud suivant est le noeud lt Actions gt qui cont
64. lifi Dans cet exemple la traduction est effectu e sur une version simplifi e du mod le Au topilot En effet le comportement de cette version est uniquement d crit par les tables logiques li es la vitesse de l avion airspeed eta sa direction lateral Les tables tant utilis es sont donc airspeedSystem Table airspeedSystem Target Table lateralSystem Table et lateral TargetSystem Table En plus de ces tables il a fallu ajouter les tables permettant de d clencher les inputs des celles ci c est dire les tables airspeedInterface Action Table et lateramInterface Action Table tout comme cela avait t n cessaire dans l exemple donn la section 4 2 Une description plus complete de ce sous mod le est donn e dans 2 la page 232 La transformation de cette version du mod le Autopilot donne 15 016 tats et 165 176 transitions Lorsque l on compare ces resultats avec ceux obtenus manuellement dans 2 on s apercoit qu ils sont completement differents Ce n est pas pour autant que l ou til ADEPT2LTS ne fonctionne par correctement En effet dans ce cas ci la raison de cette grande difference se trouve dans l interpretation de l action no action signifiant justement qu aucune action ne se produit Si Pon est attentif au fichier Java contenant la traduction manuelle du mod le qui est disponible dans le r pertoire Archives second syst abstr 1obs de annexe CD ROM on peut s apercevoir que
65. lin aire par rapport au nombre d tats du mod le Le temps de simulation plus lev pour le mod le CountDown que pour le mod le VTS qui comporte pourtant plus d tats semble indiquer que le nombre de transitions joue aussi un r le dans ce r sultat vu que le mod le CountDown poss de quelques transitions en plus Finalement plus un mod le grandit plus le temps n cessaire l extraction du fichier Java permettant la simulation d un mod le ADEPT semble n gli geable par rapport au temps n cessaire la simulation de celui ci et la transformation du mod le syst me obtenu en un mod le mental 59 60 Chapitre 7 Conclusion L ensemble des am liorations qui ont t apport es l outil jpf hmi et qui ont t pr sent es dans ce document se trouvent dans le package gov nasa jpf hmi models util pierre du code source de l outil ainsi que dans les classes ADEP2LTS et JpfHmi Le package pier re a t nomm comme cela de sorte distinguer clairement ce qui existait d j de ce qui a t ajout l outil La nouvelle version de jpf hmi est donc dot e dun traducteur automatique de mo d le ADEPT Par rapport aux traductions manuelles anciennement effectu es l outil ADEPT2LTS apporte pas mal d avantages Premi rement et c est certainement le plus important les temps obtenus pour les transformations de mod les ADEPT ne d passent pas la seconde m me pour le mod le Autopilot Manuelle
66. liser une variable tout ce qui touche cette variable va galement tre mis de c t Par exemple si une ligne contient l assignation d une variable non utilis e un composant visuel utilis toute la ligne est mise en commentaire et du coup l tat du composant ne change pas L enlevement d une variable peut donc parfois avoir plus de cons quences qu on ne le pense sur le comportement d un mod le Lorsque l on modifie un fichier de configuration il faut tre prudent avec les fonctions qui sont directement victimes du ph nom ne de cascade pr sent juste avant En effet lorsque l on veut utiliser une fonction il faut s assurer que toutes les variables pr sentes dans cette fonction soient bien utilis es En effet si l une des variables de la m thode n est pas utilis e il faut se poser la question de savoir que renvoyer la place du contenu de cette m thode Faut il renvoyer null Cela ne fonctionnerait pas avec les int double etc Renvoyer une valeur en fonction du type du return de la fonction Oui mais quelle 38 valeur renvoyer un 0 par exemple pourrait fausser compl tement le comportement du mod le D s lors le syst me lorsqu il va d tecter une variable non utilis e dans le corps de la m thode va imprimer un message de sorte indiquer l utilisateur dans quelle m thode se trouve son erreur et un commentaire appara tra la ligne concern e dans le fichier Java g n r Si
67. me obtenu LightConfstate txt LightConftransition txt etc Notez que les deux lignes auraient pu tre regroup es en une et donner le m me r sultat mais que celles ci ont t s par es pour des raisons de lisibilit et de clart java JpfHmi configGen LightConf configMod true Light sgb java JpfHmi d v config LightConf bisim tdfa learn Light sgb Ces options et le nom des fichiers g n r s ont t con us de sorte permettre a l uti lisateur d effectuer plusieurs op rations en une fois grace a des scripts En effet le fait de nommer les fichiers contenant les r sultats d une op ration avec le nom du fichier de configuration avec lequel ils ont t obtenus permet de les lier ce fichier de configuration et non au mod le utilis Il est en effet pratique de pouvoir travailler avec plusieurs fichiers de configuration en m me temps sur le m me mod le tout en distinguant les diff rents r sultats obtenus 50 Chapitre 6 Evaluation De mani re similaire l exemple de la traduction de la table airspeed TargetSystem Table du mod le Autopilot pr sent e dans la section 4 2 ce chapitre illustre l efficacit et le bon fonctionnement de l outil ADEPT2LTS en fournissant l valuation du processus de traduction sur plusieurs mod les Le premier d entre eux est le mod le F D 6 1 ou dit du FlightDirector qui est en fait une petite partie du mod le Autopilot Le second exemple
68. ment cela devait prendre des heures pour crire le fichier Java li ce mod le qui compte plus de 1500 lignes En suite l automatisation du processus enl ve le facteur erreur que peut toujours commettre un humain lors de la traduction Cette automatisation du processus a galement apport un peu plus de rigueur dans la repr sentation des mod les en fichier Java En effet lors des traductions manuelles certains l ments des mod les ADEPT pouvaient prendre des formes l g rement diff rentes une fois traduits en Java Par contre le d savantage de l outil ADEPT2LTS est la flexibilit En effet malgr la mise en place d un fichier de configura tion plut t efficace la traduction manuelle offrira toujours plus de flexibilit m me dans le respect des normes de traduction tablie dans ADEPT2LTS Cette nouvelle version de jpf hmi est galement accompagn e d une petite interface facile utiliser simple et suffisamment intuitive Celle ci permet au moyen de scripts d effectuer plusieurs analyses successives ce qui peut tre tr s pratique dans certains cas Associ s au fichiers de configurations l interface est rendue tr s efficace En effet ceux ci permettent d valuer une grande partie des sc narios possibles et imaginables partir d un seul mod le ADEPT Ceux ci malgr leur simplicit d utilisation se sont montr s tr s efficaces lors de l valuation de l outil ADEPT2LTS L valuation de l outi
69. ment toujours une paire l ment valeur mais la traduction de chaque bullet donnera lieu 4 un statement en Java Si l on se base nouveau sur le tableau a la figure 3 4 chaque corps de if statement serait de la forme suivante 27 elementi valuel x element2 value2 x elementn valuen x Cependant tout comme pour les inputs la traduction des outputs se fait selon certaines r gles dans lesquelles chaque bullet est repr sent e par stmt element value e stmt LOGIC L table gt table La premiere possibilit est que l l ment soit l l ment sp cial LOGIC cela veut dire que les valeurs seront des appels d autres tables Donc l operation devient un appel la m thode li e la table pr sente comme valeur e stmt L table outputState state value gt tableOutput table STATE VALUE Deuxi mement si l l ment est l tat d output d une table la variable Java conte nant cet tat sera modifi e et on lui assignera l quivalent de la valeur dans les tats d output possibles de la table e stmt C component field F method gt component field method stmt C component field V variable gt component field variable stmt C component field expr gt component field String expr Ensuite si l l ment est l attribut d un composant visuel alors on lui assigne so
70. miner quel niveau on se trouve et s il on est dans les inputs ou outputs Cette operation est effectu par la m thode behaviorsCreation dont le code source est donn l annexe F 3 1 3 Trosi me tape le JavaWriter L outil Java Writer est donc l entit charg e de g n rer un nouveau fichier Java portant le m me nom que le mod le en traduction et d y crire Le r le du fichier Java g n r est de virtualiser un mod le de sorte pouvoir le simuler afin de pouvoir observer les diff rents tats et transitions qu il traverse et donc de g n rer un automate repr sentant son comportement Une fois que l on appelle la classe Java Writer il faut lui fournir le nom du mod le ainsi que son emplacement afin que l outil cr e automatiquement le fichier Java Cependant le fichier est toujours vide et il faudra le remplir Pour ce faire l outil JavaWriter met disposition diverses m thodes permettant d crire dans ce fichier pr d fini Chacune de ces m thodes permet la traduction d une partie bien pr cise du mod le en son quivalent en code Java La classe Java Writer poss de par exemple une m thode writeActions servant d clarer dans le fichier Java toutes les actions pouvant avoir lieu lors de l ex cution du mod le une m thode writeFunctions permettant la traduction des fonctions F ou encore writeVariableDeclarations qui permet de d clarer les variables classiques du mod le V dans le f
71. n private Action String action this action action public String toString return action Juste en dessous et de mani re similaire on retrouve les d clarations des tats d output des diff rentes tables du mod le Pour chacune des tables ayant un tat d output utilis dans le mod le on retrouve une num ration comme celle ci dessous qui est la d claration de l tat d output de la table lateral TargetSystem Table du mod le AutoPilot 23 move pres ted lateral target to the right ected lateral target to the left teral target to the right teral target to the left lateral target i Une fois tout cela d clar chaque fichier Java repr sentant un mod le contient une sous classe State qui aura pour but de repr senter l tat dans lequel se trouve un mod le Cette classe State ayant pour but de repr senter l tat dun mod le celle ci devra for c ment avoir comme attribut les diff rents l ments qui permettront de distinguer les tats du mod le Les premiers attributs du mod le qui sont d clar s et initialis s sont les variables de celui ci V Voici par exemple la d claration des variables du mod le Light Ensuite ce sont les tats d output des diff rentes tables du mod les qui sont d clar s et initialis s Voici une de ces d clarations li e l output de la table lateral TargetSystem Table issue du mod le AutoPilot 1 priv
72. oci e et enfin si le param tre est un composant la r f rence se fera vers un noeud d clar dans la partie ComponentsKey Chacun de ces noeuds contient galement des sous noeuds d crivant les diff rentes valeurs que peut prendre l l ment Attention que ces sous noeuds peuvent galement faire r f rence d autres l ments du mod le Notez que tout ce qui vient d tre voqu par rapport au noeud racine des inputs est transposable au noeud racine des outputs Voici par exemple les noeuds repr sentants l l ment state dans les inputs de la table topLogic Table du mod le Light 1 Node name state referenceNodeName state class gov nasa arc sgbe remote sgb nodes SgbNode gt 2 lt Node propertyEditor sun beans editors StringEditor name on isValueNode true class gov nasa arc sgbe remote sgb nodes SgbNode gt 3 lt Node propertyEditor sun beans editors StringEditor name fading isValueNode true class gov nasa arc sgbe remote sgb nodes SgbNode gt 4 lt Node propertyEditor sun beans editors StringEditor name off isValueNode true class gov nasa arc sgbe remote sgb nodes SgbNode gt 5 lt Node gt Finalement parmi les noeuds repr sentant les inputs et les outputs d une table on peut galement trouver des param tres sp ciaux Nous les avons d j voqu s plus haut ce sont les parametres sp ciaux ACTIONS et LOGIC Le noeud repr sentant le parametre ACTIONS contient tous les noeuds
73. omates l int rieur de l outil un HMI LTS est en fait impl ment comme une liste de paires tat transition De plus un mod le peut tre enrichi ou non La diff rence entre un mod le syst me enrichi ou non est que le mod le enrichi poss de une observation sur ses tats repr sentant l observation qu un op rateur peut faire lorsque le syst me est dans cet tat joa FIGURE 2 3 Vue d ensemble de l outil jpf hmi tir e de 2 14 Comme on peut le voir dans la figure 2 3 qui repr sente la structure de l outil jpf hmi on peut se rendre compte que ce dernier permet de r aliser cinq op rations diff rentes sur un HMI LTS Les deux premi res sont en fait des analyses des tests sur certaines propri t s d un mod le e FCCheck Cette analyse permet de v rifier si un mod le et donc le HMI LTS le repr sentant respecte une propri t appel e full control Cette propri t met en vidence le fait que pour qu une interaction homme machine soit convenable c est dire que l homme ne soit pas surpris par le comportement de la machine l homme doit conna tre toutes les op rations qu il peut effectuer avec le syst me et doit pouvoir s attendre tout ce qui peut arriver e FCDetCheck Cette op ration v rifie la propri t de Full control determinism d un HMI LTS Les trois op rations suivantes sont en fait les trois diff rentes manieres que jpf hmi met a disposition
74. on de divers syst mes automatis s Il a par exemple t utilis pour mod liser le pilote automatique d un avion de type boeing 777 D un autre cot les chercheurs du d partement INGI ont mis au point un outil capable d analyser un automate repr sentant un syst me automatis et d en extraire la vision qu a l op rateur de ce systeme Or l analyse HMI repose notamment sur la comparaison entre le systeme comme il est dans la r alit et la mani re dont ce systeme est percu par l operateur Cependant il n existe pas encore d outil capable de faire le lien entre un systeme vir tualise dans ADEPT et l outil jpf hmi d velopp par les chercheurs INGI Ce document presente une proposition d implementation d un troisieme outil capable de traduire un systeme virtualise via ADEPT en un automate analysable par l outil jpf hmi Cette presentation se divise en plusieurs parties Premierement afin de bien tablir les bases du nouvel outil une courte description des outils ADEPT et jpf hmi va tre donn e Ensuite le fonctionnement de l outil ainsi que les choix ayant t r alis s quant son implementation seront d crits La partie suivante pr sentera un systeme en particulier le pilote automatique voqu ci dessus Autopilot ainsi que la marche suivre pour le transformer en automate avec l outil d velopp Par apr s un petit manuel d utilisation de l outil sera pr sent contenant la marche suivre po
75. on est repr sent dans la table logique donn e la figure 6 7 topLogic Table ACTIONS Inc mouseClicked ele Reset mouseClicked e Cancel mouseClicked e Start mouseClicked e Ring mouseClicked e V value 0 e 1 D e D 2 H H H e V alarm True e False o o jojo ojo V running True e False ejo o o D V value 0 ele e e ET V alarm True e False e V running True e False D e FIGURE 6 7 La table topLogicTable issue du mod le CountDown Des lors qu une version du syst me sous forme dun mod le ADEPT existait il tait pos sible d obtenir son mod le syst me gr ce ADEPT2LTS Cette traduction donne comme r sultat un automate compos de 6 tats et 11 transitions dont la repr sentation est donn e dans la figure 6 8 Ces r sultats sont les m mes que ceux obtenus par la traduc tion manuelle effectu e dans 2 Le mod le mental obtenu de ce mod le syst me par la technique de learning est repr sent dans la figure 6 9 Les r sultats complets de cette valuation sont pr sent s dans l annexe J 59 5 Inc 6 Reset 8 Cancel 2 Ine 7 Start E 10 tau 9 tau 4 Start 1 Inc 11 Ring FIGURE 6 8 Repr sentation du mod le systeme du CountDown Inc O1 Inc 00 Inc O2
76. oncordent parfaitement avec ceux pr sent s la page 231 de 2 FIGURE 4 7 Repr sentation du mod le mental li la table airspeedTargetSystemTable 4 4 spd lt 252 spd gt 248 FIGURE 4 8 Repr sentation du mod le mental li la table airspeedTargetSystemTable 4 4 lorsque la variable selectedSpeedTarget est observable Cet exemple a permis dans un sens d illustrer une petite partie du fonctionnement du mod le Autopilot mais il a surtout servi illustrer la mani re de proc der pour extraire une table d un mod le gr ce aux fichiers de configuration De plus cette exp rience apporte un l ment de preuve du bon fonctionnement de l outil ADEPT2LTS et de l exactitude des r sultats obtenus avec celui ci Remarquez que des valuations de l outil similaires celle qui vient d tre faite sont effectu es dans la section 6 47 48 Chapitre 5 Manuel d utilisation L outil jpf hmi a t l g rement retravaill afin de permettre l utilisateur de r aliser les transformations de mod les de son choix au moyen de divers lignes de commandes En effet initialement l utilisateur devait modifier le code source de l outil afin de transformer le mod le qu il souhaitait D s pr sent gr ce la classe JpfHmi l utilisateur peut facilement effectuer toutes les sortes de transformations qu il souhaite que ce soit partir d un fichier XML repr sentant un mod le ADEPT
77. ons des bullets dans les diff rentes colonnes des tables logiques est int ressante En effet comme d j voqu dans la section 2 1 4 les colonnes dans les fichiers sgb sont repr sent es comme une suc cession de 0 et de 1 s par s par des et des permettant d indiquer quelles lignes de la table les num ros font r f rence Il existe trois niveaux de crochets chacun servant diff rencier les parties d une colonne Le premier niveau de crochets sert sim plement d limiter la colonne enti re colonne Ensuite le deuxi me niveau est utilis pour s parer les inputs des outputs mais aussi dans certains cas les goals ou les be haviorCategory behaviorCategory goals inputs outputs La possible pr sence de goals ou autres pose probl me lorsqu il faut retrouver l emplacement des inputs et outputs dans la representation La solution ce probleme tait simplement d ajou ter deux variables aux tables issues du SGBParser servant indiquer le positionnement 21 des inputs et des outputs dans les colonnes Finalement le troisi me niveau de crochets permet de s parer les diff rents l ments pr sents comme inputs ou outputs dans la co lonne in1 in2 in3 out1 out2 D s lors pour r cup rer le contenu des colonnes il suffit simplement de traverser le string la repr sentant caract re par caract re en utilisant un compteur sur les crochets afin de d ter
78. output prendre en compte comme on peut le voir dans la table situ e la figure 4 4 selectedSpeedTarget Cette premi re variable doit tre limit e entre 248 et 252 et ne pas tre observable afin de respecter ce qui a t fait dans 2 et pour obtenir les m me r sultats lt Var used true observable false max 252 min 248 gt selectedSpeedTarget lt Var gt airspeedTarget De la m me mani re que la premi re variable cette variable doit galement tre non observable et limit e entre 248 et 252 44 lt Var used true observable false max 252 min 248 gt airspeed Target lt Var gt e airspeedTargetSystemTable outputState Cet output est utilis car il est bien pr sent dans la table et est de plus utilis comme variable pour tester l galit de deux tats Tous comme les variables celui ci est non observable 1 Out used true observable false gt airspeedTargetSystemTableOutputs lt Out gt Finalement il faut indiquer dans le fichier de configuration les actions que Pon souhaite utiliser comme transitions dans l automate genere Dans 2 on utilise les outputs de la table airspeedInterfaceActionTable comme transitions ce qu il n est pas possible de faire avec un fichier de configuration comme expliqu dans la section 3 6 4 Cependant si Pon cherche un peu dans cette table on se rend compte que les outputs dont on a besoin sont directement lies a deux actions du modele ADE
79. plus il faut savoir que les colonnes sont lues de gauche droite ce qui veut dire que l on teste les inputs d une colonne uniquement si les pr c dentes ne conviennent pas Vous remarquerez sans doute qu il manque l l ment sp cial PRIMITIVES dans l illustration de la topLogicTable du mod le Light ce qui est normal car l l ment PRIMITIVES g re le d marrage des timers Or la construction de l automate li au mod le ne n cessite pas de savoir quand les timers d marrent seul le moment o ils arrivent z ro et ils se d clenchent importe et est traduit en un v nement pouvant survenir dans l environnement du syst me Ces v nements sont les m mes que ceux qui ont d j t voqu s dans la section 2 1 2 topLogic Table ACTIONS power mouseclicked ele fadeOut mouseclicked e life Timer actionPerformed e fading T imer actionPerformed D V state on D fading e off e ele V life 1 D C powerStatus background 255 0 0 e elo 0 255 0 FIGURE 2 2 La table topLogicTable issue du modele Light 2 1 4 Les fichiers SGBs Un fichier sgb est un fichier XML contenant toutes les donn es relatives la description d un mod le ADEPT Tout comme les fichiers XMLs un fichier sgb contient une sorte d arbre compos de noeuds et de sous noeuds repr sent s entre lt
80. r finir la possibilit de limiter les fonctions utilis es a t ajout e Cependant celle ci n a pas t ajout e dans le but de diminuer le nombre de variables d un tat ou le nombre de transitions lors de la simulation d un mod le mais plut t pour viter les probl mes de compilation avec le fichier Java g n r En effet la non s lection d une variable par exemple pourrait entra ner une erreur dans le corps d une m thode si celle ci fait appel cette variable Une fois les caract ristiques des fichiers de configuration d termin es il a fallu galement r fl chir un syst me pour r cup rer les donn es contenues dans ces fichiers Pour ce faire un outil ConfParser a t ajout l outil Translator Cet outil va simplement r cup rer 33 NG O WN ro Bowne 1 2 3 les informations contenues dans un fichier de configuration et les transmettre l outil Translator qui va lui m me les donner l outil JavaWriter En effet c est cet outil qui va lors de la traduction du mod le vers son quivalent en fichier Java v rifier que les informations qu il est sur le point d crire dans le fichier doivent tre utilis es et sont donc pr sentes dans le ConfParser 3 6 1 Structure Chaque fichier de configuration g n r a la m me structure Comme cela a d ja t dit auparavant le contenu des fichiers s apparente a des balises de fichiers XML Comme pour les fichiers de type sgb
81. r le HMI LTS correspondant Son but est donc bien de virtualiser le mod le de le simuler d en collecter les tats et les transitions puis de les renvoyer sous la forme d un HMI LTS repr sent dans le code source comme une instance de la classe LTS lt ExtendedState Transition gt 22 0 o NA UM WN E Pour simuler un mod le la toute premi re tape est de r cup rer l tat initial de celui ci La mani re dont les tats et les actions sur ceux ci sont repr sent s en code Java est d taill e ci apr s dans la section 3 2 2 Une fois que l on a l tat de d part celui ci est ajout une liste d tats explorer et une liste d tats d j visit s Ensuite tant que la liste des tats explorer n est pas vide on va explorer le premier tat de cette liste en testant l effet de chaque action pr sente dans le mod le sur cet tat Le tuple tat de d part action tat d arriv e forme une transition qui est ajout e la liste des transitions si elle ne s y trouve pas d j Pour finir chaque tat r sultant est ajout la liste des tats visit s si ils ne s y trouvent pas d j ainsi que dans la liste des tats explorer Enfin pour construire le HMI LTS on va parcourir la liste des tats visit s et celle des transitions pr c demment cr es afin de g n rer les tats enrichis du mod le et les transitions entre ceux ci et d ajouter tout cela au HMI LTS qui sera finalement renvoy
82. raduit sous forme de code Java gr ce aux r gles s mantiques de traduction nonc es dans la section 3 2 3 Dans le code Java chacune des colonnes de la table logique deviendra un if statement dont la condition sera la traduction des inputs de cette colonne en Java et le contenu la traduction des outputs de cette m me colonne Voici par exemple la traduction en code Java de la table top Logic Table issue du mod le Light et de ses colonnes 0 et 4 private static ve T fading 0507 25 16 17 18 Le code complet du fichier Java repr sentant le mod le Light se trouve dans l annexe B 3 2 3 R gles de traduction d une table logique Cette section contient donc les quelques r gles de traductions relatives au contenu des tables logiques Ces r gles d coulent de l observation des possibilit s offertes par le logiciel ADEPT pour la confection des tables logiques et sont inspir es des r gles s mantiques d j tablies dans 2 element 1 value 1 1 value 1 n element 2 value 2 1 value 2 n element n value n 1 value n n element 1 value 1 1 value 1 n element 2 value 2 1 value 2 n element n value n 1 value n n FIGURE 3 4 Structure des tables logiques INPUTS Comme d j dit pr c demment les inputs d une table logique peuvent se traduire en un if statement en Java Donc chaque bullet pr sente dans la parti
83. raisons que la premi re action il faut indiquer cette action comme etant une commande 1 Act used true type COMMAND gt airspeed Target DecreaseTimer actionPerformed lt Act gt 4 2 2 R sultats Une fois le fichier de configuration compl t comme ci dessus on peut alors extraire le HMI LTS li la table logique airspeed TargetSystem Table simplifi e du mod le Autopi lot Pour v rifier exactitude et le bon fonctionnement du fichier de configuration il est utile de jeter un oeil aux fichiers texte g n r s se trouvant dans l annexe G Le fichier des tats contient 9 tats et le fichier des transitions contient 27 transitions dont 9 transi tions tau L automate d crit dans ces fichiers a ensuite t mis sous forme de diagramme pour obtenir la repr sentation donn e la figure 4 6 Dans celle ci le symbole re pr sente l action airspeedTargetIncreaseTimer actionPerformed le symbole repr sente l action airspeed Target DecreaseTimer actionPerformed out d signe l output de la table 45 airspeed TargetSystem Table et finalement spd d signe la variable selectedSpeed Target Remarquez que les 11 transitions ayant un m me tat comme point de d part et d arriv e n ont pas t reprises De plus notez que les num ros des tats et des transitions sont ceux qui leurs ont t attribu s dans les fichiers texte d crivant l automate qui sont disponibles annexe G Cett
84. rtiesKey etc Voici par exemple un morceau du noeud Node du mod le Light 13 1 code name Root referenceNodeName Root class gov nasa arc sgbe ui systen SystemReferenceNode bbKey SubSystemKey gt 2 lt Node name power referenceNodeName power class gov nasa arc sgbe ui system SystemReferenceNode bbKey ComponentsKey gt 3 lt Node gt Le code complet du fichier sgb repr sentant le mod le Light se trouve dans l annexe A 2 2 JPF HMI L outil jpf hmi a t d velopp par S bastien Comb fis dans le cadre de sa these de doctorat Comme il le dit lui m me dans 2 jpf hmi est en quelque sorte une extension du Java PathFinder JPF qui analyse transforme et v rifie les propri t s de divers automates Cette section pr sente en quelques lignes cet outil ses caracteristiques et les diff rentes op rations qu il peut effectuer sur un automate donn 2 2 1 Description de l outil Le r le de l outil jpf hmi est de transformer des modeles systemes en modeles mentaux ou d effectuer quelques analyses sur ceux ci Comme d crit dans 4 un mod le syst me permet de d crire le comportement dun syst me tandis qu un mod le mental d crit la connaissance d un utilisateur par rapport ce systeme la mani re dont l utilisateur le per oit Ces mod les sont repr sent s par ce que l on appelle des HMI LTSs qui sont en fait une sorte de syst mes de transitions tats LTS ou plus simplement des aut
85. s et confi d autres sous outils de mani re simplifier le processus De nouveau cette division permet lorsqu une erreur se produit de distinguer plus ais ment l origine de cette erreur chaque tape tant testable s par ment La premi re tape consiste lire le fichier sgb et extraire les informations utiles relatives au mod le qu il repr sente L outil responsable de cette tape est appel le SGBParser et son fonctionnement est d taill dans la section 3 1 1 Deuxi mement l outil Translator va trier les informations extraites gr ce au SGBParser de sorte pourvoir donner au JavaWriter ce dont il a besoin et sous la forme la plus efficace possible Ce JavaWriter est l outil r alisant la troisi me tape de la traduction et est utilis par la m thode write de la classe Translator Il a donc pour but d crire les informations qu on lui donne dans un fichier Java Cette troisi me tape est 18 d taill e dans la section 3 1 3 N sgb xml Data ordering FIGURE 3 2 Vue d ensemble de l outil Translator 3 1 1 Premiere tape le SGBParser Le SGBParser est un outil qui comme son nom l indique aura pour objectif de parser un fichier sgb donn tant donn qu un fichier sgb est en r alit un fichier au format XML le SGBParser va se baser sur un parseur traditionnel et existant de fichiers XMLs Dans ce cas ci le parseur Java utilis est un parser de t
86. s fichiers Le probl me avec cette mani re de structurer un fichier de configuration sous forme de noeuds c est que ce nombre de noeuds est directement proportionnel au nombre d l ments du mod le et donc sa taille Or comme cela a d j t mentionn et comme cela va tre illustr dans la section 4 certains mod les peuvent tre tr s vastes et complexes pouvant d s lors n cessiter des fichiers de configuration de plusieurs centaines de lignes Pour pallier ce probleme de taille un outil du nom de ConfGenerator a t ajout l outil ADEPT2LTS permettant de g n rer automatiquement un fichier de configuration depuis un mod le donn ConfGenerator La classe ConfGenerator est donc une classe qui permet de mani re un peu similaire la classe Java Writer de g n rer automatiquement un fichier de configuration li un mod le Cette classe met disposition diverses m thodes permettant d crire chacune des parties du fichier de configuration en fonction des donn es qu elles re oivent en param tre Ces donn es c est en fait l outil Translator qui va lui fournir et ce gr ce une nouvelle m thode qui lui a t ajout e et qui sera elle m me appel e par l outil ADEPT2LTS et sa m thode generateConfigurationFile Une caract ristique de l outil ConfGenerator est qu il prend comme param tre un mode permettant de d finir le mode utilis pour la g n ration du fichier de configuration Il e
87. s logiques de modifier les l ments de l interface visuelle V Variable Cette entit repr sente les variables classiques du systeme mod lis Celles ci sont en fait comme des variables Java et peuvent avoir les m mes types que ces derni res On les trouve la fois en tant qu l ment ou comme valeur d un l ment et ce aussi bien dans les lignes d inputs que d outputs des tables logiques O Objet Cette entit repr sente les v nements qui peuvent survenir dans envi ronnement du syst me mod lis On peut les trouver dans les lignes d inputs des tables logiques aux c t s des actions sur les composants comme valeur de l l ment sp cial ACTIONS Ces actions appartiennent au deuxi me type d actions existant dans ADEPT les observations Cela signifie que ce sont des actions sur lesquelles l op rateur n a aucune influence qu il ne fait que les observer mn Fonction Cette entit repr sente les fonctions que l utilisateur peut ajouter au syst me mod lis De la m me mani re que les variables ces fonctions sont en fait des m thodes Java et se comportent donc comme telles Dans une table logique une fonction appara t toujours comme valeur d un l ment celui ci pouvant tout aussi bien se trouver dans les inputs que dans les outputs Elles peuvent par exemple tre utilis es pour calculer une valeur en fonction de plusieurs variables du syst me r
88. sa arc sgbe remote sgb nodes SgbNode gt lt Node gt lt Node propertyEditor sun beans editors IntEditor name 0 isValueNode true class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node gt lt Node gt lt Node name ACTIONS class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node featureName power mouseClicked name power mouseClicked referenceNodeName power class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node gt lt Node featureName fadeDut mouseClicked name fade0ut mouseClicked referenceNodeName fadeDut class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node gt lt Node featureName lifeTimer actionPerformed name lifeTimer actionPerformed referenceNodeName lifeTimer class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node gt lt Node featureName fadingTimer actionPerformed name fadingTimer actionPerformed referenceNodeName fadingTimer class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node gt lt Node gt lt Node gt lt Node name OUTPUTS class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node name state referenceNodeName state class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node propertyEditor sun beans editors StringEditor name on isValueNode true class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node gt lt Node propertyEditor sun beans editors StringEditor name fading isValueNode tr
89. sa colonne 0 decoule directe ment de la limitation pr sent e dans la section 3 6 4 En effet c est elle qui fait appel aux tables system Table et action Table system Table Cette table et sa colonne 0 sont utilis es car elles permettent d ac c der la table airspeed TargetSystem Table action Table Cette table et sa colonne 0 sont utilis es car elles permettent d acc der la table autoflightPanelInterfaceAction Table autoflightPanellnterfaceAction Table Tout comme les deux tables pr c dentes il faut utiliser cette table et sa colonne 0 car cette derni re permet l acc s la table airspeedInterfaceAction Table airspeedInterfaceAction Table Cette derni re et sixi me table ainsi que ses colonnes 1 2 et 4 sont n cessaires car c est sa valeur d output qui est utilis e comme input de la table airspeed TargetSystem Table Elle sert d s lors apporter une variation dans cet input utoflightPanellnterfaceActionTable airspeedinterfaceAction Table action Table systemTable airspeedTargetSystemT able FIGURE 4 5 Repr sentation des appels entre les tables Le fil de d clenchement des tables est repr sent a la figure 4 5 Une fois que les tables utiliser ont t indiqu es il faut indiquer les variables et les outputs dont l on souhaite se servir pour caract riser les tats de l automate que l on obtiendra Dans ce cas ci il y aura deux variables et un seul
90. sateur et des v nements qui pourraient survenir dans l environnement du syst me Il est important de noter que le contenu des tables logiques s apparente du code Java ce qui permet ADEPT d ex cuter et de tester le syst me mod lis Afin d illustrer le concept de mod le ADEPT jetons un coup d oeil au mod le Light qui repr sente une simple lampe pouvant notamment tre allum e ou teinte lorsque l on appuie sur le bouton power et disposant d une dur e de vie limit e Ce mod le est illustr dans la figure 2 1 le montrant lorsqu il est ouvert dans ADEPT Comme on peut le voir dans celle ci la partie droite de la fen tre contient l interface visuelle permettant d ajouter des l ments la repr sentation 2D du mod le Cette interface visuelle sert galement d interface interactive avec l utilisateur lorsque le mod le est ex cut par ADEPT gr ce au bouton TEST La partie centrale de la fen tre est elle destin e montrer le contenu de la table logique actuellement s lectionn e et modifier le contenu de celle ci Finalement la partie gauche contient un browser syst me permettant de naviguer d une table l autre ou d un l ment l autre du mod le Il faut savoir que ADEPT permet la cr ation de cinq types d l ments de cinq entit s diff rentes Ces diff rentes entit s sont d taill es dans la section 2 1 2 Une fois le mod le cr et sauvegard ADEPT va g n rer un fic
91. se repr sente simplement une ligne de la premi re colonne d un table logique celle contenant les l ments et les valeurs la colonne 1 en quelque sorte e Function Cette troisi me classe repr sente simplement une fonction d un mod le Chacune d elle a trois attributs le nom de la m thode le type de la valeur renvoy e et le contenu du corps de celle ci LogicTable Cette classe est celle qui virtualise une table logique et a donc un r le central Chaque instance de la classe Logic Table est d finie par son nom et son tat d output initial Ces tables poss dent deux vecteurs Java compos s d instances de la classe LogicElement l un pour les inputs l autre pour les outputs Cette classe repr sente simplement une valeur d une table associ e un parent qui est en fait l l ment auquel elle se rapporte De plus chaque table contient deux listes de vecteurs de type boolean l une pour les inputs l autre pour les outputs Ces vecteurs d objets boolean repr sentent en fait les colonnes de la table dont l emplacement des bullets est d fini par les boolean ayant true comme valeur Cette mani re de faire a permis de repr senter ais ment et efficacement une table logique et ses colonnes au travers des diff rents vecteurs utilis s En effet le r sultat obtenu est simplement une sorte de tableau dont les colonnes sont des vecteurs La mani re dont sont construits les vecteurs repr sentant les positi
92. t qui se trouve donc dans le fichier class issu de la compilation du fichier Java pr c demment g n r Cette m thode permet donc de simuler le compor tement du mod le repr sent et de renvoyer l automate correspondant Pour faire appel cette m thode il aura fallu une fois de plus faire usage du caract re r flexif du langage Java et de sa m thode Class forName renvoyant la classe dont le nom est donn en param tre Cependant cette m thode ne parvient trouver que les classes tant dans l entourage di rect de la classe qui y fait appel ce qui explique le fait que le fichier Java compil soit plac au m me endroit que le code source de la classe JpfHmi Le code complet de cette tape se trouve dans le code source de la classe ADEPT2LTS donn l annexe E 3 5 Fichiers texte Lors de la traduction dun mod le ADEPT ils est possible de garder une trace du HMI LTS g n r et ce gr ce cinq fichiers texte qui repr sentent l automate produit La g n ration de ces fichiers est optionnelle et se fait lors de la simulation du mod le ADEPT c est dire dans la m thode simulate de la classe li e ce mod le Voici une description de ces cinq fichiers texte state Ce fichier contient la description de tous les tats possibles de l automate c est dire tous les tats que le mod le va atteindre durant son ex cution Chaque ligne du fichier repr sente un tat et chacune d entre elles commence par
93. ter les HMI LTS sous le m me format de fichier gr ce sa m thode saveLTS LTSSaver e ADEPT2LTS Le dernier m canisme permet d importer un HMI LTS partir d un mod le ADEPT et donc du fichier XML sgb qui le repr sente 15 Notez qu une description plus compl te du fonctionnement de l outil jpf hmi et des op rations qu il permet de r aliser est donn e dans 2 En r alit la fonctionnalit per mettant d importer un HMI LTS depuis un mod le ADEPT n est pas impl ment e Le cr ateur de jpf hmi utilisait bien des mod les ADEPT mais il les transformait manuel lement En effet il ajoutait du code Java permettant de g n rer le mod le directement dans le code de jpf hmi Ce travail pr sente donc une proposition d impl mentation de cette fonctionnalite qui permet d importer les HMI LTS depuis un mod le ADEPT de mani re automatique De plus la nouvelle version de jpf hmi qui va tre pr sent e pro pose une petite interface permettant l utilisateur de facilement effectuer des op rations avec l outil Cette interface est d taill dans la section 5 et permet de faire le lien entre les HMI LTSs g n r s par ADEPT2LTS et les algorithmes de transformation d un mod le systeme en un mod le mental d j fournis par jpf hmi 16 Chapitre 3 ADEPT2LTS L outil ADEPT2LTS est une solution au probleme qui est de transformer un fichier sgb d crivant un mod le ADEPT en un HMI LTS quivalent util
94. tie d finit les tables g rant le comportement lat ral de l avion c est dire la direction vers laquelle il se dirige Dans la figure 4 3 qui repr sente la structure compl te des tables du mod le Autopilot les tables concern es par cette division ont t fonc es Les tables les plus fonc es appartiennent la partie relative a la vitesse les moins fonc es la partie relative la direction et entre les deux les tables relatives l altitude De plus chaque table logique est nomm e explicitement en fonction de celle des trois parties laquelle elle appartient 4 2 Traduction d une table Afin d illustrer le mod le Autopilot et une partie de son fonctionnement nous allons tenter d en extraire une table en particulier la table airspeed TargetSystem Table et d ob tenir de celle ci son mod le mental Pour ce faire une partie de cette table va tre isol e du reste du mod le de la m me mani re que la m thode d crite la page 229 de 2 Cette table est repr sent e dans la figure 4 4 airspeedTargetSystem Table r airspeedInterfaceAction Table outputState user rotates Airspeed selector knob clockwise e user rotates Airspeed selector knob counterclockwise e no action D V selectedSpeed Target lt 255 e gt 245 L airspeed TargetSystem Table outputState increase IAS airspeed target e decrease IAS airspeed target e
95. udier pour obtenir l automate repr sentant un mod le Par contre les noeuds repr sentant les diff rents inputs et outputs des tables ne sont pas diff rents en fonction qu ils repr sentent une variable classique ou un composant visuel C est pour cela que Le SGBParser va galement r cup rer le contenu des noeuds lt ComponentsKey gt et lt PropertiesKey gt qui de plus contiennent les valeurs initiales des variables qu ils repr sentent Finalement le noeud lt MethodsKey gt sera galement n cessaire afin de conna tre les fonctions du mod les Le SGBParser va donc transformer et stocker chacun des noeuds utiles en leur quivalent sous forme d une instance d une classe Java Par exemple le noeud lt ComponentsKey gt est 19 FIGURE 3 3 Diagramme de classe UML simple repr sentant la structure de donn es transform en une instance de la classe ComponentsKey qui elle m me contient une liste d instances de la classe Node_ComponentsKey qui sont obtenues par transformation des noeuds fils du noeud lt ComponentsKey gt De mani re analogue l outil SGBParser g n re des instances des classes PropertiesKey et MethodsKey Au niveau du noeud lt LogicsKey gt c est un peu plus compliqu et ce cause des diff rents types de sous noeuds qu il contient Comme cela a d j t dit auparavant ce noeud contient d abord une liste de sous noeuds repr sentant les tables logiques du mod le Chacun de ces no
96. ue class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node gt lt Node propertyEditor sun beans editors StringEditor name off isValueNode true class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node gt lt Node gt lt Node name life referenceNodeName life class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node propertyEditor sun beans editors IntEditor name 1 isValueNode true class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node gt lt Node gt lt Node featureName powerStatus background name powerStatus background referenceNodeName powerStatus class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node propertyEditor gov nasa arc sgbe model beans editors ColorEditor name 255 0 0 isValueNode true class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node gt lt Node propertyEditor gov nasa arc sgbe model beans editors ColorEditor name 0 255 0 isValueNode true class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node gt lt Node gt lt Node name PRIMITIVES class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node featureName lifeTimer start name lifeTimer start referenceNodeName lifeTimer class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node gt lt Node featureName lifeTimer stop name lifeTimer stop referenceNodeName lifeTimer class gov nasa arc sgbe remote sgb nodes SgbNode gt lt Node gt 66 67 68 69 70
97. ur le faire fonctionner correctement Finalement l outil d velopp sera valu gr ce divers exemples de transformation de syst mes en terme d efficacit ainsi qu en terme de performances temporelles Chapitre 2 Contexte 2 1 ADEPT ADEPT ou Automation Design and Evaluation Prototyping Toolset est un outil d velopp en Java qui a t conqu par la NASA et qui est utilis pour d velopper des prototypes de programmes de dispositifs automatis s afin d valuer les interactions homme machine HMI Ce chapitre pr sente la mani re dont fonctionne ADEPT et comment interpr ter les fichiers repr sentant les mod les qu il g n re 2 1 1 Description de l outil ADEPT permet de cr er des sortes de mod les automatiques virtuels que l on appelle des mod les ADEPT Chacun de ces mod les est compos de deux parties li es entre elles une interface utilisateur interactive et un ensemble de tables logiques L interface utilisateur donne une repr sentation visuelle en deux dimensions du syst me mod lis De plus cette repr sentation est interactive dans le sens o certains de ses l ments permettent l utilisateur d interagir avec le syst me D autre part les tables logiques d un syst me mod lis ont pour but de d crire son comportement En effet elles sont responsables de la mise jour des l ments visuels contenus dans l interface utilisateur en fonction des actions effectu es par l utili
98. utputState no action D user rotates Lateral target selector knob clockwise user rotates Lateral target selector knob counterclockwise FIGURE 6 11 D but de la colonne 8 de la table lateral TargetSystem Table 58 6 6 Performances de l outil Cette section contient une tentative d valuation de l outil ADEPT2LTS en terme de performances temporelles Les performances de l outil vont tre compar e par rapport au performance totale de l outil jpf hmi Les r sultats obtenus en terme de temps sont repris dans la figure 6 12 Dans celle ci la colonne Etats repr sente le nombre d etats composant l automate issu du mod le et la colonne Noeuds repr sente le nombre de noeuds que contient le fichier sgb de ce mod le Ensuite la colonne Trad repr sente la phase de transformation d un fichier sgb c est dire la lecture de celui ci et l criture du fichier Java lui correspondant Pour rappel cette phase est g r e par l outil Translator et est pr sent e dans la section 3 1 La colonne Sim repr sente quant elle la phase de simulation du mod le et de generation du HMI LTS le decrivant qui est pr sent e dans la section 3 4 Finalement la colonne Trans repr sente le processus appliqu un mod le syst me afin d en extraire un mod le mental par une technique de bisimulation Les r sultats obtenus proviennent d une moyenne de dix transformations successives s
99. xiste deux modes l un permettant d utiliser tout les l ments du mod le et donc de mettre les flags used de tout les noeuds true l autre de n en utiliser aucun et donc de mettre tous les flags used false Ce concept de modes permet de simplifier le travail de l utilisateur lorsqu il veut obtenir un fichier bien pr cis En effet s il veut simplement enlever quelques l ments du mod les il utilisera le mode mettant tout 37 les flags a true tandis que s il ne veut utiliser que quelques l ments du mod les il pourra simplement utiliser le mode mettant les flags false et puis mettre true manuellement les quelques l ments dont il a besoin 3 6 4 Limitations L utilisation de fichiers de configuration est tr s pratique pour manipuler les mod les et permet de les modeler de nombreuses fa ons Cependant il faut savoir que ce principe souffre de quelques limitations Une premi re limitation laquelle il faut tre attentif lorsque l on veut traduire un mod le ADEPT comportant plusieurs tables est qu il est toujours n cessaire d utiliser la table topLogic Table m me si on veut mod liser une table compl tement diff rente En effet lors de la simulation d un mod le c est cette table qui est le point de d part et qui fait appel aux autres tables si elles existent De mani re similaire il faut faire attention a utiliser toutes les tables menant la table que l on souhaite traduir
100. ype DOM Document Object Model dont la sp cificit est de renvoyer toutes les informations contenues dans le fichier XML sous la forme dun arbre Cependant le format de cet arbre ainsi que la mani re d acceder aux informations qu il contient ne sont pas tr s pratiques dans le cas ou les donn es contenues dans le fichier sont structur es comme dans un fichier sgb C est de ce constat que d coule le r le pr cis du SGBParser lire les donn es contenues dans le fichier sgb et les mettre sous une forme plus adapt e Concr tement la classe SGBParser r cup re une structure de donn es sous forme d arbre via le parseur DOM lit les informations qui y sont contenues et les place finalement dans une structure de donn es plus adapt e la r cup ration des informations importantes contenues dans un fichier sgb Cette structure de donn es est repr sent e dans la figure 3 3 et est d taill e ci dessous La nouvelle structure de donn es contenue dans le SGBParser est une fait une s rie de quatre listes Initialement le SGBParser avait t con u de mani re contenir une liste pour chaque l ment de l architecture d un fichier sgb comme pr sent dans la partie 2 1 4 mais seuls quatre de ces l ments sont utiles dans le processus de traduction Comme cela a d j t dit le noeud lt LogicsKey gt contient tout ce qui est relatif au comportement d un mod le or c est exactement ce comportement que l on doit t

Outils d`analyse de modèles de systèmes interactifs ADEPT

Contents

Download Pdf Manuals

Related Search

Related Contents

Outils d`analyse de mod&egrave;les de syst&egrave;mes interactifs ADEPT

Contents

Download Pdf Manuals

Related Search

Related Contents

Outils d`analyse de modèles de systèmes interactifs ADEPT