Protocoles d`utilisation de composants
Contents
1. Protocoles d utilisation de composants Sp cification et analyse en Kmelia Pascal Andr Gilles Ardourel Christian Attiogb LINA FRE CNRS 2729 2 rue de la Houssini re BP 92208 F 44322 Nantes Cedex 3 Pascal Andre Gilles Ardourel Christian Attiogbe univ nantes fr R SUM L approche des composants logiciels constitue une solution pour d velopper des logi ciels de fa on modulaire et en r utilisant l existant Cependant ce n est pas facile de trouver des composants appropri s un besoin sp cifique et pouvoir se servir convenablement des services offerts Nous proposons de r pondre la fois la probl matique de la description de mode d emploi pour les composants et celle de l expression de contraintes d utilisation par la sp cification de multiples modes d emploi qui peuvent tre utilis s comme des services quel conques Pour s assurer que les protocoles sont exempts d anomalies nous avons labor une technique d analyse de leur coh rence Notre tude et les exp rimentations sont faites sur la base du mod le composants Kmelia ABSTRACT The Component Based Engineering is an approach for developing software in a mod ular way by reusing existing software pieces However finding software components that fit a specific requirement and using correctly the provided services are quite difficult tasks In this paper we propose to answer both the issues of expressing a component s use2. tre exempt d anomalies Dans un article pr c dent Attiogb et al 2006 nous avons nonc des propri t s attendues pour les composants et les services relatives notamment la s ret et la vi vacit Afin d exp rimenter nos propositions et offrir terme des outils d aide aux d veloppeurs de composants nous avons entrepris le d veloppement d une plate forme pour l tude des composants COST La prise en compte de protocoles ne doit pas perturber le contr le du bon d roulement des interactions entre composants Le bon d roulement d une interaction part de l hypoth se du respect des r gles contractuelles entre service appelant et protocoles ou services appel s Un composant qui offre des services s engage fournir des protocoles coh rents servant de modes d emploi des services offerts Nous nous concentrons ici sur les v rifications et les r gles de concep tion li es aux protocoles 4 1 V rifications de protocoles en tant que services Dans la mesure o un protocole est un service offert nous pouvons le soumettre aux m mes v rifications que n importe quel autre service offert Nous exploitons pour 2 lina atlanstic net fr equipes team10 Kmelia 30 LMO 2007 cela des r sultats pr c dents Attiogb et al 2006 du point de vue de chaque com posant sont v rifi es la syntaxe et la coh rence des interfaces de services avec leur comportement du point de vue des assemblages son
3. expression de services complexes et leur composition Les services appelables au sein d un autre service sont nomm s sous services et sont d clar s dans l interface du service La composition verticale de services repose sur l ajout de points d expansion aux tats ou parmi les actions sur 6 qui permettent d inclure un service dans un autre et qui sont expans s lors des v rifications de compatibilit de services Un appel de sous service au sein d un service est valu dans son contexte Diff rents types de points d expansion peuvent tre utilis s selon que l on d sire un appel obligatoire ou optionnel de service ou de comportement La syntaxe est donn e dans le tableau 2 Point d expansion Tableau 2 Syntaxe Kmelia des points d expansion Les points d expansion de comportement se distinguent des points d expansion de service par la possibilit d atteindre le comportement d un service sans passer par l appel du service une pseudo transition qui court circuite le d but de service est no tamment ajout e Les points d expansion de comportements ne peuvent s appliquer qu aux services sans param tres d entr e ni de sortie qui ne transmettent donc d in formation que par leurs messages moins de proposer une adaptation de service Andr et al 2006a La figure illustre les concepts pr c dents dans le cas d un guichet automatique bancaire GAB Il s agit ici d une repr sent
4. Enfin il y a des risques de confusion li s au fait que les contraintes soient implicites cach es dans les descriptions des services et non explicites Pour toutes ces raisons il est n cessaire de d finir des r gles d usage et d encha nement de services du composant de mani re explicite dans l interface m me du composant Nous proposons de le faire au travers de protocoles 2 2 Divers usages de la notion de protocole La notion de protocole dans les mod les composants n est pas nouvelle mais sa d finition ou son utilisation varie d un mod le langage l autre Pour clarifier le concept nous proposons une br ve a ll entre les approches en retenant quatre crit res Le contenu des protocoles invocations de services calculs envois de messages structures de contr le conditionnnelles r p titives L unit de rattachement des protocoles le composant l interface le service le connecteur ou l architecture Le formalisme de description de la dynamique des protocoles automates ma chines tats expressions r guli res etc Les techniques de description et de preuve des propri t s des protocoles logique temporelle langage de marques algorithmes etc Cette synth se indique aussi la pr sence d outils de description de v rification des protocoles model checking theorem proving de raffinement ou de g n ration de code Le contenu est relatif aux actions l
5. LMO 2007 Attie P C Lorenz D H Establishing Behavioral Compatibility of Software Components wi thout State Explosion Technical Report n NU CCIS 03 02 College of Computer and In formation Science Northeastern University 2003 Attiogb C Andr P Ardourel G Checking Component Composability Sth International Symposium on Software Composition SC 06 vol 4089 of LNCS Springer p 18 33 2006 Becker S Overhage S Reussner R Classifying Software Component Interoperability Er rors to Support Component Adaption 7th International Symposium CBSE 2004 LNCS Springer p 68 83 2004 Beugnard A J z quel J M Plouzeau N Watkins D Making Components Contract Aware Computer vol 32 n 7 p 38 45 1999 Canal C Fuentes L Pimentel E Troya J M Vallecillo A Adding Roles to CORBA Objects IEEE Trans Softw Eng vol 29 n 3 p 242 260 2003 de Alfaro L Henzinger T A Interface automata Proceedings of the 8th European software engineering conference ESEC FSE 9 ACM Press p 109 120 2001 Giannakopoulou D Kramer J Cheung S C Behaviour Analysis of Distributed Systems Using the Tracta Approach ASE vol 6 n 1 p 7 35 1999 Inverardi P Wolf A L Yankelevich D Static checking of system behaviors using derived component assumptions ACM Trans Softw Eng Methodol vol 9 n 3 p 239 272 2000 Medvidovic N Taylor R N A
6. de protocoles est en cours d exp rimenta tion Nous proc dons d une mani re similaire celle de l analyse comportementale savoir par traduction dans des langages adapt s et outill s Pour la v rification de contrat nous exp rimentons avec le langage B Atelier B et le langage Z prouveur Z EVES Les aspects li s la concurrence entre protocoles et services ne sont pas encore trait s 5 Conclusion et perspectives Apr s avoir positionn notre approche des protocoles avec les autres usages cou rants qui en sont faits dans le domaine nous avons pr sent une solution pour d crire des modes d emploi de services de composants sous la forme de protocoles d utilisa tion Cette solution reprend la description des services offerts Kmelia en la sp cialisant et l annote avec la propri t protocole afin d en tirer parti en termes de repr sentation ou d analyse De cette fa on notre mod le de composants n est pas modifi ce qui permet de r utiliser les outils existants dans notre plate forme COSTO pour analyser la compatibilit des protocoles Nous avons donn la s mantique des protocoles dans le mod le de composant Kmelia et montr comment leur description est expans e pour obtenir des services ordinaires Nous avons propos une technique d analyse formelle de la coh rence interne de protocole et des r gles de conception de protocoles Pour pousser plus loin nos analyses de coh rence en l occurre
7. des services Une composition est un assemblage encapsul dans un composant La hi rarchisation des services ainsi que des composants est une des caract ristiques de Kmelia qui permet une bonne lisibilit flexibilit et une bonne tra abilit dans la conception des architectures Cet aspect a t abord dans Andr ef al 2006b La continuit des services est mise en ceuvre par des liens de compositions qui servent a la promotion des services d un composant vers ceux d un composite 3 2 Sp cification de protocoles en Kmelia Pour contr ler les services offerts par les composants Kmelia nous souhaitons in troduire des protocoles d utilisation pour d crire des enchainements licites d appels de services Parmi les services offerts par un composant ceux qui apparaissent dans la description de protocoles sont dits contr l s ceux qui n y figurent pas sont dits libres Ces qualificatifs viennent compl ter ceux qui gouvernent l accessibilit directe des services expos e dans l interface du composant Le mod le permet ainsi l existence de services contr l s par un ou plusieurs protocoles mais n anmoins visibles et appe lables tout moment Un composant peut offrir un ou plusieurs protocoles Certains protocoles d un composant peuvent tre qualifi s d ininterruptibles par le concepteur du composant les appels aux services que contr le le protocole doivent se d rouler donc sans interruption c est d
8. es des vues diff rentes les contrats d utilisation des services indiquant les droits et devoirs du client et du fournisseur les r gles ou protocoles d utilisation des services pr cisant les encha nements licites de services Dans cet article nous nous int ressons plus particuli rement aux r gles d utili sation des services offerts par les composants et leur v rification statique Nous avons tudi les moyens de d finir simplement des modes d emploi des services d un composant ainsi que diff rentes analyses r aliser pour garantir la coh rence des pro tocoles et donc des composants Pour ce travail nous nous appuyons sur le mod le Kmelia dont le noyau a t d crit dans Attiogb ef al 2006 Ce mod le permet de d finir des composants d une mani re abstraite vis vis des mod les op rationnels en se focalisant sur les services et les interfaces l objectif sous jacent tant la v rifi cation statique d assemblage h t rog nes de composants Les principales contributions de ce travail sont i la proposition d une m thode de description des modes d emploi des composants qui reprend la description des services offerts et ii une technique d analyse de la coh rence des protocoles L article est organis de la fa on suivante dans la section P nous exposons nos motivations pour l usage des protocoles et les solutions existantes Nous d taillons l approche des pr
9. protocole g n ralis plusieurs protocoles par composants et un protocole par service pour l illustrer la nuance Avec un mod le composant simple qui autorise une seule inter face par composant un seul protocole et des services r duits des profils d op ration on peut repr senter a des protocoles de services en mod lisant un seul service par composant b plusieurs protocoles ou bien plusieurs interfaces de composants par composition de composants et c diff rents connecteurs par sp cialisation des com Protocoles en Kmelia 23 posants Dans ce cas le concepteur d architectures devra encapsuler les protocoles dans des composants composites g rer la coh rence des interfaces proches des pro bl mes d h ritage en objet et d finir des biblioth ques de composants sp cialis s Il en r sulte donc une certaine lourdeur des mod lisations Autrement dit certains usages favorisent plus la documentation du composant que d autres Par exemple les approches de la cat gorie 1 et une partie de celles de la cat gorie 2 interpr tent le protocole plut t comme une contrainte pour l implantation du composant qu un mode d emploi Le rattachement du protocole un connecteur permet certains mod les de se rapprocher du point de vue de l orchestration de services dans laquelle l enchaf nement de messages a un sens ind pendamment des composants concern s et peut par cons quent tre d crite en dehor
10. 7 retirer msg lire maCarte retirer retirer maCarte lt lt code gt gt f lt lt montant gt gt Xretirer retirer res l code e2 IHM_CLIENTR code ue 00 msg lire monCode el BASEGAB retrait cb CB _code _montant c lt gt cb code amp amp nbe gt 0 msg c cb code rep verifAut verifAut cb id c CALLER dem_code CALLER dem_code c nbe nbe 1 Ni ICEx b code amp amp nbe 0 msg savalerCarte not rep msg estituerCarte Os consultation e3 rep msg m gt cb limit e msg CALLER dem_m IHM_CLIENTR montant a connexion Jdmsg lire m CALLER e6 retrait false CALLER dem m lt cb limit e7 debiter c m restituerCarte e8 CALLER montant m IHM_CLIENTR Figure 1 Extrait du Guichet Automatique Bancaire mod lis dans Kmelia deconnexion CALLERI js eee i BASEGAB Formellement J l interface d un service s d un composant C est sp cifi e par un 5 uplet o P Q Vs Ss o o est la signature P la pr condition d appel Q la postcondition de d roulement V un ensemble de d clarations de variables locales au service et S subs cals reqs ints un quadruplet d ensembles finis et disjoints de noms de services tels que reqs C I et subs resp cals reqs ints est l ensemble des services offerts resp les requis de l appelant les req
11. Classification and Comparison Framework for Software Architecture Description Languages IEEE Transactions on Software Engineering vol 26 n 1 p 70 93 january 2000 Moisan S Ressouche A Rigault J A Behavioral Model of Component Frameworks Techni cal Report n RR 5065 INRIA December 2003 OMG The OMG Unified Modeling Language Specification version 2 0 Rfp Superstructure Specification available at www omg org docs ptc 05 07 04 pdf Infrastructure Specification available at www omg org docs ptc 03 09 15 pdf 2005 Pavel S Noye J Poizat P Royer J C Java Implementation of a Component Model with Ex plicit Symbolic Protocols 4th International Symposium on Software Composition SC 05 vol 3628 of LNCS Springer p 115 124 2005 Plasil F Visnovsky S Behavior Protocols for Software Components IEEE Trans Softw Eng vol 28 n 11 p 1056 1076 2002 Schmidt H Trustworthy components compositionality and prediction J Syst Softw vol 65 n 3 p 215 225 2003 Siidholt M Model of Components with Non regular Protocols 4th International Sympo sium on Software Composition SC 05 vol 3628 of LNCS Springer p 99 113 2005 Yellin D Strom R Protocol Specifications and Component Adaptors ACM Transactions on Programming Languages and Systems vol 19 n 2 p 292 333 1997 Zimmermann W Schaarschmidt M Checking of Component Protocols in Component Base
12. alable nos obligations de preuve dans le formalisme pour pouvoir relever les points d incoh rence dans le protocole En reprenant l exemple de la s quence connexion connexion l application du principe de notre analyse aboutit faire la preuve de post connexion pre connexion or cette formule est fausse donc non prouvable on d tecte ainsi l incoh rence 4 3 M thodologie et r gles de conception de protocoles Le d finition adopt e pour les protocoles est relativement souple et flexible ce qui permet de mod liser des cas vari s A l inverse il est int ressant de d finir des r gles de bon usage des protocoles pour viter des incoh rences Nous en discutons ici quelques pistes La cr ation de protocoles peut intervenir dans une d marche de conception descen dante ou ascendante Dans le premier cas il est probable que les services mentionn s seront des coquilles vides destin es tre enrichies ou raffin es Dans le second cas plusieurs services existent avant que l on cr e des protocoles pour organiser ou figer une ou plusieurs utilisations ce qui implique potentiellement des changements dans 32 LMO 2007 l interface du composant Par exemple si certains services deviennent contr l s par des protocoles alors les composants qui les utilisaient doivent modifier leur interfaces de services requis Il est possible de hi rarchiser l usage des services et protocoles dans une pr sentatio
13. ation condens e qui met plat plusieurs niveaux distincts de description tels que composant et interface service et interface dynamique et contrats Une seule interface est repr sent e Les services offerts resp requis sont repr sent s par des rectangles gris s resp blancs Un lien d assemblage est repr sent par un trait reliant un service requis un service offert Dans le comportement dynamique du service requete offert par le composant IHM_CLIENTR deux points d expansion de type service optionnel permettent l appel ventuel des services code et montant l tat e1 Ces services sont consid r s ici sous une forme r duite pour faciliter la lecture en r alit ils sont suffisamment com plexes pour ne pas se r duire un simple envoi de message contr le du demandeur et cryptage des informations Dans cet exemple code et montant sont des sous services offerts par requete via le service requis retirer Les pseudo transitions en pointill entre l tat e1 de requete et les tats initiaux et finaux de code illustrent l expansion qui est g n r e syst matiquement lors de la v rification comportementale 26 LMO 2007 et selon chaque contexte d invocation de service d un composant Elles ne figurent pas dans une sp cification Kmelia Les points d expansions de type obligatoire se placent sur des transitions et sont expans es en utilisant le m me principe cf figure 2 IHM_CLIENTR requete
14. ccus s connexions d connexions ren vois est r gi par des r gles bien pr cises Dans une architecture pair pair un n ud est serveur et client de services comme le partage de fichier l change de donn es ou la t l phonie En r sum les protocoles peuvent servir contr ler des sessions des processus ou des classes de services en plus de l aspect protocoles de communication qui d taillent les principes de bonne communication entre participants Allen et al 1997 Dans la suite nous proposons une m thode de prise en compte de ces protocoles dans le mod le Kmelia 3 Protocoles dans Kmelia Apr s une br ve description du mod le Kmelia nous montrons comment d crire en Kmelia des protocoles de composants r pondant aux exigences de lisibilit de flexi bilit mais aussi de simplicit de mise en uvre pour le concepteur de composants 3 1 Kmelia Kmelia est un mod le de sp cification de composants bas s sur des descriptions de services complexes Les composants sont abstraits ind pendants de leur environne ment et par cons quent non ex cutables Kmelia peut servir mod liser des architec tures logicielles et leur propri t s ces mod les tant ensuite raffin s vers des plate formes d ex cution Andr et al 2006b Il peut aussi servir de mod le commun pour l tude de propri t s de mod les composants et services abstraction inter op rabilit composabilit Les ca
15. d Systems 5th International Symposium on Software Composition SC 06 vol 4089 of LNCS Springer p 1 17 2006
16. ia n inclut pas de contraintes dans la d finition de composants et de protocoles restreignant l interface d un composant certains services si un proto cole est pr sent une telle contrainte contredirait le mod le dans la mesure ou celui ci est bas sur des composants et des services et non des protocoles qui ne sont que des services affubl s d une propri t particuli re non sp cifique au mod le Cependant il est possible d crire les propri t s correspondantes qui peuvent tre v rifi es et utili s es pour tablir des contraintes ou mettre des messages d avertissements Une partie de ces propri t s a t crite et implant e de mani re ad hoc pour l instant 4 4 Outillage La plate forme COSTO Component Study Toolbox est une bo te outils pour sp cifier analyser et d velopper des composants Kmelia COSTO contient un analy seur compilateur de sp cifications qui permet de traiter des sp cifications Kmelia et de les repr senter dans une structure abstraite sous forme d objets COSTO comprend galement des traducteurs de sp cifications Kmelia en Lotos et en MEC afin d obtenir des sp cifications en entr e des outils d analyse formelle tels que CADP et MEC L introduction de protocoles dans COSTO est r alis e pour la compilation et la v rification de compatibilit interface et comportement dans les assemblages de Protocoles en Kmelia 33 composants La v rification des contrats
17. ifs de ces trois services aux tats i e0 et el A protocoleRetrait BASEGAB protocoleRetrai i connexion _ dem_code e0 _ idem_montant retrait e1 lt lt retrait gt gt deconnexion amp consultation i connexion deconnexion Figure 2 Un protocole pour le composant BASEGAB Ce protocole est tr s simple car il n int gre ni boucles l exception de celle implicite que constitue lt lt retrait gt gt ni gardes ni actions l mentaires sur des va riables pour tablir des compteurs de boucles ou des restrictions de chemins Il est pr sent dans l interface du composant au m me titre qu un service et peut tre appel comme n importe quel autre service pr sent dans l interface Les services pr sents dans le protocole sont appel s dans le cadre du protocole tout comme les sous services d un service sont appel s dans son contexte cf section 3 1 Dans la sp cification des services en Kmelia un protocole est distingu d un ser vice par l emploi du qualificatif protocol dans l ent te du protocole ci dessous provided protocoleRetrait Properties protocol nonInterruptible Pre true Post true Protocoles en Kmelia 29 Formellement le service p Ip Bp est un protocole si sub 0 A calp 0 A reqp D A Ly C subp U intp U L o L est l ensemble des actions l mentaires portant uniquement sur les variables locales au protocole et les variables de
18. ire que lorsque le protocole est d marr par l effet d un appel d un service client il doit se poursuivre jusqu ach vement le client s engage enchainer convenablement les appels de services Une mani re simple et efficace d introduire des protocoles dans Kmelia est de les faire appara tre comme un service offert qui donne acc s d autres services du com posant De nombreux l ments du mod le Kmelia permettent de sp cifier les caract ristiques des protocoles exprim es ci dessus 1 les syst mes de transitions tiquet s tendus expriment des enchainements d activit s dans le composant 2 les interfaces de services et de composants permettent de contr ler l acc s certains services et de subordonner l utilisation d un service un autre 3 les points d expansion permettent de hi rarchiser des d roulements de service au sein d un syst me de transition Du point de vue du mod le les protocoles constituent donc une classe particuli re de ser vices caract ris e notamment par une restriction sur les actions pr sentes dans le com portement chaque transition ventuellement gard e est tiquet e soit par un point d expansion correspondant un service qui doit tre appel en l absence de choix par le service qui utilise le protocole soit par une manipulation de variable locale li mit e aux types simples pour exprimer par exemple des conditions d encha nement comp
19. l espace d tat du composant A cette contrainte s ajoutent des r gles m thodologiques de bonne d finition cf section 4 Une partie de la s mantique d un protocole est celle d un service Kmelia elle est obtenue par le d veloppement des points d expansion La d finition actuelle des points expansions et le partage implicite du canal de communication entre le service et le protocole qui le propose font qu il n y a pas parall lisme possible entre les deux Le d veloppement consiste 1 pour la partie dynamique inclure a renommage pr s des tats et des actions l automate dynamique du service offert dans l automate du protocole et 2 pour la partie fonctionnelle tablir la cha ne des contrats pre post a renommage pr s des variables locales au service et des actions Les interfaces des services et leurs comportements doivent tre compatibles Dans cette interpr tation les m mes r gles de contr le s appliquent aux services et aux protocoles Cependant un concepteur ou un programme pourra utiliser le fait qu il poss de la propri t pro tocole pour le consid rer autrement par exemple s il existe des r gles de conception concernant des protocoles On peut alors exprimer des r gles ou des v rifications qui ne sont valables que pour les protocoles comme la section suivante va le montrer 4 Conception et v rification des protocoles Un composant mis disposition des d veloppeurs doit
20. mentaires un message correspondant un change atomique service op ration m thode ou simple communication selon le mod le Le formalisme est souvent une variante des alg bres de processus CSP des machines tats FSM LTS STS statecharts ou des expressions r guli res Les pro 1 une version plus d taill e est accessible lina atlanstic net fr equipes team10 Kmelia protocolesCBSE html 22 LMO 2007 pri t s sont d finies par des expressions variantes de logique temporelle ou par des algorithmes Elles sont tablies par des m thodes de test de d monstration automa tique ou de v rification de mod les Approche Crit res Outils Contenu Rattachement Formalisme Propri t Atte Atti eral 2003 msg calculs meme awomaes CL Beugnard Beugnard eral 1999 java interface __ Canal Canal er al 2003 mse meme open ru Heenziger de Alfaro etal 2001 msg interface awomates equiv UML 2 0 OMG 2005 msg actions composant statechars Yellin Yellin er al 1997 sg Plasil Past er al 2002 i ee m p EE Royer Pavel er al 2005 m thode f composa ss Sudolt S dholt 2005 m thode composant pros aso Schmidt Schmidt 2003 mse meme FM ooo x T EE s LTL Moizan Moisan er al 2003 Kmelia Attiogb eral 2006 msg actions Giannakopoulou et al 1999 b Zimmermann et al 2006 Tableau 1 Synth se com
21. n deux niveaux en contr lant tous les services par des protocoles Cette clarification d usage des concepts devient lourde pour les services communs ind pen dants d un composant tels que les consultations Rappelons que rien n oblige a priori les concepteurs d un composant de ne proposer que des protocoles comme services offerts dans l interface de ce composant Plusieurs cas de figure peuvent alors ven tuellement poser probl me Si un des protocoles est interruptible tout service pr sent dans l interface peut tre appel chaque tat du protocole Cela peut provoquer une explosion combina toire de la recherche de s quences incoh rentes dans le protocole Lorsqu un service s est le seul qui permettre d tablir la pr condition d un autre service sj alors s doit appara tre dans le protocole d utilisation et avant s Afin d viter des incoh rences dues aux interf rences avec l tat d un compo sant il est d conseill d avoir dans l interface du composant les services op rant des modifications d une partie de l tat prise en compte dans les pr conditions de services contr l s par des protocoles interruptibles Un service poss dant dans sa pr condition un pr dicat portant seulement sur l tat du composant et pas un param tre ventuel n a pas sa place dans l interface du composant mais devrait plut t tre contr l par un protocole Le mod le Kmel
22. nce nous avons envisag une passerelle avec un prouveur de th or mes Atelier B Les travaux en perspectives en plus de l extension d autres exemples d appli cation concernent trois points principaux i la prise en compte d autres propri t s en plus de la coh rence correction des fonctionnalit s fournies sous contr le de pro tocoles ii l exploitation des cas d anomalies pendant l analyse de coh rence pour sugg rer des modifications des composants protocoles ou bien une introduction de services ou de composants d adaptation iii le raffinement vers des plate formes exis tantes Fractal SOFA Chacun de ces points fera l objet d une mise en uvre sous forme de modules et de passerelles dans notre plate forme exp rimentale COSTO 6 Bibliographie Allen R Garlan D A Formal Basis for Architectural Connection ACM Transactions on Software Engineering and Methodology vol 6 n 3 p 213 249 July 1997 Andr P Ardourel G Attiogb C Coordination and Adaptation for Hierarchical Compo nents and Services Third International ECOOP Workshop on Coordination and Adapta tion Techniques for Software Entities WCAT 06 p 15 23 2006a Andr P Ardourel G Attiogb C Sp cification d architectures logicielles en Kmelia hi rarchie de connexion et composition re Conf rence Francophone sur les Architectures Logicielles Herm s Lavoisier p 101 118 2006b 34
23. oire d utilisation des services Du point de vue du fournisseur les protocoles per mettent d all ger la description individuelle des services et d gagent des services les contraintes d encha nement et des conditions g n rales du composant Le protocole est d fini un niveau de granularit plus large que celui des services ce qui favorise l abstraction la r utilisabilit et la modularit des composants Prenons quelques exemples pour illustrer l emploi des protocoles d utilisation Pour utiliser correctement la lecture et l criture dans un serveur de fichiers il faut d abord ouvrir les fichiers et ne pas oublier de les refermer il faut aussi s assurer de l exclusivit lors de l criture Dans un guichet automatique bancaire GAB pour r aliser des op rations services de retrait consultation d p t transfert l usager doit au pr alable s identifier se connecter on doit aussi tablir les liaisons distantes n 24 LMO 2007 cessaires au bon fonctionnement des services Par ailleurs tous les usagers n ont pas les m mes droits et possibilit s d utilisation un usager quelconque peut retirer de l argent un usager ayant un compte dans la banque du guichet peut en plus r aliser des op rations sur compte un personnel de la banque peut r aliser des services de maintenance Dans un protocole r seau tel que TCP les changes sont assimilables des services et l ordre des changes envois a
24. otocoles Kmelia dans la section B La section Jest consacr e la conception et la v rification des protocoles l analyse de coh rence des protocoles et l interaction entre les composants dont les services sont contr l s par des protocoles Nous concluons dans la section5Jet nous indiquons les perspectives de ce travail 2 Le protocole un mode d emploi des composants Cette section discute de l usage de protocoles pour documenter l utilisation des composants logiciels Protocoles en Kmelia 21 2 1 Motivations Pour se servir d un composant l utilisateur recherche dans la documentation de l interface du composant la description individuelle des services offerts et celle des services qui l int ressent Les d pendances et les contraintes d enchainement pouvant exister entre les services sont rarement d crites explicitement ou se trouvent r par ties dans la documentation Sans assistance l utilisateur pourrait invoquer de mani re inappropri e ces services utiliser n importe quel service dans n importe quel ordre en se basant sur la description individuelle des services Si des interd pendances sont d crites dans la sp cification des services par exemple sous forme de contrats alors les pr conditions risquent d tre complexes en prenant en compte les encha nements Laisser l utilisateur le soin de l analyse des cas possibles n est gu re envisageable en raison de l explosion combinatoire
25. parative des protocoles dans les mod les composants On peut classer sommairement les approches en trois cat gories en accordant plus de poids au crit re unit de rattachement qui est un crit re structurant 1 Celles dont le protocole d finit le cycle de vie du composant Becker Inve radi Kramer Moizan Royer Sud lt UML Zimmermann Un unique protocole est associ au composant ou son unique interface ce qui est quivalent Dans ces ap proches le composant est un processus et les services sont soit atomiques messages soit d finis par un comportement sp cifique Moizan UML 2 Celles dont le protocole d finit le cycle de vie d une vue du composant Allen Attie Beugnard Canal Henziger Plasil Schmidt Yellin Un protocole est associ une interface et plusieurs interfaces coexistent Les interfaces peuvent tre limit es un seul composant cible assimilable un connecteur ou pas 3 Celles dont le protocole d finit un usage du composant Kmelia Plusieurs pro tocoles coexistent au sein du composant dans une ou plusieurs interfaces Sur ce crit re les approches retenues ne sont pas radicalement diff rentes en terme d expressivit mais elle le sont en termes de facilit d expression et d utilisation car c est au concepteur d architectures de g rer la complexit induite au d veloppeur de la r soudre et l utilisateur de la comprendre Prenons l exemple du multi
26. posant avec des informations de typage issues des param tres de l interface de s et du composant vli tli vgn tgk R vli ugx De la m me fa on le pr dicat Q pr condition du service s est exprim avec les variables locales vl du service s et des variables globales vg du composant avec des informations de typage issues des param tres de s et du composant vl tlj vgr tgk e Q vl vgk Puisque nous raisonnons en dehors du contexte de d roulement effectif des ser vices les valeurs des variables locales sont inconnues on les suppose dans le meilleur des cas convenables pour la v rit des pr dicats au moment des appels de services les seules hypoth ses de travail sont celles sur les variables globales on restreint alors les pr dicats R vl vgk et Q vl vgk R vgr et Q vgk La propri t de d part ul tli vgk tgk R vli vgk gt ul tlj vgk tgk Q ul vgx devient alors vgk tgk R vgk Avge tgk e Q vgk Lever partiellement cette restriction sur la port e des pr dicats est faisable dans certains cas un param tre peut tre contraint dans une pr condition et une postcondi tion peut tablir qu une variable globale a la valeur de ce param tre comme nouvelle valeur mais tr s co teux en terme de preuve A partir de l nous devons int grer les pr dicats R et Q avec leurs contextes variables types dans le prouveur cible en transformant au pr
27. r guide and that of expressing usage constraints by specifying multiple user guides which can be used as services To ensure the correctness of the protocols a technique of consistency analysis is provided This study is experimented on the Kmelia component model MOTS CL S protocoles mod les de composants propri t s de correction et coh rence KEYWORDS protocols component models correctness and consistency properties 20 LMO 2007 1 Introduction L approche des composants logiciels constitue une solution pour d velopper des logiciels de fa on modulaire et en r utilisant l existant Cependant ce n est pas fa cile de trouver des composants appropri s un besoin sp cifique et pouvoir s en servir convenablement Plusieurs mod les composants proposent un langage de description d interface IDL qui fournit la documentation utilisateur des composants sous forme d interface Le langage IDL permet de d crire les fonctionnalit s offertes dans l inter face du composant ses services offerts et pour chacun de ces services le profil des op rations Cependant selon les mod les composants l interface propos e l utili sateur est plus ou moins expressive et inclut ou non plusieurs aspects parmi lesquels la pr sence de services requis dans l interface ceux n cessaires la r alisation des services offerts le support multi interface plusieurs interfaces disponibles en g n ral li
28. ract ristiques principales du mod le Kmelia sont les composants les services et les assemblages Leur description formelle est donn e dans Attiogb et al 2006 Un composant est d fini par un espace d tats des services et une interface T L espace d tat est un ensemble de constantes et de variables typ es contraintes par un invariant Dans l interface d un composant on distingue les services offerts I qui r alisent une fonctionnalit et les services requis I qui d clarent les besoins des fonctionnalit s Allen et al 1997 Medvidovic et al 2000 Les services sont eux m mes constitu s d une interface qui peut inclure des sous services d une descrip tion d tat et d assertions pre post conditions Formellement un service s est d fini par un couple Is Bs o I est l interface du service et B est un ventuel compor tement dynamique les services requis n en n ont pas L interface du service est une abstraction des relations de composition de services soit une composition horizon Protocoles en Kmelia 25 tale ou d pendance soit une composition verticale ou inclusion Le comportement dynamique d un service offert est caract ris par un automate qui pr cise les en cha nements d actions autoris s Ces actions sont des calculs des communications missions r ceptions de messages des invocations ou retours de services Un des objectifs de Kmelia est de permettre l
29. s d un composant L utilisation de protocole en tant que mode d emploi embarqu dans un composant en facilite la documentation et l int gration dans un cadre non d termin l avance De fa on orthogonale les protocoles peuvent s inscrire dans une d marche contractuelle en s associant avec des assertions Becker Beugnard Kmelia Schmidt UML OCL Schmidt et des contraintes non fonctionnelles comme la qualit de ser vice Becker Beugnard Il est vident que ces aspects sont importants pour la docu mentation et la v rification d assemblage de m me que le traitement de l adaptation Allen Becker Canal Kmelia Schmidt Yellin Notons que certaines approches traitent de la r cursion Sud lt Zimmerman du sous typage de protocoles Becker Plasil Yellin ou du raffinement Henziger Moi zan D autres relient les protocoles des implantations de composant Allen Kramer Royer ou proche de mod les comme CORBA Canal ce qui leur donne la fois une certaine cr dibilit mais aussi des structures moins abstraites Mais ces aspects ne concernent pas directement la documentation et l int gration de composants 2 3 Protocole d utilisation Un protocole d finit un mode d emploi de son composant Plus pr cis ment il d finit des r gles d encha nement de services du composant c est un protocole d uti lisation En explicitant la dynamique de l ensemble des services on r duit la combi nat
30. t v rifi es la compatibilit des interfaces de services offerts requis et leur compatibilit comportementale Dans ce dernier cas il est noter que les probl mes d explosion combinatoire sont limit s puisque la correction globale des interactions est l union des corrections locales d in teraction Attie et al 2003 Dans notre cas une interaction est la donn e de trois services un contexte un service offert v rifier li un autre service offert l ap pelant via un service requis dans l assemblage Ces v rifications sont faites l aide des outils existants de la plate forme COSTO permettant l analyse syntaxique et struc turelle des composants via des algorithmes ad hoc et la v rification des compatibilit s comportementales par exemple la v rification de la bonne interaction avec des ser vices offerts en s appuyant sur les environnements LOTOS CADP ou MEC 4 2 Coh rence des protocoles La d tection d incoh rence dans les protocoles fait partie des v rifications n ces saires pour assurer la correction d un composant Un protocole r d un composant C est incoh rent si un des encha nements de services qu il d crit peut tre impossible du seul fait de l encha nement Les deux causes d incoh rence suivantes peuvent tre d tect es L existence de chemins gard s sans alternatives menant l tat final du proto cole dans le cas o l expression de ces gardes ne peut
31. teur de boucles pr dicats de chemin Le mod le Kmelia permet d associer des propri t s nomm es aux entit s du langage services et composants notamment Il s agit d un m canisme d extension dans le sens o les propri t s peuvent tre exploi 28 LMO 2007 t es par la suite l instar des restrictions exprim es dans des st r otypes UML La restriction pr dicat qui caract rise la propri t protocole est associ e au qualificatif protocol dans l ent te du service La repr sentation de protocoles comme classe de services pr sente plusieurs avantages simplicit du support multiprotocole pas de ni veaux structurants complexes qui rendent plus d licate l utilisation par d autres com posants interop rabilit avec les mod les qui ne supportent pas les protocoles pour l assemblage de composants h t rog nes volutivit des mod les un protocole peut devenir un service dans un autre composant ou un raffinement de composant exten sion coh rente de Kmelia une nouvelle classe de services Prenons un exemple simplifi dans lequel les l ments de visibilit et de structura tion sont masqu s et qui fait appara tre le comportement dynamique du protocole La figure 2 pr sente le protocole protocoleRetrait du composant BASEGAB qui sp cifie un ordre sur l usage des services connexion retrait et deconnexion Les points d expansion de service de type obligatoire impliquent les appels respect
32. tre valu e vrai L existence dans un protocole d une s quence d appels s1 sn Sn41 telle que la prise en compte des postconditions de s sn implique la n gation de la pr condition de 5 1 c est dire qu un des services appel s avant Sn et dont les effets n ont pas t remis en cause emp che le d roulement correct de 5 41 il s agit d une s quence infaisable Par exemple si le service connexion pos s de une pr condition not connected et une postcondition connected la s quence connexion connexion rend le protocole incoh rent ainsi que toute autre s quence ne contenant aucune modification de connected entre deux appels de connexion Pour l analyse des suites de s quences infaisables nous exp rimentons une passe relle avec des prouveurs de th or mes bas s sur la logique du premier ordre tel que Atelier Le principe est le suivant on consid re un protocole non expans et les sous s quences d appels de services allant d un tat initial un tat final du protocole pour viter les boucles Pour chacune de telles s quences on v rifie que pour toutes les sous s quences 5 sj avec j 1 qu elle contient post s gt pre s 3 www atelierb societe com Protocoles en Kmelia 31 Le pr dicat R postcondition d un service s est exprim avec des variables locales vl du service s qui sont les param tres du service et des variables globales vg du com
33. uis d un composant quel conque les offerts en interne dans le cadre du service s B le comportement d un service s est un syst me de transitions tiquet es tendu ou eLTS sp cifi par un sexuplet S L So Sr o S est l ensemble des tats de B So S est l tat initial Sr C S est l ensemble non vide des tats finaux le service se termine toujours L est l ensemble des tiquettes des transitions entre les l ments de S les actions autoris es y compris les points d expansion obligatoire S x L S est la relation de transition entre les tats de S selon les tiquettes S sub est la relation d tiquetage des tats par des points d expansion de type optionnel Les composants Kmelia peuvent tre assembl s ou compos s via des liens entre services Dans un assemblage les services requis par certains composants sont li s connect s aux services offerts d autres composants Ces liaisons appel es liens d as semblage tablissent des canaux implicites pour les communications entre services Protocoles en Kmelia 27 Les canaux sont point point dans la version actuelle du mod le mais bidirection nels La figure Hillustre une vue partielle d un assemblage du GAB dans laquelle on se focalise sur le lien retirer retrait pour lequel deux sous liens sont d finis il n y a pas de restrictions la profondeur des sous liens elle est li e la composition verti cale
Download Pdf Manuals
Related Search