Manuel d`utilisation de GénéSyst Laboratoire LSR, équipe VASCO
Contents
1. Les commandes Tous les effacer et Lister chaque dossier sont identiques celle du premier menu ceci pr s que l on parle l de projets et non de dossiers 5 3 Format interm diaire des syst me de transitions tiquet es Oracle Depuis sa version 1 3 janvier 2004 G n Syst permet de g n rer et d exporter le format in term diaire lui servant g n rer les syst mes de transitions tiquet es Les fichiers obtenus par cette exportation portent le doux nom d Oracle car ils peuvent ensuite tre donn s en entr e de l outil afin qu il ne refasse pas les preuves d j effectu es ou qu il oriente les obligations de preuves g n rer pour est r duire le nombre La premi re motivation pour la cr ation d un fichier de format interm diaire est la g n ration du syst me de transitions tiquet es d un raffinement En effet il arrive fr quemment que des erreurs ou des impr cisions soient d tect es lors de la visualisation d un STE Or la g n ration du syst me de transitions tiquet es d un raffinement n cessite de g n r d abord celui de son abstraction Et comme une g n ration est souvent longue il est alors tr s int ressant de pouvoir sauter cette premi re tape De plus une utilisation fine de l Oracle permet de se concentrer sur une partie seulement de la g n ration en for ant temporairement certains r sultats de preuve Ainsi on pourra crire un Oracle d crivant tout2. 2 2 1 Recherche des tats 2 2 2 Calcul des transitions 3 Appels de G n Syst en ligne de commande 3 1 Mode G n ration de syst me de transitions tiquet es eee 3 2 Mode nettoyage u suyus y y te Se OR EE US Ow N 3 3 diras ES ur Gi Rae Seb b d h RE e 4 Interface graphique 41 Mode G n ration de syst mes de transitions tiquet es 4 1 1 Lancement de G n Syst 4 1 2 Ex cution de G n Syst 4 25 Mode nettoyage Lk Ra Jas RU an d h m ae En fa Gas L 5 Sorties et traces de G n Syst 5 1 Mode G n ration de syst me de transitions tiquet es 5 1 1 Fichiers g n r s O an A A R 5 1 2 Traces de G n Syst 21 5 2 Mode Nettoyage 24 5 3 Format interm diaire des syst me de transitions tiquet es Oracle 25 5 3 1 G n ration d un Oracle 26 5 3 2 Utilisation d un Oracle 26 5 3 3 Edition d un Oracle 27 6 Exemples 30 6 1 Distributeur caf Format BCG et DOT 30 7 Preuve d une formule avec l AtelierB 34 8 Bilan 36 Intro
3. Un num ro d signe chaque tat Ce chiffre est choisi par ordre croissant partir de O et attribu par ordre d apparition des tats Ainsi la num rotation des tats raffin s est 0 pour Etat 1 feu rouge 1 pour Etat 1 feu vert et 2 pour Etat 0 Recherche des associations entre tats abstraits et du raffinement L tat 1 est raffin par O or 1 L tat O est raffin par 2 23 Enfin la fin de l ex cution de G n Syst les deux lignes suivantes sont affich es Elles indique le nom du fichier g n r contenant le syst me de transitions tiquet es et le fait que l outil terminer de travaill Il rend donc la main l utilisateur G n ration du fichier MachineACafeClassique dot termin e Fin de la g n ration des syst mes de transitions 5 2 Mode Nettoyage En mode nettoyage le programme va d abord regarder s il y a des projets puis des dossiers susceptibles d avoir t cr s par lui S il n y en a pas il dira simplement Aucun projet effacer n a t trouv Aucun dossier effacer n a t trouv S il y a des projets qui porte comme nom CalculTransitionsTmpxxxn o n est un entier positif alors ils seront tous list s Exemple Projets trouv s CalculTransitionsTmpxxx CalculTransitionsTmpxxx0 CalculTransitionsTmpxxx12556 Ensuite un men
4. des op rateurs Les parenth ses sont obligatoires autour de chacune des quivalences Il est d ailleurs conseill d en mettre galement autour des membre de gauche et de droite ainsi qu autour de chacun des tats comme sur l exemple Afin de ne pas se baser uniquement sur une quivalence syntaxique des obligations de preuve sont g n r es pour montr es l quivalence d entre les tats abstraits donn s dans le raffinement et ceux donn s dans l abstraction Ainsi les obligations de preuve suivantes vont tre g n r es pour notre exemple Etat de Etat membre de gauche d une l abstraction quivalence du raffinement Feu Vert Feu Vert Feu Vert Feu Rouge Feu Vert Feu Orange Feu Rouge Feu Vert Feu Rouge Feu Rouge Feu Rouge Feu Orange Feu Orange Feu Vert Feu Orange Feu Rouge Feu Orange Feu Orange lt gt lt gt lt gt lt lt lt lt lt lt Ensuite comme les OPs 1 5 et 9 sont les seules tre v rifi es par preuve alors nous pouvons faire l association des tats abstraits et des tats raffin s 2 2 2 Calcul des transitions Dans un deuxi me temps l outil va calculer les transitions du syst me de transitions tiquet es du raffinement Seul le calcul vers les tats raffin s est pour le moment implant C est dire que 10 la factorisation des transition n est pas encore support e En fait ce calcu
5. D selectionn zr_boisson D D piece D D mettre fiece D P arreter machine P mettre_ n Figure 6 1 Exemple de g n ration BCG 32 EE G G selectionner_boisson mettre_en_marche arreter_machine rendre_monnaie_2 G G mettre_piece G G mettre_piece rendre_monnaie_1 G G distribuer 116 annuler G G mettre_piece prendre_gobelet G G mettre_piece G G distribuer Figure 6 2 Exemple de g n ration DOT Preuve d une formule avec l AtelierB Dans cette section nous allons simplement expliquer comment nous r alisons des preuves de formules gr ce l AtelierB alors que ce dernier n est pas proprement parler un prouveur de th or me tel que Coq ou PVS Le principe est simple il suffit de g n rer une machine dont les obligations de preuve corres pondent aux formules attendues et de prouver ces derni res l aide de l AtelierB Pour cela si l on met la formule d sir e dans la clause d assertion alors l obligation de preuve g n r e sera ANPNI J o repr sente les conditions sur les ensembles d clar s P les propri t s et J l invariant En fait il est n cessaire de mettre dans cette machine toutes les clauses du syst meB original exception faite des op rations Remarquons simplement que toutes les obligati
6. Dans le cas contraire l AtelierB sera relanc chaque fois qu une obligation de preuve devra tre r solue Ce deuxi me cas semble souvent plus s r et n est pas plus co teux grace la mise en cache de l atelier D ou SymboleD faut G par d faut Ce flag doit tre suivi d un caract re seul sans quotes Ce caract re sera utilis pour indiquer qu une condition du graphique produit n est pas r ductible true P ou SymboleProuv par d faut Ce flag doit tre suivi d un caract re seul sans quotes Ce caract re sera utilis pour indiquer qu une condition du graphique produit est r duc tible true I ou SymboleNonProuve par d faut Ce flag doit tre suivi d un caract re seul sans quotes Ce caract re sera utilis Uniquement dans le cas o le flag E est vrai pour indiquer qu une condition n a pas put tre d termin e malgr les 3 OP g n r e G ou QueGenererOP False par d faut Ce flag doit tre suivi d un bool en true false S il vaut true aucune preuve ne sera effectu e et toutes les machines contenant les obli gations de preuve seront g n r es De plus le dossier de travail ne sera pas effacer DOT True par d faut Ce flag doit tre suivi d un bool en true false S il vaut true alors le r sultat produit sera g n r notamment dans le format DOT HTML True par d faut Ce flag doit tre suivi d
7. associer chaque triplet form d un tat de d part El d un tat d arriv e E2 et d un v nement Ev une condition d atteignabilit Pr E2 peut tre toujours atteignable depuis E1 par Ev T partiellement atteignable depuis E1 par Ev T jamais atteignable depuis E1 par Ev T ou l on peut ne pas conna tre la condition de atteignabilit de E2 par Eu depuis E1 2 27 Equ int ER int EA BoolExt Pr Ce pr dicat sert dans le cas de l Oracle d un raffi nement En effet dans ces cas l G n Syst va chercher retrouver la correspondance entre les tats de l abstraction et les tats du raffinement Cela permet de ne pas contraindre l utilisateur une comparaison syntaxique des tats mais une comparaison s mantique Ce pr dicat associe donc un tat raffin ER et un tat abstrait EA une preuve d quivalence Pr Celle ci a les contraintes suivantes 1 Chaque tat doit tre quivalent 1 et 1 seul autre 2 Pr ne peut pas prendre la valeur Remarque Nous avons vu plus avant que chacune des obligations de preuve g n r es pour faire avancer l outil dans la g n ration du syst me de transitions tiquet es final est conserv e dans le dossier de l Oracle Le nom de chacun des fichier ayant t produit et utilis est not en commen taire dans l Oracle c t du r sultat qu elle a permis d obtenir Par exemple la ligne Init 3 F nit E3 T mch Ilnit E3 F mch indique que
8. etm ETM ASSERTIONS etm arret V etm pret V etm select V etm distri V etm tropp V etm remb INITIALISATION boisson somme af fichage etm rien 0 0 arret OPERATIONS mettre en marche sELECT etm arret THEN etm pret END arreter machine SELECT etm pret THEN etm arret END selectionner boisson SELECT etm pret THEN ANY bb WHERE bb BOISSONS bb Z rien THEN boisson bb somme 0 a f fichage prix bb etm select END END mettre piece SELECT etm select A somme lt prix boisson THEN 30 ANY cc WHERE cc PIECES THEN somme somme valeur cc af fichage af fichage valeur cc END etm select END distribuer SELECT etm select A somme gt prix boisson THEN IF somme prix boisson THENetm distri ELSE etm tropp END END yy rendre monnaie 1 SELECT etm tropp THEN yy somme prix boisson somme prix boisson af fichage 0 etm distri END prendre _gobelet SELECT etm distri THEN boisson rien somme 0 a f fichage 0 etm pret END annuler SELECT etm select THEN IF somme 0 THENaf fichage 0 boisson rien etm pret ELSE etm remb END END zz rendre monnaie 2 SELECT etm remb THEN zz somme somme 0 a f fichage 0 boisson rien etm pret END END 31 P prendre gobelet P D mettre piece D D distribuer D D disy uer D rendre_i
9. 0 T Att 0 1 0 G Ensuite l affichage indique pour chaque tat s il est initial Dans l exemple suivant l tat Eo est initial et l tat E ne l est pas Statut EO est un tat totalement initial Statut El n est pas un tat initial Enfin pour chacun des tats atteignable non encore tudi l outil calcule et affiche pour chaque v nement s il est d clenchable et si oui o il m ne Dans l exemple qui suit la trace indique que les tats num ro O et 1 ont t v rifi s comme atteignables et que l on cherche les transitions qui en partent En l occurrence seul un v nement Prendre_ Monnaie semble d clenchable Il donne lieu deux transitions qui partent de l tat Eo avec une condition r ductible true et m nent respectivement en l tat Eo et l tat Ei avec les conditions d atteignabilit true et G 0 1 Ev nement 0 Prendre_Monnaie 11 Statut Ev nement d clenchable dans l tat 0 Sans cond 11 Recherche des tats d arriv e Statut Transition de EO Vers EO par EvO Sans cond 22 1 Statut Transition de EO Vers El par EvO Sous cond Statut Ev nement non d clenchable dans l tat 1 Ev nement 1 Servir_Cafe Statut Ev
10. Ev6 E4 F mch Att 5 4 7 F Att E5 Ev7 E4 T mch Att E5 Ev7 E4 F mch Att 5 4 8 F Att E5 Ev8 E4 T mch Att E5 Ev8 E4 F mch Att 5 5 2 F Att E5 Ev2 E5 T mch Att E5 Ev2 E5 F mch Att 5 5 3 F Att E5 Ev3 E5 T mch Att E5 Ev3 E5 F mch Att 5 5 4 F Att E5 Ev4 E5 T mch Att E5 Ev4 E5 F mch Att 5 5 5 F Att E5 Ev5 E5 T mch Att E5 Ev5 E5 F mch Att 5 5 6 F Att E5 Ev6 E5 T mch Att E5 Ev6 E5 F mch Att 5 5 7 F Att E5 Ev7 E5 T mch Att E5 Ev7 E5 F mch Att 5 5 8 F Att E5 Ev8 E5 T mch Att E5 Ev8 E5 F mch FIN DU FICHIER 29 Exemples 6 1 Distributeur caf Format BCG et DOT Sur l exemple figure 6 1 nous remarquons que l op ration mettre _ piece peut aller depuis l tat 1 dans n importe quel tat Cela vient du fait que rien n a put tre prouv Ce m me exemple a t produit au format DOT en figure 6 2 Voici le code de la machine B initiale MACHINE DISTRI SETS BOISSONS rien cafe the choc PIECES demiF unF deuxF cingF ETM arret pret select distri tropp remb CONSTANTS prix valeur PROPERTIES prix BOISSONS NAT A valeur PIECES NAT A prix rien A prix cafe 300 A prix the 200 A prix choc 250 A valeur demiF 50 A valeur unF 100 valeur deuxF 200 A valeur cinqgF 500 VARIABLES boisson somme a f fichage etm INVARIANT boisson BOISSONS A somme 0 max ran prix max ran valeur af fichage prix boisson somme
11. changer le num ro associer un tat mais cela n est actuellement pas fait Il faut donc conserver l ordre d apparition des tats et leur num rotation AssocNumEv Ev int Ev String S Ce pr dicat permet d associer un num ro Ev un v nement L v nement en question repr sent ici par la chin de caract res 5 de son nom pr dicat n est actuellement utilis dans G n Syst que pour savoir combien il y a d v nements dans le syst me d crit Dans un proche avenir il pourra aussi servir permettre l utilisateur de changer le num ro associer un v nement mais cela n est actuellement pas fait Il faut donc conserver l ordre d apparition des v nements et leur num rotation Init int E BoolExt Pr Ce pr dicat permet d associer chaque tat E un niveau d ini tiabilit Pr Un tat peut tre totalement initial T partiellement initial G jamais initial F ou l on peut ne pas conna tre son niveau d initiabilit Decl int E int Ev BoolExt Pr Ce pr dicat permet d associer chaque couple form d un tat E et d un v nement Ev une condition de d clenchabilit Pr Ev peut tre totalement d clenchable depuis partiellement d clenchable depuis E G jamais d clenchable depuis F F ou l on peut ne pas conna tre la condition de d clenchabilit de Ev depuis E 9 Att int E1 int 2 int Ev BoolExt Pr pr dicat permet d
12. g n ral peut tre sch matis comme montr sur la figure 1 1 Fithier MCH BoB Fichier HTML GraphViz Format Fichier DOT JBTools GeneSyst a GraphVi Atelier B ou B4free Fichier REF Fichier GKL Figure 1 1 Sch matisation des interactions de G n Syst avec les autres outils 1 3 Installation 1 3 1 Pr recquis L AtelierB ou l outil B4free doivent tre install s pour que l outil G n Syst puisse fonctionner http www b4free com R cup rer et installer la BoB http www lsr imag fr Les Personnes Nicolas Stouls Installation linux seulement Si l application graphiz n est pas install e alors r cup rer et installer le package disponible ici http dag wieers com packages graphviz Shttp www clearsy com html clearsy htm 1 3 2 M thode d installation 1 R cup rer le fichier GeneSyst tar gz http www lsr imag fr Les Personnes Nicolas Stouls 2 Dans le r pertoire d installation de la BoB que nous appellerons BoBdir pour des raisons videntes de comodit faire tar xzvf GeneSyst tar gz 3 Vous devez obtenir un r pertoire GeneSyst contenant 3 ou 4 r pertoires Class Le programme en lui m me Licences Contenant le contrat de licence CeCILL sous lequel est diffus cet outil icons Les icones de G n Syst GraphViz Seulement dans la version UNIX livr
13. les fichiers Init E3 T mch et Init E3 F mch on ser vit la preuve du r sultat de cette ligne F Voici ci dessous un exemple d Oracle Celui est l Oracle d crivant l int gralit du syst me de transitions tiquet es g n r partir de l exemple en section 6 1 et qui d crit les figures 6 1 et 6 2 Fichier g n r automatiquement par G n Syst u CORRESPONDANCE NUMETAT lt gt ETAT syntaxe AssocNumEtat Etat num ro tat pr dicat d crivant l tat AssocNumEtat Etat 0 etm arret AssocNumEtat Etat 1 etm pret AssocNumEtat Etat 2 etm select AssocNumEtat Etat 3 etm distri AssocNumEtat Etat 4 etm tropp AssocNumEtat Etat 5 etm remb CORRESPONDANCE_NUMEV lt gt EV syntaxe AssocNumEv Ev num ro v nement nom v nement AssocNumEv Ev 0 mettre_en_ marche AssocNumEv Ev 1 arreter_ machine AssocNumEv Ev 2 selectionner_ boisson AssocNumEv Ev 3 metire_ piece AssocNumEv Ev 4 distribuer AssocNumEv Ev 5 rendre_monnaie_ 1 AssocNumEv Ev 6 prendre_ gobelet AssocNumEv Ev 7 annuler AssocNumEv Ev 8 rendre monnaie __ 2 ETATS INITIAUX syntaxe Init num ro tat Niveau Preuve Init 0 F Init E0 T mch Init E0 F mch Init 1 T Init E1 T mch Init E1 F mch 28 Init 2 F Init E2 T mch Init E2 F mch Init 3 F Init E3 T mch Init E3 F mch Init 4 F Init E4 T mch Init E4 F mch Init
14. signe le niveau de force de preuve employer dans AtelierB lors de la r solution des obligations de preuve M ou AffichageMinimum False par d faut Ce flag doit tre suivi d un bool en true false Il permet de minimiser l affichage en ne d taillant pas chaque op ration effectu e E ou OPExistentielles False d faut Ce flag doit tre suivi d un bool en true false Il permet de g n rer les obligations de preuve 3 et 6 d crites au chapitre 2 0 ou OracleMachine Ce flag doit tre suivi d un nom de fichier Celui ci doit tre un oracle pour les obligations de preuve de la machine OR ou OracleRaffinement Ce flag doit tre suivi d un nom de fichier Celui ci doit tre un oracle pour les obligations de preuve du raffinement 12 V ou VerifierOracle False par d faut Ce flag doit tre suivi d un bool en true false S il vaut true et qu un oracle est pass en param tre alors l oracle sera utilis pour diriger les obligations de preuves g n r es afin de les minimiser N ou Nettoyer True par d faut Ce flag doit tre suivi d un bool en true false Il permet de dire l outil de laisser les fichiers de travail en place la fin de la g n ration ABP ou AtelierBenParallele False par d faut Ce flag doit tre suivi d un bool en true false S il vaut true alors un processus de l AtelierB sera conserver en m moire
15. un syst me sauf les transitions qui partent d un tat E le temps d affiner la sp cification afin que cette partie de l automate soit bien celle que l on attendait La deuxi me grande raison est de pouvoir affiner par preuve interactive les transitions C est dire que l ensemble des obligations de preuve sont g n r es et crites dans des fichiers mis dans le m me dossier que l Oracle Ainsi si l on pense qu une transition devrait avec une condition r ductible false ou true et que cela n a pas t prouv automatiquement alors on peut r cup rer l obligation de preuve et le prouver soit m me Ensuite Le r sultat doit tre int gr dans l Oracle pour tre pris en compte la prochaine g n ration du syst me de transitions tiquet es du syst me Dans les trois sous sections suivantes nous allons donc d crire comment obtenir un oracle puis comment l utiliser avant de conclure sur comment l diter 25 5 3 1 G n ration d un Oracle Nous appelons un Oracle plein un Oracle contenant les r sultats de la g n ration d un syst me de transitions tiquet es Il est nomm ainsi par opposition avec un Oracle vide qui contient toute la structure syntaxique mais aucun r sultat de preuve Ce dernier type d Oracle est utilis Uniquement pour l dition manuelle cf 5 3 3 Obtention d un Oracle plein Par d faut le format interm diaire Oracle est toujours produit Cependant il
16. 5 F Init E5 T mch Init E5 F mch DECLENCHABILITES syntaxe Decl num ro tat numero v nement Niveau Preuve Decl 0 0 T Decl E0 Ev0 T mch Decl E0 Ev0 F mch Decl 0 1 F Decl E0 Ev1 T mch Decl E0 Ev1 F mch Decl 0 2 F Decl E0 Ev2 T mch Decl E0 Ev2 F mch Decl 0 3 F Decl E0 Ev3 T mch Decl E0 Ev3 F mch Decl 5 6 F Decl E5 Ev6 T mch Decl E5 Ev6 F mch Decl 5 7 F Decl E5 Ev7 T mch Decl E5 Ev7 F mch Decl 5 8 T Decl E5 Ev8 T mch Decl E5 Ev8 F mch ATTEIGNABILITES syntaxe Att num ro tat de part num ro tat d arrivee numero v nement Niveau Preuve Att 0 0 0 F Att E0 Ev0 E0 T mch Att E0 Ev0 E0 F mch Att 0 1 0 T Att E0 Ev0 E1 T mch Att E0 Ev0 E1 F mch Att 0 2 0 F Att E0 Ev0 E2 T mch Att E0 Ev0 E2 F mch Att 0 3 0 F Att E0 Ev0 E3 T mch Att E0 Ev0 E3 F mch Att 0 4 0 F Att E0 Ev0 E4 T mch Att E0 Ev0 E4 F mch Att 0 5 0 F Att E0 Ev0 E5 T mch Att E0 Ev0 E5 F mch Att 1 0 1 T Att E1 Ev1 E0 T mch Att E1 Ev1 E0 F mch Att 1 0 2 F Att E1 Ev2 E0 T mch Att E1 Ev2 E0 F mch Att 1 1 1 F Att E1 Ev1 E1 T mch Att E1 Ev1 E1 F mch Att 1 1 2 F Att E1 Ev2 E1 T mch Att E1 Ev2 E1 F mch Att 1 2 1 F Att E1 Ev1 E2 T mch Att E1 Ev1 E2 F mch Att 1 2 2 G Att E1 Ev2 E2 T mch Att E1 Ev2 E2 F mch Att 1 3 1 F Att E1 Ev1 E3 T mch Att E1 Ev1 E3 F mch Att 5 4 5 F Att E5 Ev5 E4 T mch Att EH5 Ev5 E4 F mch Att 5 4 6 F Att E5 Ev6 E4 T mch Att E5
17. Dans le cas contraire l AtelierB sera relanc chaque fois qu une obligation de preuve devra tre r solue Ce deuxi me cas semble souvent plus s r et n est pas plus co teux gr ce la mise en cache de l atelier Debug Vous devez cocher la case ou pas Ce cas n est utile que lorsque vous poss dez une version de G n Syst qui est en cours de d veloppement Cela permet alors d obtenir des traces d ex cution plus d taill es Symbole D faut Vous devez choisir un caract re dans la liste d roulante Ce caract re sera utilis pour indiquer qu une condition du graphique produit n est pas r ductible true Symbole Prouve Vous devez choisir un caract re dans la liste d roulante Ce caract re sera utilis pour indiquer qu une condition du graphique produit n est pas r ductible true Les valeurs par d faut sont les m mes que dans le cas d un appel en ligne de commande Remarque Certains remarques sont pr ciser Lorsque vous choisissez d indiquer les noms de fichiers partir de Parcourir on v rifie si le fichier choisi est le type de fichier attendu Si ce n est pas le cas vous tes invit rechoisir un autre Lorsque vous souhaitez g n rer que les obligations de preuve alors vous verrez les champs Oracle Machine Oracle Raffinement Force V rifier Oracle se d sactiv s 16 GeneSyst f Machine Canal_Communication mch Parcourir
18. Manuel d utilisation de G n Syst Laboratoire LSR quipe VASCO 681 rue de la Passerelle BP 72 38402 St Martin d h res Cedex Version 1 3 2 du manuel Compil e le 7 novembre 2005 Pour la version 0 1 7 de G n Syst Historique des versions Version 1 2002 premi re r daction de ce manuel Nicolas Stouls Nicolas Stouls imag fr Version 1 0 1 04 02 2004 Relecture et corrections diverses Version 1 1 12 05 2004 Prise en compte des modifications de G n Syst Version 1 2 31 08 2004 Rajout des descriptions de l interface graphique et des possibilit s de formats de sortie Version 1 2 1 01 10 2004 Relecture et corrections diverses Version 1 3 20 05 2005 Prise en compte de la version 0 1 6 2a de G n Syst Version 1 3 1 07 11 2005 Prise en compte de la version 0 1 6 3a de G n Syst Version 1 3 2 17 10 2005 Prise en compte de la version 0 1 7 de G n Syst Contents 1 Introduction LIT Configuration ee DA Ge ey 1 2 Description g n rale 1237 Installations 2721212 RE E Ce S a Tar i p O ge Eo Eo g a V3 1 Pr recquisS s a s us us e se a de ee S Y SON W ON 1 3 2 M thode d installation 2 Algorithmes implant s 2 1 Cas d une sp cification abstraite 2 2 w insu 365 OE
19. Raffinement Canal_Communication_r1 ref Parcourir Oracle Machine ndexMachineAbstr oracle Parcourir r Oracle Raffinement IndexRaffinernent oracle Force 1 M Generer OP existentielle lad Affichage Minimum Nettoyer v Verifier Oracle Que Generer ls Atelier B en parall le Debug Symbole Prouv B Symbole non prouv Symbole Conditionn v Formats de Sortie DOT v RENE vi IGXL_ C NETTOYER LANCER QUITTER G n Syst VO 1 6 23 Figure 4 1 Exemple d utilisation de l interface graphique Tant qu aucun oracle n est fournit le champ V rifier Oracle reste inactif Lorsque vous choisissez en sortie un fichier au format HTML alors automatiquement le format Dot sera aussi g n r 4 1 2 Ex cution de G n Syst Apr s avoir choisi de lancer de G n Syst vous verrez appara tre une fen tre permettant de suivre la trace de son ex cution cf Fig 4 2 Enfin apr s que celle ci soit termin e les deux boutons retour et visualiser deviennent actifs Le premier permet de revenir au menu principal tandis que le second permet d avoir un aper ut de ce que l outil vient de produire Un exemple est donn en figure 4 3 4 2 Mode nettoyage Ce mode sert effacer automatiquement les diff rentes pollutions qui ont pu tre g n r es par l outil Pour acc der ce mode il suffit de cliquer sur le bouton Nettoyer n y a aucun c
20. String S AssocNumEv Ev int Ev String S Init int E BoolExt Pr Decl int E int Ev BoolExt Pr Att int int E2 int Ev BoolExt Pr Equ int ER int EA BoolExt Pr Remarque Attention l ordre d apparition des pr dicats Un Oracle doit toujours commencer par les pr dicats AssocNumEtat Etat puis les pr dicats AssocNumEv Ev oak SN Les fonctions ne sont s par es que par un ou plusieurs retours la ligne Il n y a donc pas de Les types utilis s pour d crire les param tres sont int String et BoolExt Le premier d signe l ensemble des entiers positifs ou nuls le deuxi me est l ensemble des cha nes de caract re Une cha ne de caract res commence et fini par une double quotte Ex Ma chaine Enfin le dernier ensemble est l ensemble des bool ens tendus avec la valeur Gard et la valeur Inconnu Syntaxiquement on notera T la valeur true F la valeur false G la valeur Gard et la valeur Inconnu La s mantique de chacune de ces op rations est la suivante AssocNumEtat Etat int E String S Ce pr dicat permet d associer un num ro E un pr dicat logique d crivant un tat Le pr dicat logique en question est la cha ne de caract re S le repr sentant Sa syntaxe est celle du Ce pr dicat n est actuellement utilis dans G n Syst que pour savoir combien il y a d tat dans le syst me d crit Dans un proche avenir il pourra aussi servir permettre l utilisateur de
21. demand par l utilisateur Ce format d riv du XML est textuel et peut tre utilis par un grand nombre d outils Historiquement le premier format support par G n Syst a t le format bcg qui n cessitait l utilisation de la suite d outils CADP de H Garavel GMS01 GLM02 GM99 Cependant cette sortie a t temporairement desactiv e En effet le format BCG impose certaines contraintes dont le fait que les noms des tats ne peuvent pas tre autre chose que des nombres et qu il n est pas possible de r aliser d automate hi rarchis De plus on ne peut pas mettre de couleurs ou de styles particuliers pour mettre en valeurs certaines informations Un exemple de r sultat obtenu avec la sortie BCG est en section 6 1 et un exemple du m me r sultat obtenu avec la sortie DOT est en section 6 1 5 1 2 Traces de G n Syst Lors de son ex cution en mode g n ration de syst me de transitions tiquet es G n Syst com mence par afficher un tableau r capitulatif des diff rents param tres qu il va utiliser pour son travail En voici un exemple EHEHE HEHE HEHE HE HEHEHE HEHE HEHE HEHE HE HEHEHE EHE HEHE HEHE HE HEHEHE EHE HEHE HEHE HEHE HEHE HEHE HEHE HEHE HEHEHE HEHE HEE HR HHH EH R HHHH H Rappel sur les donn es du traitement W R Fichier du syst me abstrait Distributeur DISTRI3 mch Fichier du raffinement Distributeur DISTRI3_rl ref Faire la v rification d
22. duction 1 1 Configuration requise Ce programme ne tourne que sous UNIX ou LINUX Test uniquement sur les distributions FEDORA Son installation n cessite d avoir pr alablement install les logiciels suivants La BoB outil gratuit d velopp au LSR pour la g n ration des obligations de preuve http www lsr imag fr Les Personnes Nicolas Stouls L AtelierB outil payant d velopp par Clearsy pour la v rification des obligations de preuve http www clearsy com OU B free l outil gratuit pour les possesseurs de l AtelierB ou les universitaires diffus l adresse http www b4free com Sous LINUX seulement car fournit avec la distribution UNIX GraphViz d velopp par AT amp T pour la g n ration des graphiques r sultats partir des fichiers de sortie produits http www graphviz org Une copie du logiciel G n Syst peut tre r cup r e l adresse suivante http www lsr imag fr Les Personnes Nicolas Stouls 1 2 Description g n rale G n Syst est un programme Java diffus sous les termes du contrat de licence Cecill V2 Ce logiciel ne peut tre diffus autrement car il inclut le programme Grappa et n cessite l installation de l application GraphViz 3 qui sont tous deux diffus s sous la licence GPL G n Syst PS04 BC00 00 Ham02 est un outil permettant de g n rer un syst me de transitions tiquet es repr sentant exactement le comportement d
23. e avec Graph Viz et 4 fichiers README txt un fichier qui rappel quelques informations sur l utilisation de GeneSyst Ce fichier ne peut pas tre utilis comme manuel Il serait incompr hensible Manuel ps gz le manuel de G n Syst Install sh le script d installation INSTALL txt un manuel d installation identique cette section du manuel 4 Votre variable CLASSPATH doit acc der au r pertoire des classes de G n Syst GeneSyst Class Pour cela ajoutez la s quence suivante dans votre fichier login ou quivalent la suite de la s quence pour la d tection des classes de la BoB en csh setenv CLASSPATH CLASSPATH BOBPATH GeneSyst Class setenv CLASSPATH CLASSPATH BOBPATH GeneSyst Class GUI setenv CLASSPATH CLASSPATH BOBPATH GeneSyst Class Grappa en bash CLASSPATH CLASSPATH BOBPATH GeneSyst Class CLASSPATH CLASSPATH BOBPATH GeneSyst Class GUI CLASSPATH CLASSPATH BOBPATH GeneSyst Class Grappa export CLASSPATH 5 Lancez le script d installation install sh Attention Vous devez lancer ce script depuis l int rieur du dossier GeneSyst et taper la commande bin sh install sh Suivez les consignes qui apparaissent alors l cran Ce script ne fait que g n rer et compiler le fichier GeneSyst Class ConfigurationGeneSyst java Celui ci contient quelques variables de configuration de G n Syst Donc en cas de probl me d utilisation du
24. e dossier de travail ni le projet ni le fichier de trace ne sont effac s A la fin du calcul d un syst me de transitions tiquet es G n Syst g n re un ou deux dossiers suivant que l on ait ou non demander tudier un raffinement Ces dossiers sont nomm s Resultats mch pour les informations concernant la machine et Resultats ref pour celles du raffinement Ces dossiers contiennent tous les fichiers de sortie permettant la visualisation du sys t me de transitions tiquet es Le fichier au format dot qui est le fichier g n r par d faut par G n Syst Ce format est textuel et peut tre traduit en un grand nombre de formats vectoriels ou non par l outil GraphViz GN99 de AT amp T De m me qu un fichier au format html g n r aussi par G n Syst la demande de Puti lisateur Ce format n cessite la g n ration du format dot Le format html permet d avoir plus d informations sur le graphe g n r par le dot sans l alourdir pour autant gr ce l utilisation d hyperliens sur une image La g n ration d un tel r sultat entrainera aussi la g n ration d une image gif repr sentant l automate et de trois dossiers Clusters Etats et Transitions qui contiennent les pages html de description des diff rentes transitions Ces sont ces pages qui sont appel es lorsque l on clique sur l hyperimage de la repr sentation html Le fichier au format gzl si celui ci est
25. e l oracle non Nom du projet CalculTransitionsTmpxxx7 Nom du Dossier de calcul CalculDesTransitionsO Nom du fichier de traces de l atelier TraceGenesyst log Nom du fichier d oracle machine lire Nom du fichier d oracle raffinement a lire Force des preuves 21 Ne faire que g n rer les OPs non Effacer le dossier de travail la fin oui Conserver un processus de l AtelierB en parall le non Thttp www graphviz org 2http www inrialpes fr vasy cadp 21 Symbole de condition r ductible true Symbole de condition non r ductible true G Formats de sortie demand s Dot Html Lis ss SES SSSR SSI EE Si un oracle est utilis alors les information qui y sont contenues sont affich es Bien s r seule les informations contenant un r sultat de preuve sont prises en compte Ainsi une r gle contenant une information de preuve sera ignor e Pour plus d information sur la syntaxe d un oracle r f rez vous la section 5 3 3 Voici un exemple de trace de chargement d oracle Chargement de l oracle CalculDesTransitions IndexMachinesAbstr Oracle AssocNumEtat Etat 0 Etat 0 AssocNumEtat Etat 1 Etat 1 AssocNumEv Ev 0 Prendre_Monnaie AssocNumEv Ev 1 Servir_Cafe Tnit 0 F Init 1 T Dec1 0 0 T Dec1 0 1 F Decl 1 0 F Decl 1 1 F Att 0 0
26. ela il y a deux possibilit s Soi les deux sont calcul s dans la m me session de G n Syst soi un Oracle est donn pour l abstraction Tout cela sera d crit plus en d tail en section 5 3 2 2 1 Recherche des tats L outil va chercher associer les diff rents tats raffin s au tats abstraits Notons en passant que la syntaxe de d finition des tats du raffinement n est pas la m me que celle de l abstraction En effet il faut que l utilisateur indique l association des diff rents tats Raffin avec les tats abstraits Par exemple l assertion suivante indique que l tat Feu Vert est d compos en Feu Vert ParkingVide true et Feu Vert A ParkingVide false et que les 2 autres tats sont rest s inchang s ASSERTIONS Feu Vert amp Feu Vert ParkingVide true V Feu Vert A ParkingVide false N Feu Rouge amp Feu Rouge A Feu Orange lt Feu Orange La syntaxe attendue pour l assertion d crivant les tats d un raffinement est donc une conjonc tion d quivalences En outre le membre de gauche de chacune d entre elle doit tre le pr dicat d un tat abstrait et le membre de droite une disjonction de pr dicats d crivant des tats du raffinement Le raffinement d crit dans cet exemple a donc 4 tats Feu Rouge Feu Vert A ParkingVide true Feu Vert A ParkingVide false et Feu Orange Remarque Attention la priorit
27. er les preuves D o le nom d oracle qui leur est donn Les oracles seront d taill la section 5 3 De m me un nouveau projet est cr dans l AtelierB lors de chacune des g n rations de syst mes de transitions tiquet es Ces projets se nomment CalculTransitions Tmpzzx avec un ventuel suffixe num rique Enfin un fichier tra ant l utilisation de l AtelierB est cr dans le dossier courant Celui ci peut tre assez volumineux et doit donc tre effac si l outil ne l a pas fait Ce fichier se nomme par d faut TraceGenesyst log Contrairement aux noms de dossier et projet lors de l ex cution de G n Syst si un fichier portant ce nom est d j pr sent alors il est effac et remplac par celui ci Par d faut le projet le dossier de calcul et le fichier de traces sont effac s la fin de l ex cution du programme si tout s est bien pass et un fichier d automate est g n r dans le sous dossier Resultat mch ou Resultat ref pour le cas d un raffinement du dossier courant Les exceptions notables sont les suivantes si l option N est mise false alors le dossier de travail et le fichier de trace ne sont pas effac s mais le projet est effac si l option G est mise true alors le dossier de travail n est pas effac mais le projet et le fichier de trace sont effac s 20 si l outil est arr t au milieu de son travail par ctrl c par exemple alors ni l
28. est g n r dans le dossier de travail Ainsi pour le r cup rer il faut interdire G n Syst d effacer ce dossier L op tion n false est donc indispensable Le fichier d Oracle porte par d faut le nom IndexMachine sAbstr Oracle ou IndexMachinesRaff Oracle suivant que le syst me tudi sois une abstraction ou un raffinement Obtention d un Oracle vide L obtention d un Oracle vide se fait gr ce l option G true Il n est pas n cessaire de pr ciser n false avec celle ci car le dossier ne sera pas effacer la fin de la g n ration Avec l option G true G n Syst ne va que g n rer toutes les obligations de preuves possible et un Oracle vide Celui ci n aura alors d int r t que s il est ensuite dit manuellement cf 5 3 3 5 3 2 Utilisation d un Oracle Mettons nous dans le cas o nous avons un syst me B et un Oracle partiel ou total de son syst me de transitions tiquet es Cet Oracle peut avoir t g n r automatiquement ou manuel lement cela est indiff rent Si notre syst me est une machine abstraite nomm e MaMachine mch alors l appel de l outil pour g n rer son syst me de transitions tiquet es d crit par l Oracle In dezMachinesAbstr Oracle est le suivant java geneSyst MaMachine mch OM IndexMachinesAbstr Oracle L option 0M indique que le param tre suivant est le nom de l Oracle utiliser pour la g n ration du syst me de transitions tiquet es de la mach
29. eu Vert Feu Rouge Feu Orange ASSERTIONS Feu Vert V Feu Rouge V Feu Orange Les variables qui ne sont pas pr cis es dans un tat peuvent y prendre toutes les valeurs auto ris es par l invariant Ensuite on recherche les tats initiaux C est dire que pour chaque tat E on va chercher v rifier successivement les deux obligations de preuve suivantes 1 Imat E 2 Hnit E Remarque Si la premi re OP est v rifi e alors la seconde n est pas calcul e Remarque La m thode de v rification d une obligation de preuve sera d crite dans la section 7 Si 1 est v rifi e alors nous consid rons que toutes les valuations possibles de l tat E sont initiales Sinon si 2 est v rifi e alors nous consid rons qu aucune des valuations possibles de l tat E n est initiale Enfin si ni 1 ni 2 ne sont v rifi es alors nous consid rons que seules certaines valuations de l tat E sont initiales Ensuite nous construisons l ensemble des tats atteignables Cette construction est r alis e de mani re inductive sur les tats atteignables et s arr te lorsqu il n y a plus de nouvel tat atteint Au d part seuls les tats initiaux sont atteignables Cette construction n cessite de calculer pour chaque tat l ensemble des transitions qui en partent En effet L ensemble des tats atteignables depuis un tat est l ensemble des tats atteignables depuis par au moins une trans
30. hamp n cessaire pour lancer ce mode Ensuite vous verrez appara tre une fen tre Fig 4 4 constitu e de deux onglets Projets qui permet le nettoyage des projets qui ont t cr s dans l AtelierB par G n Syst par l utilisateur courant Ces projets sont nomm s par d faut Calcul TransitionsTmpxxx nom peut tre suivi d un suffixe num rique Les projets vous seront list s il vous suffit de choisir ceux que vous d sirez supprimer en 17 v A O OAP O P Generation en cours LEE 1 15 RETOUR VISUALISER T zy T youre Sorry TA he ee Hemmspesemmesemsmenens H ff acquiter 1 Sans Cond 0 Sans Cond if ff traiter 2 Sans Cond 1 Avec Cond Z traiter 2 Sans Cond 2 Avec Cond 17 ff 44 Liste des tats initiaux ff 0 ff Correspondance num ro d tat lt gt Assertion ff D Ack TRUE ff 1 Ack FALSE amp 77 EltsAEnvoyer D ff 2 Ack FALSE amp EltsAEnvoyer gt D ff G n ration du fichier Resultats mch Canal_ Communication V2 G n ration du fichier Resultats mch index html Ok Effacement du projet dans l atelierB Ok Effacement du fichier de trace
31. i le rentrer au clavier Celui ci doit tre un oracle pour les obligations de preuve de la machine Oracle Raffinement 15 Ce champ doit contenir le nom d un fichier Pour entrer le nom du fichier vous pouvez parcourir votre r pertoire mais aussi le rentrer au clavier Celui ci doit tre un oracle pour les obligations de preuve du raffinement Force Vous devez choisir dans la liste d roulante un entier entre 0 et 3 Il d signe le niveau de force de preuve employer dans l AtelierB lors de la r solution des obligations de preuve Affichage Minimum Vous devez cocher la case ou pas Cela permet de minimiser l affichage en ne d taillant pas chaque op ration effectu e Nettoyer Vous devez cocher la case ou pas Cela permet de dire l outil de laisser les fichiers de travail en place la fin de la g n ration Que G n rer Vous devez cocher la case ou Si la case est coch e aucune preuve ne sera effectu e et toutes les machines contenant les obligations de preuve seront g n r es De plus le dossier de travail ne sera pas effacer V rifier Oracle Vous devez cocher la case ou pas Si la case est coch e et qu un oracle est pass en param tre alors l oracle sera utilis pour diriger les obligations de preuves g n r es afin de les minimiser AtelierBenParallele Vous devez cocher la case ou pas Si la case est coch e alors un processus de l AtelierB sera conserver en m moire
32. ine abstraite On pourra ainsi demander de g n rer le syst me de transitions tiquet es d une machine et de son raffinement avec soi un Oracle pour ne simplifier que la g n ration du syst me de transitions tiquet es de la machine java geneSyst MaMachine mch OM IndexMachinesAbstr Qracle R MonRaffinement ref Soi un Oracle pour ne simplifier que la g n ration du syst me de transitions tiquet es du raffinement java geneSyst MaMachine mch OR IndexMachinesRaff Qracle R MonRaffinement ref Soi un Oracle pour simplifier la g n ration du syst me de transitions tiquet es de la machine et un Oracle pour diriger la g n ration du syst me de transitions tiquet es du raffinement java geneSyst MaMachine mch OM IndexMachinesAbstr racle OR IndexMachinesRaff Qracle R MonRaffinement ref Enfin dans tous les cas si l on veut juste que l Oracle serve diriger la g n ration des obligations de preuve on rajoute l option V TRUE Tous les oracles pass s en param tre seront donc v rifi s par preuve Exemple java geneSyst MaMachine mch OM IndexMachinesAbstr Qracle OR IndexMachinesRaff Uracle R MonRaffinement ref V TRUE 26 5 3 3 Edition d un Oracle Un Oracle est un fichier texte ayant une syntaxe particuli re Concr tement chaque ligne contient 0 ou 1 instruction Un commentaire commence par et se termine sur la fin de la ligne Il existe 6 instructions diff rentes 1 AssocNumEtat Etat int E
33. isation de l AtelierB les fichiers prouver etc Les dossiers en question portent le nom CalculDes Transitions Celui ci peut tre suivi d un suffixe num rique 3 3 D faut Si ni le param tre n ni le nom d une machine n est trouv la suite de l appel de la classe java java geneSyst alors le message d aide suivant est affich M thode d appel java ganaSyst N Nettoyer Argument unique lt nomSystemeAbstrait gt R Raffinement lt nomRaffinement gt C F Force 1011121331 E OPExistentielles TRUE FALSE MIAffichageMinimum TRUE FALSE 0M OracleMachine lt nomFichierOracle gt OR OracleRaffinement lt nomFichierOracle gt V VerifierOracle TRUE FALSE N Nettoyer TRUE FALSE ABP AtelierBenParallele TRUE FALSE G QueGenerer0P TRUE FALSE D SymboleD faut 33 255 P SymboleProuv 33 255 I SymboleNonProuve 33 255 DOT TRUE FALSE GXL TRUE FALSE C HTML TRUE FALSE DEBUG TRUE FALSE Exemple java geneSyst DISTRI mch R DISTRI ref M true Information 33 255 est l ensemble des caract res visibles tous sauf espace tabulation retour chariot Si vous passez des symboles reconus par votre SHELL comme tant une commande ex signifie l ensemble des fichiers alors pensez les pr c der d un anti slash ex au lieu de 14 Interface graphique Il est d sormai
34. ition La recherche de la d clenchabilit et de l atteignabilit donne lieu au calcul des conditions D pv condition de d clenchabilit et pv r condition d atteignabilit qui forment la garde de chacune des transitions Les obligations de preuves g n r es sont alors les suivantes Obligations de preuve Valeur des conditions E Garde Ev Dig Ev true Vx E gt Garde Ev D F Fv false 1 V 2 De nv Garde Ev E A Garde Ev Action Ev F true E A Garde Ev Action Ev F false 4 v 5 Comme pour l initialisation 2 ne sera g n r e et soumise au prouveur que si 1 n est pas v rifi e Et l OP 3 ne sera pas calcul e car elle est la cons quence logique de la n gation de 1 et 2 De m me pour 4 5 et 6 A E gv r Action Ev F Remarque est tout de m me possible de demander G n Syst de g n rer et v rifier aussi les OP 3 et 6 Il est ainsi possible d avoir 4 tat pour une condition Toujours vraie gard e impossible ou inconnue De mani re informelle on peut d crire ces deux conditions de la mani re suivante D clenchabilit d un v nement Ev depuis un tat C est le pr dicat d crivant le sous tat de permettant le d clenchement de Ev Atteignabilit d un tat E gt par un v nement Ev depuis un tat C est le pr dicat d crivant celles des va
35. l est celui d j implant pour l abstraction et ne sera donc pas red crit Cepen dant certaines simplifications y sont faites Tout d abord le calcul de recherche des tats initiaux ne sera effectu que sur les sous tats des tats initiaux de l abstraction Enfin pour un v nement d j existant dans l abstraction son raffinement ne sera pas calcul sur tous les tats mais seule ment au niveau des tats qu il relie dans l abstraction Cela simplifie les calculs de sa d clenchabilit aussi bien que de son atteignabilit 11 Appels de G n Syst en ligne de commande On peut faire la distinction entre deux modes d utilisations de l outil Pour g n rer des STE ou pour effacer tous les fichiers temporaires qui ont t laiss s dans le dossier courant sur demande ou par arr t inopin de G n Syst 3 1 Mode G n ration de syst me de transitions tiquet es Pour entrer dans ce mode seul un param tre est obligatoire le nom du fichier contenant une machine B dont les op rations n ont pas de pr conditions mais des gardes L appel est donc le suivant java geneSyst MaMachine mch A la suite du nom de la machine on peut rajouter des param tre optionnels dont voici la liste R ou Raffinement Ce flag doit tre suivi d un nom de fichier Celui ci doit contenir un raffinement de la machine F ou Force 1 par d faut Ce flag doit tre suivi d un entier entre O et 3 Il d
36. lculDesTransitions4 C CalculDesTransitionsS SUPPRIMER RETOUR Figure 4 4 Exemple de fen tre permettant le nettoyage par G n Syst 19 Sorties et traces de G n Syst 5 1 Mode G n ration de syst me de transitions tiquet es 5 1 1 Fichiers g n r s Pour g n rer un automate G n Syst doit effectuer un certain nombre d obligations de preuve qui sont produites sous forme de machines et qui sont prouv es pour l instant via l AtelierB Ce dernier point n cessite notamment la pr sence d un dossier BDP et d un dossier LANG C est pourquoi l outil commence par cr er un r pertoire de travail dans lequel il produira par la suite les fichiers et dossiers n cessaire son bon fonctionnement Le dossier de travail produit se nommera par d faut CalculDes Transitions Ce choix est configurable lors de l installation Il se peut que ce nom soit suivi d un suffixe num rique afin d viter tout conflit avec un dossier d j existant Parmi les fichiers pr sents dans ce dossier se trouve le fichier IndexMachinesAbstr Oracle et possiblement le fichier IndexMachinesRaff Oracle Ces deux fichiers sont la version textuelle et ditable du format interm diaire utilis en interne pour repr sent le syst me de transitions tiquet es g n r Ainsi Ces fichiers peuvent tre remis en entr e de l outil avec les options 0M et OR afin de simplifi
37. leurs de la d clenchabilit permettant de mener E gt Autrement dit ce pr dicat d crit l ensemble des valeurs de l tat qui permettent le d clenchement de Ev et qui m ne E Cependant pour des raison de simplification des preuves la description de ce dernier pr dicat se fait sous hypoth se de l tat et de la d clenchabilit Il en r sulte que l atteignabilit n implique pas la d clenchabilit mais que la conjonction des deux forme la garde classique qui orne les automates symboliques la disjonction des conditions d atteignabilit sur chaque transition d un v nement Ev sur un tat est quivalente true la condition de d clenchabilit est la m me sur chaque transition d un v nement Ev sur un tat E Notons cependant que le calcul de l atteignabilit d un v nement vers les diff rents tats se fait de la mani re suivante On cherche d abord prouver qu aucun tat n est atteignable S il n y a qu un tat atteignable alors l atteignabilit de la transition qui y m ne est forc ment toujours vraie Implicitement il est normal que si un v nement peut se d clench il puisse all quelque part 2 2 Cas d un raffinement La g n ration d un syst me de transitions tiquet es pour un raffinement ne peut tre calcul actuellement que si le syst me de transitions tiquet es de son abstraction est d j charg en m moire Pour c
38. nement non d clenchable dans l tat 0 Statut Ev nement non d clenchable dans l tat 1 Une fois le calcul de toutes les transitions r alis l ensemble des transitions est r sum dans un tableau textuel qui est affich a la suite des traces d ex cution L exemple ci dessous r sume les transitions trouv es dans l exemple pr c dant De plus les tats initiaux sont rappel s et la concordance entre les num ros d tat et les pr dicats est indiqu e Ainsi ce seul r sultat suffit construire enti rement un syst me de transitions tiquet es Ce sont d ailleurs ces informations qui sont stock es dans le fichier d oracle tant le format interm diaire de sortie g n r Re see none Op ration ff 2 gt gt gt ZA Prendre Monnaie 0 Sans Cond 0 Sans Cond _ 1 Liste des tats initiaux 11 O Correspondance num ro d tat lt gt Assertion O Etat 0 1 Etat 1 Dans le cas d un raffinement seul le calcul de recherche des quivalences d tats est ajout au d but des calculs Dans l exemple qui suit nous consid rons que les tats de la sp cification ont t d finis par l assertion Etat 0 V Etat 1 et les tats du raffinement par Etat 1 Etat 1 A feu rouge V Etat 1 A feu vert Etat 0 Etat 0
39. ni re version de G n Syst est disponible en libre t l chargement l adresse suivante http www lsr imag fr Les Personnes Nicolas Stouls Elle est accompagn e d un rapide fichier d aide l installation L installation ne sera donc pas d crite dans ce document car la m thodologie peut avoir chang e entre temps De plus sur cette page se trouve un lien vers la documentation JavaDoc des classes de G n Syst Toutes les demandes d informations compl mentaires ou les probl mes d installation ou autres concernant l outil G n Syst peuvent tre adress es soit Didier Bert didier bert imag fr soit Nicolas Stouls nicolas stouls imag fr 1 application G n Syst est d velopp e sous les termes du contrat de la licence Cecill Celle ci permet de diffuser librement les sources d un programme sans pour autant en perdre la propri t Une copie de ce contrat de licence est disponible 4 la m me adresse que G n Syst 36 Bibliography Abr96a Abr96b Abr96c AM98a AM98b BC00 BP03 BPS05 Bri02 But99 BW96 Cav00 Coo00 GLM02 GM99 J R Abrial Extending B without Changing it for Developping Distributed Systems In H Habrias editor Proceedings of the 1st Conference on the B method 1996 ISBN 2 906082 25 2 J R Abrial Extending B Without Changing it In Nantes H Habrias editor First B conference 1996 J R Abrial The B Book Cambridge University Pres
40. ons de preuves dont nous parlions jusqu main tenant avaient en hypoth ses implicites la pr sence de ces clauses Voici un exemple tir de la sp cification de la machine caf d crite en section 6 1 Cet exemple est l obligation de preuve g n r e pour prouver la d clenchabilit de l v nement mettre_en_ marche depuis l tat etm arret MACHINE DISTRI SETS BOISSONS rien cafe the choc PIECES demiF unF deuxF cingF ETM arret pret select distri tropp remb CONSTANTS prix valeur PROPERTIES prix BOISSONS NAT A valeur PIECES A prix rien A prix cafe 300 A pria the 200 A prix choc 250 A valeur demiF 50 A valeur unF 100 A valeur deuxF 200 A valeur cingF 500 VARIABLES boisson somme af fichage etm INVARIANT boisson BOISSONS A somme 0 max ran prix max ran valeur A 34 af fichage prix boisson somme etm ETM ASSERTIONS L v nement 0 n est il jamais d clenchable depuis l tat 0 Etat1 0 Etat2 1 transition n 0 etm arret gt not etm arret INITIALISATION boisson somme af fichage etm rien 0 0 arret OPERATIONS mettre marche skip arreter _ machine skip selectionner _ boisson skip mettre_ piece skip distribuer skip yy rendre_monnaie_1 skip prendre __ gobelet skip annuler skip zz rendre monnaie 2 skip END 35 Bilan Actuellement la der
41. rm for the formal B method In PPPJ 02 pages 137 140 Trinity College Dublin Ireland Juin 2002 38
42. s Ok E Effacement du dossier de travail Ok Fin de la g n ration des syst mes de transitions il gt Figure 4 2 Exemple de trace d utilisation de G n Syst cochant les cases correspondantes Dossiers qui permet le nettoyage des dossiers qui servent stocker toutes les informations temporaires pendant le calcul R pertoires pour l utilisation de l AtelierB les fichiers prou ver etc Les dossiers en question se nomment CalculDes Transitions Ce nom peut tre suivi d un suffixe num rique Les dossiers vous seront list s il vous suffit de choisir ceux que vous d sirez supprimer en cochant les cases correspondantes Remarque Lorsque aucuns projets ni dossiers n ont t trouv s un message vous serra fournit La fen tre de nettoyage va appara tre mais les boutons de suppressions sont d sactiv s 18 iv Systeme de transition etiquete produit Bog envoyer G traiter acquiter ACk FALSE amp EltsAEnvoyer gt 0 G traiter FALSE amp Figure 4 3 Exemple de visualisation produite par Grappa sous G n Syst iv Mode nettoyage e Projets Dossiers Nettoyage des dossiers existants Tout cocher CalculDesTransitions CalculDesTransitions0 R CalculDesTransitions1 v CalculDesTransitions2 CalculDesTransitions3 _ Ca
43. s 1996 J R Abrial and L Mussat Introducing Dynamic Constraints in B In D Bert editor B 98 The 2nd International B Conference Recent Advances in the Development and Use of the B Method volume 1345 of LNCS Springer Verlag 1998 J R Abrial and L Mussat Introducing Dynamic Constraints in B In D Bert editor Proceedings of the Second International B Conference volume 1393 of LNCS Springer Verlag 1998 D Bert and F Cave Construction of Finite Labelled Transition Systems from B Abs tract Systems In Integrated Formal Methods volume 1945 of LNCS Springer Verlag 2000 D Bert and M L Potet Sp cification B Support de cours de l ENSIMAG et du DEA ISC 2003 Institut National Polytechnique de Grenoble D Bert M L Potet and N Stouls Genesyst a tool to reason about behavioral aspects of b event specifications application to security properties In ZB 2005 For mal Specification and Development in Z and B volume 3455 of LNCS pages 299 318 Springer Verlag 2005 Alexandre Brillant Introduction UML 2002 Michael Butler Fm 99 World congress on formal methods In An Overview of Event Based B Septembre 1999 M Butler and M Wald n Distributed System Development in B In H Habrias editor Proceedings of the 1st Conference on the B method 1996 ISBN 2 906082 25 2 Francis Cave Passage du B syst me aux syts mes de transitions tiquet s finis Rapport de DEA Institut National Poly
44. s possible de faire appel au deux modes d utilisation de G n Syst au travers de l interface graphique r alis e par Hounayda MOHAMED durant l t 2004 Celle ci permet de r aliser les m me actions que la ligne de commande mais de mani re plus agr able Pour lancer l interface graphique il suffit de taper la commande java AppliGene 4 1 Mode G n ration de syst mes de transitions tiquet es 4 1 1 Lancement de G n Syst Pour entrer dans ce mode il est obligatoire de remplir le champ Machine Ce champ doit contenir le nom d un fichier repr sentant une machine B dont les op rations n ont pas de pr conditions mais des gardes MaMachine mch Pour entrer le nom du fichier vous pouvez parcourir votre r pertoire mais aussi le rentrer au clavier de pr ciser le s format s attendu s en sortie dans la liste Formats de sortie Il suffit de cocher sur la case correspondant au x format s souhait s DOT HTML ou GXL Ensuite il ne vous reste qu ex cuter G n Syst avec le bouton Lancer D autres options peuvent tre pr cis s Raffinement Ce champ doit contenir le nom d un fichier Pour entrer le nom du fichier vous pouvez parcourir votre r pertoire mais aussi le rentrer au clavier Celui ci doit tre un raffinement de la machine Oracle Machine Ce champ doit contenir le nom d un fichier Pour entrer le nom du fichier vous pouvez parcourir votre r pertoire mais auss
45. sation de syst mes en B Proposition de guides m thodologiques pour la d composition d v nements Rapport de DEA Institut National Polytechnique de Grenoble France 2000 Pierre Alain Muller and Nathalie Gaertner Mod lisation objet avec UML ISBN 2 212 09122 2 Code diteur G09122 Editions Eyrolles 2002 Xavier Morselli Marie Laure Potet and Nicolas Stouls G n syst G n ration d un syst me de transitions tiquet es partir d une sp cification B v nementiel In AFADL 2004 pages 317 320 June 2004 J Nahoum Outils d assistance 4 la construction de syst mes dans la m thode B Rap port de DEA Institut National Polytechnique de Grenoble France 2001 OMG Unified Modeling Language Specification septembre 2001 Version 1 4 C Oriat Invocation de m thodes en Java 2000 Polycopi ENSIMAG C Oriat Quelques l ments de Java 2000 Polycopi ENSIMAG Marie Laure Potet B Systeme Etude de cas Parking 2000 Institut National Polytech nique de Grenoble Transparents de cours Marie Laure Potet Introduction au B v nementiel Ev nement Raffinement D com position 2000 Institut National Polytechnique de Grenoble Transparents de cours M L Potet and N Stouls Explicitation du contr le de d veloppement _ v nementiel In AFADL 2004 pages 13 27 June 2004 SUN Java Virtual Specification Mai 2000 J C Voisinet B Tatibouet and A Hammad jBTools An experimental platfo
46. script vous pouvez le relancer autant de fois que vous voulez ou m me le contourner et diter manuellement le fichier 6 Pour la version UNIX avec GraphViz uniguement Votre variable PATH doit acc der au r pertoire des binaires ex cutables de GraphViz Pour cela ajoutez la s quence suivante dans votre fichier login ou quivalent set path BOBPATH GeneSyst GraphViz bin path setenv MANPATH MANPATH BOBPATH GeneSyst GraphViz man Pour toute demande d informations compl mentaires s adresser Nicolas Stouls imag fr ou aller sur la page http www lsr imag fr Les Personnes Nicolas Stouls Algorithmes implant s Les fondements th oriques de G n Syst ne sont pas abord s dans ce manuel En revanche ils sont d taill s dans PS04 BPS05 Dans ce chapitre nous allons simplement d crire bri vement l organisation des calculs effectu s permettant l obtention d un syst me de transitions tiquet es 2 1 Cas d une sp cification abstraite Une fois la description du syst me charg e en m moire par la jBTools l ensemble des tats est charg partir de la clause assertion du syst me En effet l utilisateur doit pr ciser dans l assertion les tats qu ils souhaite voir appara tre sur l automate Ces tats doivent alors tre d crits sous la forme d une disjonction des diff rents pr dicats d finissant chacun des tats Voici un exemple concret d finissant les trois tats F
47. technique de Grenoble France 2000 K M L Cooper Statecharts Document de cours Universit de Dallas Texas 2000 H Garavel F Lang and R Mateescu An overview of CADP 2001 EASST Newsletter 4 13 24 2002 Hubert Garavel and Radu Mateescu Mod lisation d un syst me d entr es sorties scsi 2 v3 0 Technical report action VERDON 1999 37 GMS01 GN99 Ham02 Har87 HM01 Leb00 MG02 MPS04 Nah01 OMG01 Ori00a Ori00b Pot00a Pot00b PS04 5177400 2 Garavel R Mateescu and Smarandache Parallel state space construction for model checking In Proceedings of the 8th international SPIN workshop on Model che cking of software Series Proceeding Article pp 217 234 Springer Verlag New York 2001 E R Gannsner and S C North An open graph visualization system and its applications to software engineering Technical report Laboratoires AT amp T Etats unis 26 mai 1999 Smaine Hamdane G n ration de syst mes de transition tiquet s partir de la des cription d un syst me d v nements d crits avec le langage B Rapport de ma trise Universit Joseph Fourrier Grenoble 1 France mai 2002 David Harel Statecharts visual formalism for complex systems Science of Computer Programming 8 3 231 274 1987 P H Hartel and L Moreau Formalising the Safty of Java the Virtual Machine and JavaCard 25 mars 2001 J Lebray Mod li
48. u apparait T Tous les effacer L Lister chaque projet et demander s il faut l effacer P n effacer aucun projet et nettoyer les Dossiers Q Quitter le programme sans toucher aux projets Si l on choisit Quitter alors on sort du programme sans avoir touch rien Si l on choisit de Passer alors les projets resteront intouch s et l on passera la suite Si l on choisit la premi re option alors tous les projet list s ci dessus seront effac sans plus poser de question Si l on choisit de lister chaque projet alors le contenu de chacun d eux sera affich et tour de r le on vous demandera Projet CalculTransitionsTmpxxx Voulez vous effacer ce projet 0 24 Deux r ponses sont alors possibles O si l on veut effacer le projet et N si l on ne veut pas effacer le projet Mais dans la plupart des cas le projet sera vide Une fois cette premi re partie termin e un deuxi me menu appara t pr c d du nom des dossiers ayant put tre g n r s par le programme Dossiers trouv s CalculDesTransitions CalculDesTransitions0 CalculDesTransitions13215 T Tous les effacer L Lister chaque dossier et demander s il faut l effacer Q Quitter le programme sans rien toucher Cette fois ci encore Quitter permet de quitter le programme sans toucher aux dossiers trouv s Cependant les projets qui auront t effac s pr c demment ne seront pas pour autant r cup r s
49. un bool en true false S il vaut true alors le r sultat produit sera g n r notamment dans le format HTML Attention il est quand m me noter que la g n ration au format HTML n est possible que gr ce l utilisation de l outil GraphViz de At amp T et en passant par le format DOT Sont utilisation n cessite donc que le format DOT soit aussi s lectionn GXL False par d faut Ce flag doit tre suivi d un bool en true false S il vaut true alors le r sultat produit sera g n r notamment dans le format GXL Exemple d utilisation java geneSyst MaMachine mch R MonRaff ref m false f 1 n false html TRUE Remarque L ordre dans lequel les param tres sont donn s est totalement indiff rent sauf pour un l ment le premier param tre doit tre soi le nom de la machine traiter soi le param tre n 13 3 2 Mode nettoyage Ce mode sert effacer automatiquement les diff rentes polutions qui ont pu tre g n r es par l outil Pour acc der ce mode il faut lancer l outil de la mani re suivante java geneSyst n Les l ments qui seront alors effac s sont Les projets qui ont t cr s dans l AtelierB par G n Syst par l utilisateur courant Ces projets sont nomm s CalculTransitions Ce nom peut tre suivi d un suffixe num rique Les dossiers qui servent stocker toutes les informations temporaires pendant le calcul R pertoires pour l util
50. un syst me B v nementiel Abr96c Abr96b AM98b Abr96a AM98a BP03 But99 BW96 Sp cification ou raffinement Pour cela il se base sur un parseur B le jBTools V TH02 qui lui sert charger les syst mes en m moire et sur une biblioth que de manipulation des structures B la qui lui permet de Thttp www cecill info http www research att com john Grappa 3http www graphviz org 4www lsr imag fr B Documents CNAM 2002 06 13 Resumes Bert pdf g n rer des obligations de preuve Ensuite ces derni res sont donn e au prouveur automatique de l AtelierB d velopp par 1 Le r sultat de G n Syst est un automate d cor Celui ci peut l heure actuelle tre produit sous trois formes diff rentes au format DOT support par l outil GraphViz GN99 de AT amp T au format HTML produit en utilisant les fonctionnalit s de GraphViz au format GXL Graph eXchange Language bas sur le XML et reconnu par de nombreux outils Format non encore test Historiquement le premier format a avoir t support tait le BCG Mais l impossibilit de pouvoir repr senter des automates hi rarchiques ou d tiqueter les tats avec des pr dicats nous a pouss ne plus supporter ce format Cet outil est bas sur les tudes pr alables de D Bert et F Cave BC00 Cav00 S Hamdane Ham02 et N Stouls et M L Potet PS04 MPS04 505 Enfin son fonctionnement
Download Pdf Manuals
Related Search