Processus de fabrication de systèmes répartis centré sur un modèle : l'expérience du projet MORSE

01/09/2017
Publication REE REE 2006-3
OAI : oai:www.see.asso.fr:1301:2006-3:19744
DOI :

Résumé

Processus de fabrication de systèmes répartis centré sur un modèle : l'expérience du projet MORSE

Métriques

16
4
3.17 Mo
 application/pdf
bitcache://ab068c06dfa61227f4a3e378a4a281d32f30aa14

Licence

Creative Commons Aucune (Tous droits réservés)
<resource  xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
                xmlns="http://datacite.org/schema/kernel-4"
                xsi:schemaLocation="http://datacite.org/schema/kernel-4 http://schema.datacite.org/meta/kernel-4/metadata.xsd">
        <identifier identifierType="DOI">10.23723/1301:2006-3/19744</identifier><creators><creator><creatorName>Fabrice Kordon</creatorName></creator><creator><creatorName>Frédéric Gilliers</creatorName></creator><creator><creatorName>Yann Thierry-Mieg</creatorName></creator></creators><titles>
            <title>Processus de fabrication de systèmes répartis centré sur un modèle : l'expérience du projet MORSE</title></titles>
        <publisher>SEE</publisher>
        <publicationYear>2017</publicationYear>
        <resourceType resourceTypeGeneral="Text">Text</resourceType><dates>
	    <date dateType="Created">Fri 1 Sep 2017</date>
	    <date dateType="Updated">Fri 1 Sep 2017</date>
            <date dateType="Submitted">Tue 15 May 2018</date>
	</dates>
        <alternateIdentifiers>
	    <alternateIdentifier alternateIdentifierType="bitstream">ab068c06dfa61227f4a3e378a4a281d32f30aa14</alternateIdentifier>
	</alternateIdentifiers>
        <formats>
	    <format>application/pdf</format>
	</formats>
	<version>33518</version>
        <descriptions>
            <description descriptionType="Abstract"></description>
        </descriptions>
    </resource>
.

Repères 2 LE PROJET MORSE m Processus de fabrication de systèmes répartis centré m sur un modèle : l'expérience du projet MORSE Mots clés Modélisation, Vérification, Générationautomatique deprogrammes, Model Checking Frédéric GILLIERS, Fabrice KORDON, Yann THIERRY-MIEG LIP6-SRC, Université P & M Curie 1. Introduction La complexité des systèmes croît de manière non contrôlée [16] et il apparaît que les techniques « tradition- nelles » de développement, basées sur une démarche objet et le test (unitaire puis d'intégration) ne suffisent plus à assurer un besoin de qualité sans cesse croissant. Pour preuve, de la " crise du logiciel " dans les années 1960, on est passé à la " crise chronique du logiciel " dans les années 1990 [6]. Le problème est particulièrement crucial dans le contexte actuel d'applications de plus en plus réparties. La répartition génère un asynchronisme entre flots d'exé- cutions parallèles qui complique la compréhension de la dynamique du système. C'est cette multiplicité des exé- cutions possibles qui bloque l'analyse des systèmes par des méthodes de tests. Pour s'assurer que le système a un comportement déterministe (i.e. il se comporte de manière similaire pour toutes les séquences d'exécutions possible), il faut passer à des approches sûres : les méthodes formelles. Cependant, les méthodes formelles ne sont hélas pas la solution miracle. De nombreux auteurs comme [23, 17] signalent de nombreuses difficultés comme la difficulté d'apprentissage, l'adaptation à un processus de dévelop- pement de type industriel ou le passage à l'échelle. Pour rendre ces approches utilisables, il faut être pragmatique et concilier des techniques formelles avec une démarche méthodologique permettant leur usage dans un monde industriel grâce à des outils utilisables par les ingénieurs. Sur ces points, beaucoup de progrès sont fait actuelle- ment. Dans ce contexte, le projet MORSE définit une démarche méthodologique centrée sur UML pour aider des ingénieurs à construire une application dont le com- portement sera déterministe, puis à produire l'application correspondante. Le projet MORSE couvre donc les points suivants : 1) la mise en place d'une méthodologie adaptée au domaine d'application considéré ; 2) la définition d'un langage de spécification, adapté au domaine et aux besoins de génération de code et de vérification en aval ; 3) la mise en place de techniques de vérification du bon comportement du système ; 4) la réalisation d'un générateur automatique de programmes pour produire le système rapidement et sans dérive par rapport à la spécification. De plus l'intégration dans un contexte industriel exis- tant impose au niveau modèle une compatibilité avec des ESSENTIEL SYNOPSIS La complexitédes systèmes croît de manière non contrôlée et il apparaîtque lestechniques« traditionnelles »de développement, baséessur une démarcheobjet et le test (unitairepuis d'intégra- tion) ne suffisent plus à assurer un besoin de qualité sans cesse croissant. Dans ce contexte, nous présentons les résultats du ProjetMORSEqui vise à intégrerdans une démarcheméthodolo- gique centrée sur UML, l'utilisation de méthodes formelles et de générateursautomatiques de programme. MORSEa ainsi pour objectif de rendreaccessibleà des ingénieursspécialistesde leur métier des techniques de conception et de développement pro- pres aux systèmes répartis. As the complexity and sizeof software systems increasesuncon- trolably, "traditional" development methodologies that rely on tests to ensure quality needs are showing their limits. In this context, we present the results of the MORSE project, which aims at offering a development methodologybasedon UML, that offers support for code generation and formal verification.Thus MORSE'sgoal is to provide software designers expert in their business model with high level concepts adapted to distributed systems, that help to master their complexity. 102 REE No 3 Mars2006 Processus de fabrication de systèmes répartis centré sur un modèle 'expérience du projet MORSE aspects de l'application modélisés en UML, et au niveau logiciel un mécanisme permettant la réutilisation et l'in- tégration de composants existants. Cet article vise à relater l'expérience dans ce domaine du projet MORSE et à en présenter les premiers résultats au bout de deux ans (sur trois) de déroulement du projet. La section suivante évoque les problèmes du dévelop- pement d'applications réparties que nous adressons. Nous présentons ensuite la démarche méthodologique de MORSE (section 3) avant d'aborder le langage de spéci- fication que nous utilisons (section 4). Nous exposons alors les techniques de vérification mises en oeuvre (section 5) puis enfin les aspects liés à la génération auto- matique de programmes (section 6). 2. Poînts clefs Nous présentons ici les problèmes principalement liés aux ruptures dans le cycle de vie du logiciel et les tendan- ces de la communauté scientifique. 2.1. Rupture du cycle de vie Le cycle de vie du développement logiciel contient plusieurs ruptures importantes (figure 1). La première se situe entre la phase d'analyse et la phase de conception. On passe d'un raisonnement en lan- gage naturel à un autre basé sur les principes de l'objet (et s'appuyant en général sur UML). Nous ne nous intéresse- rons pas dans cet article à cette première rupture mais l'intérêt d'approches à base de logique a été identifié dès les années 1990 [15]. C'onception EïnsiSSu l.nn. Nal. l;:Llf['Lnt. l'rn. + l:in. l-.rrc (lLjrLCl'r-' ".1. : ;'1. L,,,,j. Y'1 .''j : "...''-.LC' (aa : i : : o.. : i ;'td ! j.Li. itf, outpuî => d ! sptayHand ! er. ! tf) - l'Pl i- i [ - 1 -1 -- r --1 1,1, ; 1 > - - i -. - 1 -] 1 l -.-, l,,-J, F i i. 1 . ; f1 *, 1, 1, t : 1 1 1, , 1,'11. 1. Figtire 8. Instanciation dynaiiiique d'line classe LJP et le code généré associé. un générateur de programmes prototypes en langage Java [8]. Pour des besoins d'expérimentation du projet MORSE, un générateur vers C++, reprenant les princi- paux choix du générateur Java, est en cours de finalisa- tion. 6.4. L'environnement d'exécution Une fois l'application répartie développée, il reste à la déployer sur un ensemble de machines. Dans le cadre d'un projet comme MORSE, cela signifie que certains processeurs peuvent être embarqués. Cette opération pose donc des contraintes particulières. L'usage d'un middleware permet de s'abstraire des caractéristiques du système d'exploitation et du matériel. Mais cette approche a l'inconvénient d'entraîner un important surcoût, que ce soit en emprunte mémoire ou en utilisation des ressources. Ainsi, le middleware " idéal ", dans le contexte de MORSE, doit tout d'abord être fortement configurable : il doit fournir des services pour implémenter l'exécutif LjP aussi bien sur une machine équipée d'un système d'exploitation complet (par exemple sous Linux) que sur des noeuds ayant de fortes contraintes mémoire. Une grande versatilité sur les API proposées aux développeurs et les protocoles d'interaction entre noeuds d'une application répartie serait aussi un avantage com- plémentaire certain. En effet, cela permet d'adapter les protocoles en fonctions des conditions dans un système réparti hétérogène. Par exemple, dans un système partiel- lement embarqué dans des satellites, on choisira un pro- tocole économe en bande passante pour une liaison espace/sol et des protocoles plus lourds entre les machines du centre de calcul qui exploite les données satellitaires. De tels middleware commencent à exister. Notons dans ce domaine les projets TAO [28], Quarterware [24] ou PolyORB [20]. TAO est utilisé dans de nombreux pro- jets, et PolyORB, outre une utilisation dans plusieurs pro- jets, fait l'objet d'un support technique par une société commerciale. Cela montre qu'une génération de middle- ware nouvelle intéressante pour supporter notre méthodo- logie de développement est opérationnelle. REE Nn 3 Mars2006 Repères 2 LE PROJET MORSE Conclusion Nous avons présenté dans cet article une méthodolo- gie pour les systèmes logiciels répartis développés dans le cadre du projet MORSE. Ce projet regroupe deux parte- naires industriels (Sagem-Défense et Aonix) avec deux laboratoires de recherche (LIP6 et LaBRI). Ce projet RNTL a débuté en juillet 2003 et se, terminera en 2006. La principale caractéristique de la méthodologie, MORSE est d'établir une liaison entre un niveau de des- cription UML (contraint par un profil dédié) et la vérifi- cation formelle d'une part et la génération automatique de programmes d'autre part. Nous espérons ainsi rendre les techniques formelles utilisables dans le contexte d'un développement industriel. Des outils intègrent la majeure partie du savoir faire dans la maîtrise des applications réparties, les ingénieurs de développement se focalisent alors sur les parties métier de leur domaine. La méthodologie est actuellement opérationnelle : . le profil UML-MORSE est intégré dans une version étendue d'Améos, l'AGL d'Aonix ; . le langage LjP sert de pivot entre la modélisation, la vérification et la génération automatique de pro- grammes. LjP est synthétisé automatiquement par Améos ; . un outil de model checking est en cours d'implé- mentation, après que des expérimentations sur des spécifications caractéristiques aient démontré la fai- sabilité du problème [9] ; . des générateurs de code ont été développés en Java et en C++. Au contraire de la plupart des produits basés sur UML, ils produisent l'application com- plète (structure et comportement) dans un contexte d'exécution repartie. Les modèles et les outils ont été éprouvés sur des cas d'études simples. Dans la dernière année du projet MORSE, nous allons réaliser une étude de cas complexe issue des activités de Sagem-Défense. Cette étape de vali- dation nous permettra d'affiner les besoins et d'identifier les étapes futures à mettre en oeuvre pour la conception d'un environnement de développement industriel basé sur les principes du prototypage par raffinement [13], un cycle de développement itératif centré sur un modèle de haut niveau. Références [1] B. Berthomieux, P-0. Ribet, F V.J.-L. Bernartt, J.-M. Farines, J.-P Bodeveix, M. Filali, G. Padiou, P Michel, P Farail, P Gauffilet, P Dissaux, & K.-L. Lambert, "Towards the Verification of Real-Time Systems in Avionics the Cotre Approach'.'In Proceedings of the 8th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'03), 2003. [21 R. Bryant, " Graph-based Algorithms for Boolean Function Manipulation' : IEEE Transactions on Computers, 35 (8) 677-691, August 1986. [3] R. Clark & A. Moreira, " Use of E-LOTOS in Adding Formality to UM'Journal of Universal Computer Science, 6 (11) 1071-1087, 2000. [41 J.-M. Couvreur, E. Encrenaz, E. Paviot-Adet, D. Poitrenaud & P-A. Wacrenier, " Data Decision Diagrams for Petri Net Anaysis'.'n Proc. of ICATPN'2002, volume 2360 of Lecture Notes m Computer Science, pages 101-120. Springer Verlag, June 2002. [5] J.-M. Couvreur & Y Th-Mleg, " Hierarchical Decision Diagrams to Exploit Model Structure " In Proc. of the 25th IFIP WG 6. 1 Int. Conf on Formal Techniques for Networked and Distributed Systems (FORTE'05), volume 3731 of LNCS, pages 443-457, Taipei, Taiwan, October 2005. Springer [61 VV, Gibbs, " Softwares Chronic Crisis'.'Scientific American, 271 (3) 72-81, Sept, 1994 [7] F. Gilliers, " Sémantique du langage LJP'.'Laboratoire d'Informatique de PARIS VI, 2004, [81 F Gilliers, " Développement par prototypage et génération de code à partir de U ?, un langage de modélisation de haut niveau'.'PhD thesis, Universite Pierre et Marie Cune (Paris VI), 2005. [91 F. Gilliers, F Bréant, D. Poitrenaud & F Kordon, " Model Checking of High-Level Object Oriented Specifications :The Lf P Experience'.'In Third Workshop on Modelling of Objects, Components, andagents (MOCA'04), 2004, flOI F Gilllers, J.-P Velu & F Kordon, " Generation of Distributed Programs in their Target Execution Environment " In Fifteenth IEEE International Workshop on Rapid System prototyping, 2004. [111 J. Hugues, Y Thierry-Mieg, F Kordon, L. Pautet, S. Baarir & T Vergnaud, "On the Formal Verification of Middleware Behavioral Propertles' : ln Proceedings of the 9th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'04), volume ENTCS 133, pages 139 - 157, Linz, Austria, Sept. 2004. Elsevier [121 ISO. Meta Object Facility (MOF) specification. Technical report, ISO, april 2002. [131 F Kordon & J. Henke " An Overview of Rapid System [141 Prototyping Today' : Design Automation for Embedded Systems, 8(4) 275-282, december 2003. F. Kordon & M. Lemoine, editors, " Formal Methods for Embedded Distributed Systems How to Master the Complexity'.'Kluwer Academie, 2004. [15] L. Lamport. Managing proofs. ln TMargaria & B. Steffen, Editors, TACAS, volume 1055 of Lecture Notes in Computer Sc/ence, page 34. Springer, 1996. [16] N. Leveson, " Software Engineering : Stretching the Limits of Complexity'.'Communications of the ACM, 40 (2) : 129-131, 1997 [17] Luqi & J. Goguen, " Formal Methods : Promises and Problems'.'IEEE Software, 14 (l) : 73-85, January/February 1997 [18] S. N. Mejia, "Le méta-Modèle LfP'.'Laboratoire d'Informatique de PARIS VI, 2004. [19] OMG, " Model Driven Architecture (MDA) :' Document num- ber ormscl2OOl-O7-01, 2001 [201 L. Pautet & F Kordon, " Des vertus de la schizophrénie pour le prototypage d'applications à composants intéropérab) es " REE N. 1i Mars2006 Processus de fabrication de systèmes répartis centré sur un modèle : l'expérience du projet MORSE TSI, 2310) 1301-1328, 2004. [21] R. Silaghi, F Fondement & A. Strohmeier, " Towards an mda-Orienied uml Profile for Distribution'.'ln Proceedings of the Sth IEEE Enterprise Distributed Object Computing Conference (EDOC 2004), 2004. [22] D. Regep.Y.Thierry-Mteg&F. Kordon, " Modélisation et véri- fication de systèmes répartis : une approche intégrée avec UP' n Proceedings of AFADU03, January 2003. [23] H. Saiedian, "An Invitation to Forma ! Methods' ; Comparer, 29 (4) 16-17, 1996. [24] A. Singhai, A. Sane & R. H. Campbell, " Quarterware for Middlevvare'.'In ICDCS'98 : Proceedin_qs of the The 18th International Conference on Distributed Computing Systems, page 192,VVashington, DC, USA, 1998. IEEE Computer Society. [25] M. Team. " The MORSE Project home page' ; http ://morse.lip6.fr. [261 Y. Thierry-Mieg C. Dutheillet & 1. Mounier, "Automatic Symmetry Detection ln Well-Formed Nets'.'In Proc. Of ICATPN 2003, volume 2679 of Lecture Notes in Computer Science, pages 82-101, Springer Verlag, June 2003. [27] Y. Th.-Mieg, J.-M. Ilié & D. Poitrenaud, "A symbolic Symbolic State Space'.'In Proc. of the 24th IFIP WG 6. 1 Int. Conf on Formal Techniques for Networked and Oistnbuted 9 Systems (FORTE'04), volume 3235 of LNCS, pages 276-291, Madrid, Spain, September 2004. Springer. [28] N.Wang, K. Parameswaran, D. C. Schmidt & 0. Othman, " The design & Performance of Meta-Programming Mechanisms for Object Request Broker Middleware'.'In COOTS, pages 101-118. USENIX, 2001. Les auteurs Frédéric Gilliers est docteur de l'Université P & M. Curie et ensel- gnant à 'Université Paris X. Ses activités se concentrent sur la génération automatique de programmes répartis à partir de spéci- fications de haut niveau. Fabrice Kordon est professeur à l'Université P & M. Curie et res- ponsable du thème Systèmes Répartis et Coopératifs au Laboratoire d'informatique de Paris 6 LIP6), Ses centres d'intérêts sont à la convergence des systèmes répartis, des méthodes for- melles et du Génie Logiciel. Il a lancé de nombreux projets dans ces domaines (CPNAM !, PofyORB, MORSE, etc...). Yann Thieny-Mieg est Maître de Conférences à !'Un ! versité P & M. Curie. Ses activités concernent la modélisation et la vérification formelle de systèmes complexes par model checking. Il se focalise en particulier sur 'exploitation des spécifications UML pour les techniques de vérification. REE No 3 Mars 2006