Programme des journées nationales 2010 PDF Imprimer
Statiques
Écrit par Yves Ledru   

Programme des journées nationales du GDR GPL 2010

Le détail des sessions avec les résumés des présentations est donné en bas de page.

Les icon Actes des journées nationales 2010 sont disponibles en ligne.

Une Journée Thématique: Adaptation, Variabilité et Réutilisation dans l'ingénierie logicielle est organisée le 8 mars 2010 par le groupe de travail COSMAL.

mercredi 10 mars 9h-10h30 Conférencier invité :

A Classification Framework for Component Models

Ivica Crnkovic, Université de Mälardalen (Suède)

Président de session : Franck Barbier
Pause café et posters
mercredi 10 mars 11h-12h30

Présidents de session : Laurence Duchien et Yves Ledru

Présentation de l'institut INS2I (Florence Sèdes)

1ere session Défis pour le Génie de la Programmation et du Logiciel


Software (re)modularization: Fight against the structure erosion and migration preparation
Nicolas Anquetil, Simon Denier, Stéphane Ducasse, Jannik Laval, Damien Pollet, Roland Ducournau, Rodolphe Giroudeau, Marianne Huchard, Jean-Claude Konig and Abdelhak-Jamel Seriai

Component and Service Farms: Towards folkregistries
Gabriela Arévalo, Zeina Azmeh, Marianne Huchard, Chouki Tibermacine, Christelle Urtado and Sylvain Vauttier
mercredi 10 mars 12h30-14h Repas
mercredi 10 mars 14h-15h30

Session 1 : GT MTV2

Président de session : Arnaud Gotlieb

Exploration aléatoire de modèles

Johan Oudinet (LRI, Univ. Paris-Sud - CNRS)

Détection de Vulnérabilités Logicielles par le Test Passif
Amel Mammar, Ana Cavalli, Willy Jimenez ( Telecom SudParis)
Edgardo Montes de Oca  (Montimage)
Shanai Ardi, David Byers, Nahid Shahmehri (Linköpings universitet)

Combining Frama-C and PathCrawler for C Program Debugging
Omar Chebaro (CEA/LIST, LIFC),
Nikolai Kosmatov (CEA/LIST),
Alain Giorgetti (LIFC, INRIA),
Jacques Julliand (LIFC)

Session 2 : GT Transformations

Président de session : Pierre-Etienne Moreau

Machine-Checked Sequencer for Critical Embedded Code Generator
Nassima Izerrouken, (Continental Automotive, et Université de Toulouse, IRIT-ENSEEIHT)
Marc Pantel, Xavier Thirioux (Université de Toulouse, IRIT-ENSEEIHT)



Les plates-formes d'exécution dans l'IDM : Quelles modélisations pour quelles utilisations ?
Jérôme Delatour, Matthias Brun, Guillaume Savaton, Jonathan Ilias-Pillet, Cédrick Lelionnais (Groupe ESEO)

+ 2 exposés jeunes chercheurs
mercredi 10 mars 15h30-16h30

Session Posters/Démos et Pause café

  1. Alexandre Cortier. Projet SPaCIFY : Ingénierie des modèles et Méthodes Formelles pour les systèmes embarqués critiques (Poster)
  2. François Fages and Martin Julien. Modelling Search Strategies in Rules2CP (Poster et Démo)
  3. Arnaud Gotlieb. EUclide is a Constraint Language based on Imperative DEfinitions(Poster et Démo)
  4. Nassima Izerrouken, Marc Pantel and Xavier Thirioux. Integrated Formal Approach for a Qualified Critical Code Generator (Poster)
  5. Nour Alhouda Aboud, Philippe Aniorté, Eric Cariou and Eric Gouarderes. Integration of Agent and Component approaches by Service Oriented vision using Model Driven Engineering (Poster)
  6. Sabina Akhtar, Stephan Merz and Martin Quinson. Extending PlusCal: A Language for Describing Concurrent and Distributed Algorithms (Poster)
  7. Vincent Aranega. Traceability Mechanism in Transformations Chains Dedicated to Model and Transformation Debugging (Poster)
  8. Iyad Alshabani, Joyce El Haddad, Nikolaos Georgantas, Tarek Melliti, Lynda Mokdad and Pascal Poizat. Pervasive Service Composition (Projet ANR PERSO) (Poster)
  9. Thanh Thanh Le Thi. L’Activité de Génération de Codes Dirigée par les Modèles (Poster)
  10. Fatiha Zaidi, Richard Castanet, Ana Cavalli, Edgardo Montes de Oca and Andrey Sadovykh. WebMov : Modélisation, Test de la composition de services Web (Poster)
  11. Youssef Ridene, Franck Barbier, Nicolas Belloir and Nadine Couture. Définition d'un langage de modélisation spécifique (Domain Specific Modeling Language) au test d'applications embarquées sur téléphones mobiles (Poster)
  12. Sebastien Mosser and Mireille Blay-Fornarino. Taming Orchestration Design Complexity through the ADORE Framework (Poster et Démo)
  13. Regine Laleau. Projet ANR SELKIS (Poster)
  14. Akram Idani, Mohamed Amine Labiadh and Yves Ledru. Approche orientée modèles pour une intégration efficace de B et UML (Poster)
  15. Peggy Cellier, Mireille Ducassé, Sébastien Ferré and Olivier Ridoux. Fouille de données pour la localisation de fautes dans les programmes (Poster)
  16. Romain Adeline, Janette Cardoso, Christel Seguin, Pierre Darfeuil and Sophie Humbert. Vers une méthode de validation des modèles formels AltaRica (Poster)
mercredi 10 mars 16h30-17h30

Session 3 : GT RIMEL

Président de session : Salah Sadou

Une architecture de composants répartis adaptables
An Phung-Khac, Jean-Marie Gilliot et Maria-Teresa Segarra (TELECOM Bretagne)

OCL contracts for the verification of model transformations
Eric Cariou, Nicolas Belloir, Franck Barbier, Nidal Djemam (Université de Pau et des Pays de l’Adour / Liuppa)

Session 4 : GT  MFDL

Présidente de session : Marie-Laure Potet

Application du Model Checking aux commandes de vol : l’expérience Airbus
Thomas Bochot (AIRBUS & ONERA/DTIM), Pierre Virelizier (AIRBUS), Hélène Waeselynck (LAAS-CNRS), Virginie Wiels (ONERA/DTIM)

Définition d’une sémantique Event-B pour les patrons de raffinement de buts KAOS
Abderrahman Matoussi, Frédéric Gervais et Régine Laleau (LACL, UPEC)

mercredi 10 mars 18h30 Visite du château
mercredi 10 mars 20h Dîner de gala au palais Beaumont (en ville, pas très loin du château).
jeudi 11 mars 9h-10h30 Ouverture des journées nationales (Yves Ledru)

Conférencier invité :

Combiner Java et réécriture, c'est possible et utile

Pierre-Etienne Moreau , professeur à l'Ecole des Mines de Nancy , membre du LORIA /INRIA
Pause café et posters
jeudi 11 mars 11h-12h30

Session 5 : GT  COSMAL

Président de session : Mourad Oussalah

Matrice de dépendances enrichie

Jannik Laval, Alexandre Bergel, Stéphane Ducasse, Romain Piers (INRIA - Lille Nord Europe - USTL - CNRS UMR 8022)

Évaluation de l'efficacité des implémentations de l'héritage multiple en typage statique.
Floréal Morandat, Roland Ducournau (LIRMM)
Jean Privat {Université du Québec à Montréal)

Correction d'assemblages de composants impliquant des données et assertions
Mohamed Messabihi, Pascal André et Christian Attiogbé (LINA)

Session 6 : GT FORWAL

On-the-fly Emptiness Check of Transition-Based Streett Automata
Alexandre Duret-Lutz, Denis Poitrenaud, Jean-Michel Couvreur

Reachability Analysis of Communicating Pushdown Automata
Alexander Heußner, Jérôme Leroux, Anca Muscholl, Grégoire Sutre (LaBRI, Université Bordeaux, CNRS)

Repas
jeudi 11 mars 14h-15h30

Session 7 : Action IDM

Présidente de session : Mireille Blay-Fornarino

Meta-model Pruning
Sagar Sen (IRISA/INRIA Rennes Bretagne Atlantique),
Naouel Moha (IRISA/Université de Rennes1),
Benoit Baudry(IRISA/INRIA Rennes Bretagne Atlantique),
Jean-Marc Jézéquel (IRISA/Université de Rennes1)

Modeling Modeling
Pierre-Alain Muller, Frédéric Fondement (Université de Haute-Alsace)
Benoît Baudry (INRIA Rennes Bretagne Atlantique)

Retours sur l'école de printemps Model-Driven Development for Distributed Realtime Embedded Systems
Jean-Philippe Babau (Université de Brest),
Sylvain Robert  (CEA)


Session 8 : GT  LAMHA

Président de session : Frédéric Loulergue

OC4MC: Objective Caml for Multicore Architectures
Mathias Bourgoin, Benjamin Canou, Emmanuel Chailloux, Adrien Jonquet, Philippe Wang  (LIP6)

New Implementation of a BSP Composition Primitive with Application to the Implementation of Algorithmic Skeletons
Frédéric Gava, Ilias Garnier (LACL, UPEC)

A Scalable Parallel Algorithm for Join Queries Evaluation on Heterogeneous Distributed Systems
Mohamad Al Hajj Hassan, Mostafa Bamha (LIFO, Université d'Orléans)
Pause café et posters
jeudi 11 mars 16h-18h00

2e session défis pour le Génie de la Programmation et du Logiciel

et table ronde animée par Laurence Duchien (LIFL) avec Bertrand Braunschweig (ANR)

End-User Modelling
Patrick Albert, Mireille Blay-Fornarino, Benoît Combemale, Sophie Dupuy-Chessa and Xavier Le Pallec.

Towards Disappearing Languages
Charles Consel

Vers une réification de l'énergie dans le domaine du logiciel
Jean-Marc Menaud, Adrien Lèbre, Thomas Ledoux, Jacques Noyé, Pierre Cointe, Rémi Douence and Mario Südholt.
jeudi 11 mars 18h00-19h00 Réunion des comités
vendredi 12 mars 9h-10h30

Session 9 : GT  LTP

Présidente de session : Catherine Dubois

Types Abstraits et Types Existentiels Ouverts
Benoît Montagu, Didier Rémy (INRIA Paris-Rocquencourt)

Lucy-n : une extension n-synchrone de Lustre
Louis Mandel, Florence Plateau, Marc Pouzet (Université Paris-Sud 11)

A3PAT, an Approach for Certified Automated Termination Proofs
Évelyne Contejean, (LRI/CNRS/UPS)
Pierre Courtieu, (Cédric/CNAM)
Julien Forest, (Cédric/ENSIIE)
Andrei Paskevich, (LRI/UPS)
Olivier Pons, (Cédric/CNAM)
Xavier Urbain (LRI/ENSIIE)

Session 10 : GT AFSEC

Présidente de session : Christel Seguin

Compilation modulaire des programmes synchrones flot de données: une représentation symbolique efficace
Marc Pouzet (Université Paris-Sud 11, LRI)
Pascal Raymond, (VERIMAG)

Collaboration entre méthode d'ordonnancement et calcul réseau
Marc Boyer, David Doose (ONERA)

Analyse des délais de bout en bout pire cas dans des réseaux avioniques
J.-L. Scharbarg, J. Ermont, H. Bauer, C. Fraboul (Université de Toulouse IRIT/ENSEEIHT-INPT)


Pause café et posters
vendredi 12 mars 11h-12h30 Conférencier invité :

Gérard Berry, directeur de recherche à l'INRIA, titulaire de la chaire « Informatique et sciences numériques » au Collège de France et membre de l'Académie des Sciences.
vendredi 12 mars 12h30 Cloture : proclamation du meilleur poster
vendredi 12 mars 12h35
Repas

 

Journées Nationales du GDR GPL : résumés des présentations

Conférenciers Invités

A Classification Framework for Component Models

Ivica Crnkovic, Université de Mälardalen (Suède)

The essence of component-based software engineering is embodied in component models. Component models specify the properties of components and the mechanisms of component interactions. In the last decade a large number of different component models have been developed, with different aims and using different principles and technologies. This has resulted in a number of models which have many similarities, but also principal differences, and in many cases unclear concepts. Component-based development has not succeeded in providing standard principles, as has, for example, object-oriented development. In order to increase the understanding of the concepts, and to differentiate component models more easily, this presentation discusses fundamental principles of component models, and  defines a Component Model Classification Framework which includes these principles. Further,  the principles of several component models are presented using this framework.

Combiner Java et réécriture, c'est possible et utile

Pierre-Etienne Moreau , professeur à l'Ecole des Mines de Nancy , membre du LORIA /INRIA

Le système Tom (http://tom.loria.fr) est une extension de Java permettant de programmer par filtrage, en utilisant des règles et des stratégies. La notion de signature et de terme algébrique permet de définir de manière abstraite les structures de données. Dans ce cadre, l'utilisation de règles de réécriture et de motifs permet de définir, de manière élégante et sûre, des transformations à effectuer. Tom permet donc de programmer aussi bien en Java que par réécriture. Ce qui se prête particulièrement bien à l'enseignement et à la transformation de structures arborescentes telles que les termes ou les documents XML par exemple. Une des particularités du système est de fournir du filtrage modulo l'associativité avec élément neutre. Cette théorie permet de manipuler aisément des structures de liste par exemple. Une autre originalité de Tom est de ne pas imposer de structure de donnée particulière pour représenter les informations à transformer. Le lien entre la structure concrète et le signature algébrique devient un paramètre du programme. Cette souplesse permet d'utiliser la notion de filtrage algébrique pour effectuer des transformations de graphes par exemple. Enfin, la notion de stratégie est un moyen efficace et élégant pour contrôler la façon dont les transformations sont appliquées. L'exposé présentera le système Tom, ses particularités et ses applications.

Qualité du logiciel : certification vs. vérification

Gérard Berry, directeur de recherche à l'INRIA, titulaire de la chaire « Informatique et sciences numériques » au Collège de France et membre de l'Académie des Sciences.

La certification est un processus classique pour certains systèmes embarqués critiques (avionique, carte à puce, etc.); elle est certainement amenée à se généraliser. Elle se fonde encore essentiellement sur une analyse et une revue du flot de développement et de test. Cette approche reste indispensable, car tout programme mal développé et testé est évidemment dangereux. Mais, avec l'évolution vers un outillage de haut niveau avec synthèse de code embarqué et vérification formelle, d'autres approches plus scientifiques deviennent indispensables. Elles doivent être fondées sur des techniques réellement formelles et réellement implémentées. Nous étudierons l'état de ces techniques, leur évolution potentielle, leurs limites, et leur impact indirect sur les méthodes de conception.

Session 1 : GT MTV2

Exploration aléatoire de modèles
Johan Oudinet (LRI, Univ. Paris-Sud - CNRS)

Cet article présente des méthodes d’explorations probabilistes qui garantissent une bonne couverture des chemins du modèle quelle que soit sa topologie. Ces méthodes sont basées sur des techniques de comptage et de tirage uniforme de structures combinatoires qui dans leurs versions de bases sont très coûteuses en espace mémoire. Ce papier présente des améliorations qui permettent d’explorer uniformément des modèles plus gros en tirant des chemins plus longs. Une étude de la complexité binaire, accompagnée de résultats expérimentaux de chacune des variantes possibles permet de décider quelle variante utiliser en fonction de la taille du modèle, des longueurs de chemins désirées et des ressources disponibles.



Détection de Vulnérabilités Logicielles par le Test Passif
Amel Mammar, Ana Cavalli, Willy Jimenez ( Telecom SudParis)
Edgardo Montes de Oca  (Montimage)
Shanai Ardi, David Byers, Nahid Shahmehri (Linköpings universitet)

L'utilisation de modélisations formelles est devenue une partie intégrante du processus de développement de logiciels sûrs. En effet, une bonne modélisation du système à développer permet d'améliorer la qualité des logiciels en détectant, par exemple, certaines vulnérabilités avant même leurs déploiements. Dans cette optique, on propose une nouvelle méthode de modélisation de vulnérabilités ainsi qu'un langage formel pour l'expression précise sans ambiguïté des causes et événements pouvant les produire. La définition d'un tel langage formel permet également la détection automatique des vulnérabilités par des outils de test. Plus précisément, nous illustrons l'utilisation de l'outil de test passif TestInv, développé au sein de notre équipe, pour la détection automatique de vulnérabilités exprimées dans le langage formel ainsi défini. Notre approche a l'avantage de produire un nombre beaucoup plus réduit de faux positifs tout en maintenant à jour la base de connaissances de l'outil TestInv. L'approche proposée est illustrée à travers l'exemple de vulnérabilité CVE-2005-3192 représentant un ``buffer overflow" dans un programme C.

Combining Frama-C and PathCrawler for C Program Debugging
Omar Chebaro (CEA/LIST, LIFC),
Nikolai Kosmatov (CEA/LIST),
Alain Giorgetti (LIFC, INRIA),
Jacques Julliand (LIFC)

Session 2 : GT Transformations

Machine-Checked Sequencer for Critical Embedded Code Generator
Nassima Izerrouken, (Continental Automotive, et Université de Toulouse, IRIT-ENSEEIHT)
Marc Pantel, Xavier Thirioux (Université de Toulouse, IRIT-ENSEEIHT)

This paper presents the development of a correct-by-construction block sequencer for GENEAUTO a qualifiable (according to DO178B/ED12B recommendation) automatic code generator. It transforms SIMULINK models to MISRA C code for safety critical systems. Our approach which combines classical development process and formal specification and verification using proof-assistants, led to preliminary fruitful exchanges with certification authorities. We present parts of the classical user and tools requirements and derived formal specifications, implementation and verification for the correctness and termination of the block sequencer. This sequencer has been successfully applied to real-size industrial use cases from various transportation domain partners and led to requirement errors detection and a correct-by-construction implementation.

Les plates-formes d'exécution dans l'IDM : Quelles modélisations pour quelles utilisations ?
Jérôme Delatour, Matthias Brun, Guillaume Savaton, Jonathan Ilias-Pillet, Cédrick Lelionnais (Groupe ESEO)

L’un des objectifs de l'Ingénierie Dirigée par les Modèles (IDM) est de mettre en œuvre un même modèle de fonctionnalités sur différents supports technologiques, ces derniers sont souvent désignés comme des plates-formes d'exécution. Toutefois, peu de travaux ont été menés, à la fois pour préciser comment modéliser ces plates-formes et comment les mettre en œuvre dans des transformations. L'objectif de cette présentation est de proposer des éléments de réponse à ces questions.

+ 2 exposés jeunes chercheurs


Session 3 : GT RIMEL

Une architecture de composants répartis adaptables
An Phung-Khac, Jean-Marie Gilliot et Maria-Teresa Segarra (TELECOM Bretagne)

Plusieurs travaux récents proposent des solutions ou des frameworks dédiés au développement d’applications adaptables qui peuvent ainsi dynamiquement changer leur comportement pendant l’exécution afin de s’adapter au contexte d’exécution courant. Cependant, avec ces approches, les tâches à la charge des développeurs sont encore complexes. Ces tâches incluent la définition des variantes et la spécification des actions d’adaptation, qui dans le contexte des systèmes répartis, incluent des contraintes liées aux parties distribuées. Dans cet article, nous présentons une approche de développement d’applications réparties adaptables permettant la génération correcte des variantes d’une application et des actions d’adaptation à exécuter en vue de faciliter la tâche des développeurs.


OCL contracts for the verification of model transformations
Eric Cariou, Nicolas Belloir, Franck Barbier, Nidal Djemam (Université de Pau et des Pays de l’Adour / Liuppa)

A model-driven engineering process relies on a set of transformations which are usually sequentially executed, starting from an abstract level to produce code or a detailed implementation specification. These transformations may be entirely automated or may require manual intervention by designers. In this paper, we propose a method to verify that a transformation result is correct with respect to the transformation specification. This method both includes automated transformations and manual interventions. For that, we focus on transformation contracts written in OCL. This leads to making the proposed method independent of modeling and transformation tools. These contracts are partially or fully generated through a dedicated tool.

Session 4 : GT MFDL

Application du Model Checking aux commandes de vol : l’expérience Airbus
Thomas Bochot (AIRBUS & ONERA/DTIM), Pierre Virelizier (AIRBUS), Hélène Waeselynck (LAAS-CNRS), Virginie Wiels (ONERA/DTIM)

Cet article présente des études réalisées par Airbus sur l’utilisation du model checking pour la vérification de systèmes critiques, les leçons que l’on peut en tirer et les moyens pour étendre l’utilisation industrielle de la vérification formelle au niveau modèle.

Définition d’une sémantique Event-B pour les patrons de raffinement de buts KAOS
Abderrahman Matoussi, Frédéric Gervais et Régine Laleau (LACL, UPEC)

Tandis que les spécifications répondent à la question « que fait le système ? », les buts résolvent quant à eux les questions « qui ? quand ? comment ? ». Ainsi, les buts jouent un rôle très important dans l’ingénierie des besoins et par conséquent dans le développement logiciel. Néanmoins, le processus de développement associé aux méthodes formelles marginalise la phase d’analyse des besoins. En effet, ce processus ne commence qu’à partir de la phase de spécification. Par conséquent, le fossé entre ces deux phases s’élargit et la réconciliation paraît de plus en plus difficile. L’objectif de cet article est d’inclure la phase d’analyse des besoins et plus précisément la méthodologie KAOS dans le développement logiciel associé aux méthodes formelles tout en restant au même niveau d’abstraction. Pour cela, nous proposons une approche constructive dans laquelle les modèles Event-B sont construits d’une manière incrémentale à partir des modèles de buts KAOS en se basant sur les patrons de raffinement de buts. Nous justifions le choix d’Event-B par : (i) la possibilité d’utiliser la méthode durant tout le processus de développement logiciel ; (ii) la maturité des outils qui supportent la notation Event-B.

Session 5 : GT COSMAL

Matrice de dépendances enrichie
Jannik Laval, Alexandre Bergel, Stéphane Ducasse, Romain Piers (INRIA - Lille Nord Europe - USTL - CNRS UMR 8022)

Les matrices de dépendance (DSM - Dependency Structure Matrix), développées dans le cadre de l’optimisation de processus, ont fait leurs preuves pour identifier les dépendances logicielles entre des packages ou des sous-systèmes. Il existe plusieurs algorithmes pour structurer une matrice de façon à ce qu’elle reflète l’architecture des éléments analysés et mette en évidence des cycles entre les sous-systèmes. Cependant, les implémentations de matrices de dépendance existantes manquent d’informations importantes pour apporter une réelle aide au travail de réingénierie. Par exemple, le poids des relations qui posent problème ainsi que leur type ne sont pas clairement présentés. Ou encore, des cycles indépendants sont fusionnés. Il est également difficile d’obtenir une visualisation centrée sur un package. Dans ce papier, nous améliorons les matrices de dépendance en ajoutant des informations sur (i) le type de références, (ii) le nombre d’entités référençantes, (iii) le nombre d’entités référencées. Nous distinguons également les cycles indépendants. Ce travail a été implémenté dans l’environnement de réingénierie open-source Moose. Il a été appliqué à des études de cas complexes comme le framework Morphic UI contenu dans les environnements Smalltalk open-source Squeak et Pharo. Les résultats obtenus ont été appliqués dans l’environnement de programmation Pharo et ont mené à des améliorations.

Évaluation de l'efficacité des implémentations de l'héritage multiple en typage statique.
Floréal Morandat, Roland Ducournau (LIRMM)
Jean Privat {Université du Québec à Montréal)

La programmation par objets présente une apparente incompatibilité entre trois termes : l'héritage multiple, l'efficacité et l'hypothèse du monde ouvert -- en particulier, le chargement dynamique. Cet article présente des résultats d'expérimentations exhaustives comparant l'efficacité de différentes techniques d'implémentation (coloration, BTD, hachage parfait, ...) dans le contexte de différents schémas de compilation (de la compilation séparée avec chargement dynamique à la compilation purement globale). Les tests sont effectués avec et sur le compilateur du langage Prm. Ils confirment pour l'essentiel les résultats théoriques antérieurs. Les schémas d'optimisation globale démontrent un gain significatif par rapport à la coloration qui fait fonction de référence, tandis que le chargement dynamique rend réel le surcoût de l'héritage multiple. Enfin, ces tests confirment l'intérêt du hachage parfait pour les interfaces de Java.

Correction d'assemblages de composants impliquant des données et assertions
Mohamed Messabihi, Pascal André et Christian Attiogbé (LINA)

La démarche de construction du logiciel en partant de l'architecture, nécessite la prise en compte de la correction à différentes étapes afin d'assurer la qualité du logiciel final. Ainsi la correction est une préoccupation qui doit être prise en compte au niveau des composants et de leurs assemblages pour élaborer l'architecture logicielle. Kmelia est un langage et un modèle à composants multi-service où les composants sont abstraits et formels de façon à pouvoir y exprimer des propriétés et les vérifier. Les services de Kmelia peuvent êtres paramétrés par des données et sont dotés d'assertions (pré/post-conditions opérant sur les données). Dans cet article nous nous intéressons à la correction des modèles à composants en couvrant différents aspects: la correction au niveau des services et la correction des assemblages du point de vue des données présentes dans les interfaces des services. Nous présentons les enrichissements du langage de données de Kmelia permettant de traiter la correction au niveau des services et de l'architecture. Nous illustrons l'étude par un exemple.



Session 6 : GT FORWAL

On-the-fly Emptiness Check of Transition-Based Streett Automata
Alexandre Duret-Lutz, Denis Poitrenaud, Jean-Michel Couvreur

Reachability Analysis of Communicating Pushdown Automata
Alexander Heußner, Jérôme Leroux, Anca Muscholl, Grégoire Sutre (LaBRI, Université Bordeaux, CNRS)

We propose restrictions for the reachability analysis of recursive programs that communicate asynchronously over reliable fifo channels in order to assure decidability. Our proposed model extends the model of communicating pushdown systems of [La Torre et al.,TACAS08], that permits to dequeue with empty stack only, by the dual condition. Hence, we can model both event based and interrupt based process models. We study the conservation of the decidability of reachability when adding pushdowns to a setting of (possibly cyclic) network architectures that ensure the decidability of reachability for finite state systems under a semantic assumption. In the positive case, we obtain exponential time as the exact complexity bound. A second result generalizes the doubly exponential time algorithm of [La Torre et al.] for bounded context analysis to our symmetric queueing policy by providing a direct (and simpler) algorithm.



Session 7 : Action IDM

Meta-model Pruning
Sagar Sen (IRISA/INRIA Rennes Bretagne Atlantique),
Naouel Moha (IRISA/Université de Rennes1),
Benoit Baudry(IRISA/INRIA Rennes Bretagne Atlantique),
Jean-Marc Jézéquel (IRISA/Université de Rennes1)

Large and complex meta-models such as those of Uml and its profiles are growing due to modelling and inter-operability needs of numerous stakeholders. The complexity of such meta-models has led to coining of the term meta-muddle. Individual users often exercise only a small view of a meta-muddle for tasks ranging from model creation to construction of model transformations. What is the effective meta-model that represents this view? We present a flexible meta-model pruning algorithm and tool to extract effective meta-models from a meta-muddle. We use the notion of model typing for meta-models to verify that the algorithm generates a super-type of the large meta-model representing the meta-muddle. This implies that all programs written using the effective meta-model will work for the meta-muddle hence preserving backward compatibility. All instances of the effective meta-model are also instances of the meta-muddle. We illustrate how pruning the original Uml metamodel produces different effective meta-models.

Modeling Modeling
Pierre-Alain Muller, Frédéric Fondement (Université de Haute-Alsace)
Benoît Baudry (INRIA Rennes Bretagne Atlantique)

Retours sur l'école de printemps Model-Driven Development for Distributed Realtime Embedded Systems
Jean-Philippe Babau (Université de Brest),
Sylvain Robert  (CEA)

Cette année du 20 au 24 avril s'est tenue à Aussois la 4ième école internationale de printemps MDD4RES. Elle a été l'occasion de présenter les contributions académiques et industrielles aussi bien en terme d'avancées en ingénierie des modèles (modéles et langages, tests de transformations, analyse de performances...) que des standards adoptés (UML Marte, Autosar). Cet exposé donnera un aperçu de ce programme.


Session 8 : GT LAMHA

OC4MC: Objective Caml for Multicore Architectures
Mathias Bourgoin, Benjamin Canou, Emmanuel Chailloux, Adrien Jonquet, Philippe Wang Affiliation (LIP6)

OCaml est un langage multiparadigme de haut niveau connu pour ses performances. Cependant, sa bibliothèque d'exécution a été conçue pour être performante sur des architectures mono-processeur mono-coeur. Leur gestion des co-processus ne permet pas de profiter des nouveaux processeurs (grand public) multi-coeurs (fonctionnant sur le modèle "SMP"). OC4MC est un projet montrant la faisabilité de la réalisation d'une bibliothèque d'exécution alternative permettant de profiter de ces processeurs multi-coeurs avec le modèle des co-processus communiquant par mémoire partagée.

New Implementation of a BSP Composition Primitive with Application to the Implementation of Algorithmic Skeletons
Frédéric Gava, Ilias Garnier (LACL, UPEC)

A Scalable Parallel Algorithm for Join Queries Evaluation on Heterogeneous Distributed Systems
Mohamad Al Hajj Hassan, Mostafa Bamha (LIFO, Université d'Orléans)

Owing to the fast development of network technologies, executing parallel programs on distributed systems that connect heterogeneous machines became feasible but we still face some challenges: Workload imbalance in such environment may not only be due to uneven load distribution among machines as in parallel systems but also due to distribution that is not adequate with the characteristics of each machine. In this paper, we present a scalable parallel join algorithm called DFA-Join (Dynamic Frequency Adaptive Join) for heterogeneous distributed architectures based on an efficient dynamic data distribution and task allocation which makes it insensitive to data skew and ensures perfect balancing properties during all stages of join computation. The performance of this algorithm is analyzed using the scalable and portable BSP (Bulk Synchronous Parallel) cost model. We show that DFA-Join algorithm guarantees optimal complexity and near linear speed-up while reducing communication and disk input/output costs to a minimum. These results are confirmed by a series of tests.


Session 9 : GT LTP

Types Abstraits et Types Existentiels Ouverts
Benoît Montagu, Didier Rémy (INRIA Paris-Rocquencourt)

Les types abstraits ont été initialement expliqués par l'emploi de types existentiels. Nous verrons que ceux-ci ne peuvent être utilisés facilement en pratique, et peuvent avantageusement être remplacés par des types existentiels ouverts.

Lucy-n : une extension n-synchrone de Lustre
Louis Mandel, Florence Plateau, Marc Pouzet (Université Paris-Sud 11)

Les langages synchrones flot de données permettent la programmation de réseaux de processus communicant sans buffers. Pour cela, chaque flot est associé à un type d'horloges, qui indique les instants de présence de valeurs sur le flot. La communication entre deux processus f et g peut être faite sans buffer si le type du flot de sortie de f est égal au type du flot d'entrée de g. Un système de types, le calcul d'horloge, infère des types tels que cette condition est vérifiée. Le modèle n-synchrone relâche ce modèle de programmation en autorisant les communications à travers des buffers de taille bornée. En pratique, cela consiste à introduire une règle de sous-typage dans le calcul d'horloge.

Nous présentons un langage de programmation n-synchrone : Lucy-n. Dans ce langage, l'inférence des types d'horloges est paramétré par l'algorithme de résolution des contraintes de sous-typage. Nous décrivons un des algorithmes existant et comment programmer en Lucy-n à travers l'exemple d'une application de traitement multimédia.


A3PAT, an Approach for Certified Automated Termination Proofs
Évelyne Contejean, (LRI/CNRS/UPS)
Pierre Courtieu, (Cédric/CNAM)
Julien Forest, (Cédric/ENSIIE)
Andrei Paskevich, (LRI/UPS)
Olivier Pons, (Cédric/CNAM)
Xavier Urbain (LRI/ENSIIE)

En génie logiciel, démonstration automatique, spécifications ou programmation par règles, il est courant d'utiliser des systèmes de récriture pour lesquels la terminaison, entre autres propriétés, doit être établie.
Nous présentons l'approche développée au sein du projet A3PAT pour non seulement trouver mais aussi certifier formellement, de façon complètement automatique, des preuves de terminaison de systèmes de récriture du premier ordre.
Cette approche repose sur deux développements logiciels : la bibliothèque Coccinelle formalisant pour l'assistant de preuve Coq de nombreux critères et techniques de terminaison ; la boîte à outils de récriture CiME3 transformant des traces de preuves de terminaison (provenant de CiME3 lui-même ou d'autres prouveurs) en scripts pour Coq qui les compilera à l'aide de Coccinelle pour obtenir la certification.
Un des bénéfices de la modélisation formelle est de nous permettre d'affaiblir sensiblement les prémisses de certains théorèmes de la littérature. Nous obtenons ainsi de nouveaux critères, comme l'extension du puissant critère dit de « sous-terme » (pour lequel nous proposons la première formalisation Coq complète). Nous proposons également des techniques alternatives, améliorant nos travaux antérieurs sur la formalisation et l'analyse des graphes de dépendance.

Session 10 : GT AFSEC

Compilation modulaire des programmes synchrones flot de données: une représentation symbolique efficace
Marc Pouzet (Université Paris-Sud 11, LRI)
Pascal Raymond, (VERIMAG)

Cet article considère le problème de génération modulaire de code séquentiel à partir d'un programme synchrone flot de données. Précisément, étant donné un système à plusieurs entrées et plusieurs sorties, comment le décomposer en un nombre minimal de classes exécutées atomiquement et ordonnées statiquement sans contraindre les rebouclages possibles entre entrées/sorties ? Bien qu'identifié par Raymond au début de Lustre, cette question est restée peu abordée jusqu'aux travaux récents de Lublinerman, Szegedy and Tripakis. Les auteurs montrent que le problème est NP-complet puisqu'il s'agit d'un problème d'optimisation reposant sur la décision --- il existe une solution avec c classes --- elle-même NP-complète. A partir de ce résultat, les auteurs en déduisent un algorithme itératif en recherchant une solution pour c = 1, 2,... classes, chaque étape étant ramenée à un problème SAT. Malgré la complexité théorique du problème, la complexité effective semble beaucoup plus faible. Dans cet article, nous proposons une nouvelle représentation symbolique du problème à partir des relations entre entrées/sorties dans le reséau et reprenant ainsi les premiers résultats de Raymond. Cet encodage simplifie le problème dans la mesure où il contient moins de solutions tout en gardant les solutions optimales. Il permet, en temps polynomial, (1) d'identifier les noeuds pour lequels plusieurs ordonnancements sont possibles conduisant ainsi à une éventuelle explosion combinatoire; (2) d'obtenir directement des solutions optimales dans certains cas; (3) sinon, de fournir une borne minimale non triviale de c pour démarrer une recherche itérative. La solution proposée s'applique à de nombreux formalismes ou langages de type ``schéma/bloc'' formés d'opérateurs atomiques et d'un opérateur de délais. Elle s'applique, en particulier, à des langages de programmation synchrones tels que Lustre, Scade ou Signal ainsi qu'à des outils de modélisation/simulation tels que Simulink.

Collaboration entre méthode d'ordonnancement et calcul réseau
Marc Boyer, David Doose (ONERA)
Dans cet article, nous faisons collaborer deux méthodes de calcul du monde temps réel: l'ordonnancement de tâches et le calcul réseau. L'ordonnancement de tâches cherche à savoir si, sur un processeur partagé, un ensemble de tâches (temps-réel) respectera ses échéances. Les différentes techniques d'ordonnancement peuvent souvent trouver exactement le pire temps de réponse, mais avec une complexité algorithmique assez importante. Le calcul réseau, lui, fait souvent des sur-approximations, mais avec une complexité algorithmique plus faible (souvent linéaire) qui lui permet de traiter des systèmes de très grande taille. Nous nous proposons ici de faire collaborer es deux techniques dans un système embarqué communiquant en appliquant l'ordonnancement dans les calculateurs pour évaluer au plus près le flots de données qui en est issu dans un format adapté au calcul réseau.

Analyse des délais de bout en bout pire cas dans des réseaux avioniques
J.-L. Scharbarg, J. Ermont, H. Bauer, C. Fraboul (Université de Toulouse IRIT/ENSEEIHT-INPT)

L’AFDX (Avionics Full DupleX) est un réseau avionique qui permet le multiplexage de flux de communication sur un réseau Ethernet commuté full duplex. La standardisation de ce réseau dans le cadre de la la norme ARINC 664 en a fait la technologie de de communication de référence pour l’avionique civile. Cette technologie élimine l’indétermisme lié aux collisions dans les réseaux Ethernet de base. Cependant, l’indéterminisme est présent au niveau des commutateurs, où différents flux partagent des ressources (politique de service FIFO au niveau des ports de sortie des commutateurs). Pour maîtriser cet indéterminisme, le standard AFDX impose des contraintes, en particulier au niveau de la définition des flux : chaque flux est défini statiquement et son débit doit être borné (rafale, débit moyen). La certification du réseau, indispensable dans le domaine de l’avionique, nécessite de prouver que le délai de communication de bout en bout est borné pour tout flux transmis sur le réseau. Pour l’A380, la certification s’est appuyée sur une approche fondée sur le calcul réseau. D’autres approches sont envisageables, utilisant en particulier la méthode des trajectoires et la vérification de modèles. L’objectif de cette présentation est de monter l’application des différentes méthodes envisageables pour l’analuse pire cas des déléais de bout en bout d’un réseau AFDX, puis de comparer les résultats qu’elles permettent d’obtenir sur une configuration AFDX industrielle.

Défis pour le Génie Logiciel et la Programmation

Software (re)modularization: Fight against the structure erosion and migration preparation
Nicolas Anquetil, Simon Denier, Stéphane Ducasse, Jannik Laval, Damien Pollet, Roland Ducournau, Rodolphe Giroudeau, Marianne Huchard, Jean-Claude Konig and Abdelhak-Jamel Seriai

Software systems, and in particular, Object-Oriented systems are models of the real world that manipulate representations of its entities through models of its processes. The real world is not static: new laws are created, concurrents offer new functionalities,users have renewed expectation toward what a computer should offer them, memory constraints are added, etc. As a result, software systems must be continuously updated or face the risk of becoming gradually out-dated and irrelevant. This is a main issue in software maintenance which has a high cost for software companies. We explain why the existing solutions have failed to solve this problem and which tracks of research should be followed to address the challenge. In particular, we propose to combine different approaches based on graph theory, lattice theory, visualization, metrics and to introduce the expert in the heart of the approach.

Component and Service Farms: Towards folkregistries
Gabriela Arévalo, Zeina Azmeh, Marianne Huchard, Chouki Tibermacine, Christelle Urtado and Sylvain Vauttier



End-User Modelling
Patrick Albert, Mireille Blay-Fornarino, Benoît Combemale, Sophie Dupuy-Chessa and Xavier Le Pallec.
L'implication de plus en plus forte des utilisateurs finaux dans les processus de développement (e.g., méthodes agiles) montre un impact positif dans la réussite et la qualité des projets informatiques. D'autre part, l'introduction massive des nouvelles technologies dans la vie de tous les jours et la diversité des domaines d'applications amènent de plus en plus d'experts métiers voir des utilisateurs finaux à s'intéresser aux environnements de développement. Pour cela, nous proposons comme défi pour le Génie de la Programmation et du Logiciel à échéance de 2020, la définition des moyens de développement qui permettent une implication plus forte, plus active et plus formelle des experts et des utilisateurs finaux dans la construction et l'évolution de leur système informatique. Pour relever ce défi, nous développons une approche basée sur les modèles dont les fondements visent i) l'abstraction nécessaire pour être destinée aux utilisateurs finaux, par l'utilisation de langages dédiés, ii) la prise en compte les différentes préoccupations d'un même système, et iii) la capacité à s'appuyer sur des fondations formelles assurant un certain niveau de fiabilité des systèmes.

Towards Disappearing Languages
Charles Consel
This paper explores challenges that need to be addressed to make the domain- specific language (DSL) approach successful. In particular, we argue that a DSL should be blended with a domain process and used by domain experts in support of their job. We call such languages disappearing.

Vers une réification de l'énergie dans le domaine du logiciel
Jean-Marc Menaud, Adrien Lèbre, Thomas Ledoux, Jacques Noyé, Pierre Cointe, Rémi Douence and Mario Südholt.
En quelques années, le problème de la gestion de l'énergie est devenu un enjeu de société. En informatique, les principaux travaux se sont concentrés sur des mécanismes permettant de maîtriser l'énergie au niveau du matériel. Le renforcement du rôle de l'informatique dans notre société (développement des centres de données, prolifération des objets numériques du quotidien) conduit à traiter ces problèmes aussi au niveau du logiciel. Dans ce papier, nous nous posons la question de la réification de l'énergie comme fut posée en son temps celle de la réification de la mémoire (l'espace) et de l'interpréteur (la machine d'exécution). Le défi est d'abord de sensibiliser l'utilisateur final au problème de la consommation énergétique en lui offrant des mécanismes d'introspection visualisant la ressource énergie à l'image de ce qui se fait aujourd'hui dans le domaine automobile (consommation d'essence). Il s'agira ensuite de proposer des mécanismes d'intercession aux développeurs aptes à contrôler cette consommation énergétique. Ces mécanismes réflexifs devront concerner l'ensemble du cycle de vie du logiciel.

Table ronde : le Génie de la Programmation et du Logiciel à échéance de 2020
Animée par Laurence Duchien
L'omniprésence de l'informatique dans notre quotidien à l'échelle de l'embarqué et de l'intelligence ambiante, l'extension du web au niveau de la planète, mais également dans les objets du quotidien, le développement de grandes infrastructures de calcul ou des centres de traitement de grandes masses de données soulèvent de nombreuses questions pour le génie de la programmation et du logiciel. Parmi ces questions, quelles sont celles qui correspondent à des défis que devront relever les chercheurs dans le domaine du génie de la programmation et du logiciel à échéance de 5 à 10 ans ? De nouveaux paradigmes, de nouveaux langages, de nouvelles approches de modélisation, de vérification, de tests et de nouveaux outils dans le domaine de la programmation et du logiciel devraient voir le jour dans les 5 à 10 ans à venir, que ce soit pour faciliter la vie des concepteurs de logiciel, pour modéliser et fiabiliser les logiciels ou encore pour devancer l'évolution technologique, mais également pour prendre en compte de nouveaux enjeux de société tels que le développement durable et les économies d’énergie. Les cinq défis seront présentés lors de deux sessions. Ils portent sur la (re)modularisation du logiciel, la mise en place de fermes de composants et de services, l’évaporation des langages, la modélisation pour l’utilisateur final et la réification de l'énergie au niveau des systèmes et des langages. Une table ronde permettra ensuite de débattre de ces sujets. Lors de cette table ronde, Bertrand Braunschweig fera le point sur la perception de notre domaine au sein de l’ANR.

Posters et Démos


Alexandre Cortier. Projet SPaCIFY : Ingénierie des modèles et Méthodes Formelles pour les systèmes embarqués critiques (Poster)

François Fages and Martin Julien. Modelling Search Strategies in Rules2CP (Poster et Démo)

Arnaud Gotlieb. EUclide is a Constraint Language based on Imperative DEfinitions(Poster et Démo)

Nassima Izerrouken, Marc Pantel and Xavier Thirioux. Integrated Formal Approach for a Qualified Critical Code Generator (Poster)

Nour Alhouda Aboud, Philippe Aniorté, Eric Cariou and Eric Gouarderes. Integration of Agent and Component approaches by Service Oriented vision using Model Driven Engineering (Poster)

Sabina Akhtar, Stephan Merz and Martin Quinson. Extending PlusCal: A Language for Describing Concurrent and Distributed Algorithms (Poster)

Vincent Aranega. Traceability Mechanism in Transformations Chains Dedicated to Model and Transformation Debugging (Poster)

Iyad Alshabani, Joyce El Haddad, Nikolaos Georgantas, Tarek Melliti, Lynda Mokdad and Pascal Poizat. Pervasive Service Composition (Projet ANR PERSO) (Poster)

Thanh Thanh Le Thi. L’Activité de Génération de Codes Dirigée par les Modèles (Poster)

Fatiha Zaidi, Richard Castanet, Ana Cavalli, Edgardo Montes de Oca and Andrey Sadovykh. WebMov : Modélisation, Test de la composition de services Web (Poster)

Youssef Ridene, Franck Barbier, Nicolas Belloir and Nadine Couture. Définition d'un langage de modélisation spécifique (Domain Specific Modeling Language) au test d'applications embarquées sur téléphones mobiles (Poster)

Sebastien Mosser and Mireille Blay-Fornarino. Taming Orchestration Design Complexity through the ADORE Framework (Poster et Démo)

Regine Laleau. Projet ANR SELKIS (Poster)

Akram Idani, Mohamed Amine Labiadh and Yves Ledru. Approche orientée modèles pour une intégration efficace de B et UML (Poster)

Peggy Cellier, Mireille Ducassé, Sébastien Ferré and Olivier Ridoux. Fouille de données pour la localisation de fautes dans les programmes (Poster)

Romain Adeline, Janette Cardoso, Christel Seguin, Pierre Darfeuil and Sophie Humbert. Vers une méthode de validation des modèles formels AltaRica (Poster)


Mise à jour le Dimanche, 23 Janvier 2011 16:14