Programme général de Lille 2011 : CAL, IDM, COSMAL et GDR GPL

Programmes : Général Court CAL COSMAL GDR GPL IDM

• Programme du Mardi 7 juin (CAL, IDM )
• Programme du Mercredi 8 juin (CAL, IDM, GDR GPL )
• Programme du Jeudi 9 juin (GDR GPL )
• Programme du Vendredi 10 juin (GDR GPL, COSMAL )

• Conférenciers invité de la semaine
• Articles et auteurs
• Posters et démos du GDR GPL

Versions imprimables du programme de la semaine :

• Version HTML
• Version PDF (une impression papier de ce programme sera distribuée à chaque participant)

Mardi 7 juin

Revenir en haut de la page

Mercredi 8 juin

Revenir en haut de la page

Jeudi 9 juin

Revenir en haut de la page

Vendredi 10 juin

Revenir en haut de la page

Conférenciers invités

Cédric Fournet (web )

Modèles et outils pour la vérification de programmes utilisant la cryptographie

Didier Donsez

Vertus et vices de la plateforme dynamique de services OSGi

Résumé :

Ces derniers années, la technologie OSGi est devenu le standard de fait pour la modularisation et pour le déploiement des logiciels développés en Java. De nombreux logiciels patrimoniaux sont reconditionnés pour être livrable au moyen de cette plateforme. Cependant, plusieurs écueils sont rencontrés par les équipes de développement lors de ces migrations. Cette présentation présente les vertus de cette plateforme mais aussi ses « vices » qui sont généralement à la non-prise en compte de la nature dynamique de celle-ci.
Didier Donsez est professeur des universités à l'Université Joseph Fourier - Grenoble 1. Ses recherches actuelles portent sur l'ingénierie des logiciels reconfigurables à l'exécution tels que les intergiciels complexes et patrimoniaux ou bien l'informatique ambiante. Il a une dizaine d'années d'expérience du développement avec et pour la plateforme OSGi. Il contribue à plusieurs projets open source reliés à la technologie OSGi. Il enseigne à Polyetch'Grenoble, le génie logiciel et les technologies d'intergiciel pour les applications Web et l'EAI ainsi pour l'informatique ambiante.

Roberto di Cosmo (web )

Le défi des distributions de Logiciels Libres

Résumé :

Les distributions de logiciels libres, comme Debian, RedHat, ou Ubuntu, sont parmi les plus grands systemes a composants existants, basees sur les paquets, avec leurs metadonnees, avec une serie d'outils qui permettent d'ajouter ou enlever des composants selon le besoin des utilisateurs. Faire evoluer les distributions est une tache complexe qui pose des nombreux defis: dans cet expose, apres avoir donne une formalisation simple des distributions de logiciels libres, on passera en revue plusieurs resultats et algorithmes developpes ces dernieres annees pour repondre a des questions comme "quel composant est le plus important parmi les 27.000 de Debian squeeze?", ou "quel changement de version aura le plus d'impact sur le systeme?".

Tom Mens (web )

Analyse de l'évolution des aspects sociaux dans les projets logiciels

Résumé :

Le génie logiciel empirique s'intéresse aux études empiriques permettant de comprendre et d'améliorer certains aspects du processus logiciel. Nombre d'entre elles sont dédiées à l'évolution des projets logiciels. Elles extraient les données pertinentes venant de dépôts logiciels ou d'autres sources de données couramment utilisées par les développeurs. Nous suggérons d'élargir ce type d'études empiriques en tenant compte de l'information concernant les communautés de développeurs, ainsi que leur façon de travailler, d'interagir et de communiquer. L'hypothèse sous-jacente étant que les aspects sociaux influent significativement la qualité du produit logiciel, ainsi que la manière dont ce produit évolue au fil du temps. Dans cette conférence, nous présenterons un outil permettant d'extraire, de visualiser et d'analyser l'information concernant les communautés gravitant autour d'un projet logiciel. Nous montrerons quelques études empiriques effectuées avec cet outil, et nous ouvrirons des nouvelles pistes de recherche dans ce domaine de recherche combinant l'analyse des réseaux sociaux et le génie logiciel empirique.

Articles

CAL

• Mardi 7 juin, 9h00-10h30, Amphi Lebon
   Peio Loubière, Florent Devin, Yannick Le Nir
   Evolution générique d'une application web spécifique
• Mardi 7 juin, 9h00-10h30, Amphi Lebon
   Sonia Yassa, Hubert Kadima
   Négociation dynamique des services fondée sur le SLA dans un Cloud
• Mardi 7 juin, 14h00-15h30, Amphi Lebon
   Mariam Lahami, Moez Krichen and Mohamed Jmaiel
   A distributed Test Architecture For Adaptable and Distributed Real-Time Systems
• Mardi 7 juin, 16h00-17h30, Amphi Lebon
   Meriem Benhaddi, Karim Baïna and El Hassan Abdelwahed
   Alignement du Mashuping et des techniques d'orchestration des services
• Mardi 7 juin, 11h00-12h30, Amphi Lebon
   
   Evolution du principe de Réutilisation entre Objet, Composant, Services et Cloud Services
• Mardi 7 juin, 16h00-17h30, Amphi Lebon
   Anne-Lise Courbis, Thomas Lambolais, Hong-Viet Luong and Than-Liem Phan
   Analyse de l'interopérabilité et de la conformité d'architectures logicielles
• Mardi 7 juin, 14h00-15h30, Amphi Lebon
   Fadila Aoussat, Mourad Oussalah and Mohamed Ahmed Nacer
   Métamodélisation architecturale de procédés logiciels
• Mardi 7 juin, 14h00-15h30, Amphi Lebon
   Victor Noel and Jean-Paul Arcangeli
   Frameworks, architectures et composants : revisiter le développement de systèmes multi-agents
• Mardi 7 juin, 16h00-17h30, Amphi Lebon
   Emna Fki, Chantal Soulé Dupuy, Said Tazi and Mohamed Jmaiel
   Vers une composition de services basée sur les patrons de services et dirigée par les intentions
• Mardi 7 juin, 16h00-17h30, Amphi Lebon
   Nour Aboud, Eric Cariou and Eric Gouarderes
   Towards a Component Agent Service Oriented Model
• Mardi 7 juin, 9h00-10h30, Amphi Lebon
   Aziza Sabri, Laila Kjiri
   Vers une approche à base de composants pour la conception des systèmes d'informations décisionnels: existant et perspectives
• Mercredi 8 juin, 14h00-15h30, Amphi Lebon
   Rabah Mokhtari, Allaoua Chaoui and Mohamed Redha Bahri
   Transformation des architectures logicielles dynamiques vers des documents XML en utilisant ATOM3
• Mercredi 8 juin, 14h00-15h30, Amphi Lebon
   Suzy Temate, Alain Tchana, Laurent Broto and Daniel Hagimont
   Une approche de haut niveau pour générer des Editeurs Graphiques de Langage Dédiés
• Mercredi 8 juin, 9h00-10h30, Amphi Lebon
   Chouki Tibermacine and Mohamed Lamine Kerdoudi
   Migration d'applications à base de composants Web en services et orchestration de services Web
• Mercredi 8 juin, 9h00-10h30, Amphi Lebon
   Nadira Benlahrache, Faiza Belala and Kamel Barkaoui
   Description formelle du Déploiement d'Architectures AADL basée sur les Systèmes Réactifs Bigraphiques
• Mercredi 8 juin, 9h00-10h30, Amphi Lebon
   Mohamed Tahar Bhiri, Mourad Kmimech and Mohamed Graiet
   De Wright vers Ada
• Mercredi 8 juin, 9h00-10h30, Amphi Lebon
   Mustapha Hain, Abdelaziz Marzak and Bernard Coulette
   Vers une démarche pour le développement de PIM à base de Composants Multivue
• Mercredi 8 juin, 14h00-15h30, Amphi Lebon
   Sébastien Limet, Sophie Robert and Ahmed Turki
   Construction automatique d'applications de visualisation scientifique interactives sous contraintes de cohérences
• Mercredi 8 juin, 14h00-15h30, Amphi Lebon
   Ahmed Harbouche, Abdellah Kouider el Ouahed and Hamid Azzoune
   Développement de Systèmes Multi-agents par Transformation de Modèles

IDM

• Mardi 7 juin, 11h00-12h30, Amphi Migeon
   Carlos Gomez, Julien Deantoni and Frédéric Mallet
   Semantic Multi-View model for Low-Power
• Mardi 7 juin, 14h00-15h30, Amphi Appert
   Vanea Chiprianov, Yvon Kermarrec and Siegfried Rouvrais
   Practical (meta-)model extension for modeling language profiles. An enterprise architecture modeling language extension for telecommunications service creation
• Mardi 7 juin, 11h00-12h30, Amphi Appert
   Areski Flissi and Gilles Vanwormhoudt
   Conception de services télécoms : une approche IDM à base d'acteurs, sessions et rôles
• Mardi 7 juin, 16h00-17h00, Amphi Appert
   Bernard Coulette, Eric Kedji, Mahmoud Nassar and Redouane Lbath
   Vers un méta-modèle pour la description des processus IDM collaboratifs
• Mardi 7 juin, 14h00-15h30, Amphi Appert
   Clément Guy, Steven Derrien, Benoît Combemale and Jean-Marc Jezequel
   Vers un rapprochement de l'IDM et de la compilation
• Mardi 7 juin, 9h00-10h30, Amphi Migeon
   Christian Brel, Sebastien Mosser
   Vers une approche flot de données pour supporter la composition d'interfaces homme machine
• Mardi 7 juin, 9h00-10h30, Amphi Appert
   Clément Quinton, Christophe Demarey, Nicolas Dolet and Laurence Duchien
   AppliDE : modélisation et génération d'applications pour smartphones
• Mardi 7 juin, 9h00-10h30, Amphi Migeon
   Cauê Clasen, Frédéric Jouault, Jordi Cabot
   Virtual Composition of EMF Models
• Mardi 7 juin, 11h00-12h30, Amphi Migeon
   Mickael Kerboeuf, Alain Plantec and Jean-Philippe Babau
   An experiment of a MDE approach for the design of reusable DSL tools
• Mardi 7 juin, 16h00-17h00, Amphi Appert
   Emmanuelle Rouillé, Benoît Combemale, Olivier Barais, David Touzet and Jean-Marc Jézéquel
   Bridging the Gap between Software Process and Software Development
• Mardi 7 juin, 16h00-17h00, Amphi Migeon
   Alexandre Feugas, Sébastien Mosser, Anne-Françoise Le Meur and Laurence Duchien
   Déterminer l'impact d'une évolution dans les processus métiers
• Mardi 7 juin, 9h00-10h30, Amphi Migeon
   Julien Bigot, Christian Pérez
   On Model-Driven Engineering to implement a Component Assembly Compiler for High Performance Computing
• Mardi 7 juin, 14h00-15h30, Amphi Migeon
    Eric Cariou, Cyril Ballagny, Alexandre Feugas and Franck Barbier
   Une approche de vérification d'exécution de modèles par contrats
• Mardi 7 juin, 11h00-12h30, Amphi Appert
   Olivier Moïses
   Le projet Wazaabi: un interpréteur de modèles EMF d'UI et un moteur de databiding déclaratif
• Mardi 7 juin, 9h00-10h30, Amphi Appert
   Olivier Caron, Bernard Carre and Gilles Vanwormhoudt
   Bibliothèque de patterns via des templates de modèles. Atelier UML étendu sous Eclipse
• Mardi 7 juin, 16h00-17h00, Amphi Migeon
   Faiez Zalila, Xavier Crégut and Marc Pantel
   Approche transparente pour la vérification des modèles métiers
• Mardi 7 juin, 11h00-12h30, Amphi Migeon
   Marc Palyart
   HPCML - un langage dédié au calcul scientifique
• Mardi 7 juin, 14h00-15h30, Amphi Appert
   Bacha Firas, Kathia Oliveira and Mourad Abed
   Transformation des modèles de BPMN vers UIML
• Mardi 7 juin, 14h00-15h30, Amphi Migeon
   Diana Moreno Garcia and Elmehdi Damou
   Model-driven execution of service-based applications
• Mercredi 8 juin, 16h00-18h00, Amphi Chappe
   Amine Raji and Philippe Dhaussy
   Modèles orientés utilisateurs pour la vérification formelle en contexte industriel
• Mercredi 8 juin, 11h00-12h30, Amphi Chappe, Mercredi 8 juin, 11h00-12h30, Amphi Chappe
   André, Gilles Ardourel, Mohamed Messabihi
   Vérification de contrats logiciels à l'aide de transformations de modèles
• Mercredi 8 juin, 16h00-18h00, Amphi Appert
   Marie Gouyette, Olivier Barais, Jérôme, Lenoir, Cédric Brun, Marcos Almeida Da Silva, Xavier Blanc and Jean-Marc Jezequel
   Movida Studio: a modeling environment to create viewpoints and manage variability in views
• Mercredi 8 juin, 16h00-18h00, Amphi Chappe
   Marie De Roquemaurel, Jean-Paul Bodeveix and Mamoun Filali-Amine
   Réécriture de contraintes OCL
• Mercredi 8 juin, 16h00-18h00, Amphi Chappe
   Valerio Cosentino, Guillaume Doux, Patrick Albert, Gabriel Barbier, Jordi Cabot, Marcos Didonet Del Fabro and Scott Lee
   Une approche de MDE pour la résolution de problèmes de configuration : Une application à la plate-forme Eclipse
• Mercredi 8 juin, 11h00-12h30, Amphi Chappe, Mercredi 8 juin, 11h00-12h30, Amphi Chappe
   Cyril Faucher, Samnang Chea, Frédéric Bertrand, Jean-Yves Lafaye
   Validation sémantique d'objets a l'aide d'un modèle de référence et de contraintes

COSMAL

• Vendredi 10 juin, 11h00-12h30, Amphi Lebon
   Dorel Lucanu, Vlad Rusu
   Support for Formal Verification of Domain-Specific Modelling Languages
• Vendredi 10 juin, 8h30-10h30, Amphi Lebon
   Huu Nghia Nguyen, Pascal Poizat, Fatiha Zaïdi, Philippe Dague
   Test passif de la conformité de chorégraphies WS-BPEL
• Vendredi 10 juin, 8h30-10h30, Amphi Lebon
   Nicolas Petitprez, Romain Rouvoy et Laurence Duchien
   Macchiato : vers un système de panier unique pour le e-commerce
• Vendredi 10 juin, 11h00-12h30, Amphi Lebon
   Diana Allam, Rémi Douence, Hervé Grall, Jean-Claude Royer et Mario Sudholt
   The Synthesis Problem for Trusted Service-based Collaborations
• Vendredi 10 juin, 8h30-10h30, Amphi Lebon
   Nabil Fakhfakh, Hervé Verjus et Frédéric Pourraz
   Agrégation d'attributs qualité pour la supervision des orchestrations de services
• Vendredi 10 juin, 11h00-12h30, Amphi Lebon
   Elie Fares, Jean-Paul Bodeveix et Mamoun Filali
   Environnement de Transformation et de Vérification de Modèles BPEL 2.0 Temporisés
• Vendredi 10 juin, 8h30-10h30, Amphi Lebon
   Zeina Azmeh, Fady Hamoui, Marianne Huchard, Chouki Tibermacine, Maha Driss, Naouel Moha
   Classification hiérarchique et sélection de services Web composable

GDR GPL

• Jeudi 9 juin, 16h00-17h30, Amphi Appert
   Albert Benveniste, Timothy Bourke, Benoît Caillaud, and Marc Pouzet
   Divide and Recycle: Types and Compilation for a Hybrid Synchronous Language
• Jeudi 9 juin, 16h00-17h30, Amphi Appert
   Sandie Balaguer, Thomas Chatain, Stefan Haar
   Building Tight Occurrence Nets from Reveals Relations
• Résumé :
  Occurrence nets are a well known partial order model for the concurrent behavior of Petri nets. The causality and conflict relations between events, which are explicitly represented in occurrence nets, induce logical dependencies between event occurrences: the occurrence of an event e in a run implies that all its causal predecessors also occur, and that no event in conflict with e occurs. But these structural relations do not express all the logical dependencies between event occurrences in maximal runs: in particular, the occurrence of e in any maximal run may imply the occurrence of another event that is not a causal predecessor of e, in that run. The reveals relation has been introduced to express this dependency between two events. Here we generalize the reveals relation to express more general dependencies, involving more than two events, and we introduce ERL logic to express them as boolean formulas. Finally we answer the synthesis problem that arises: given an ERL formula phi, is there an occurrence net N such that phi describes exactly the dependencies between the events of N?
• Jeudi 9 juin, 11h00-12h30, Amphi Appert
   Thierry Millan et Agusti Canals
   L'ingénierie Dirigée par les modèles : où en est-on ?
• Résumé :
  L'ingénierie dirigée par les modèles et, en particulier, les processus de développement logiciel à base de modèles ont toujours été au centre des préoccupations des Journées Neptune. Ces procédures correspondent à un paradigme dans lequel le code source n'est plus considéré comme l'élément central d'un logiciel, mais comme un élément dérivé d'éléments de modélisation. Cette approche prend toute son importance dans le cadre des architectures logicielles et matérielles dirigées par les modèles utilisant des standards tels que les spécifications MDA (Model-Driven Architecture) proposées par l'OMG. De telles architectures s'intègrent tout naturellement dans un processus de développement à base de modèles s'assurant, à chaque niveau de modélisation, que les modèles obtenus et réutilisés ont les qualités requises. Cette démarche met le modèle au centre des préoccupations des analystes/concepteurs. Leur élaboration devient donc centrale et le choix du formalisme revêt une importance capitale. Les travaux concernant l'IDM menés jusqu'à ce jour dans le cadre de collaborations académiques/industrielles montrent que ces technologies intéressent de plus en plus d'industriels. Cet intérêt grandissant a donné lieu à la réalisation de nombreux projets aussi bien nationaux qu'internationaux et à la réalisation de nombreux outils industriels et open-source. Dans ce contexte, il nous a semblé pertinent, pour l'édition 2011 des journées NEPTUNE, de revenir sur des problématiques que nous avons déjà abordées par le passé afin d'une part de présenter les avancées en matière de vérification et de transformation de modèles et, d'autre part, de présenter les nouveaux projets phares dans le domaine des modèles, ainsi que des retours d'expérience d'entreprises ayant utilisé les technologies et les outils IDM dans le cadre de leurs projets. En effet, un nombre important de travaux et de projets ont vu le jour au cours des cinq dernières années et beaucoup avaient, entre autre, comme objectif le transfert technologique des connaissances issues du monde académique vers le monde industriel et le passage à l'échelle. Le mode de sélection des présentations basé sur la cooptation nous permet chaque année d'analyser les différents projets issus de l'ANR, de l'IST, des Pôles de Compétitivités et des grands laboratoires Français pour réaliser notre programme. Cette stratégie offre l'avantage d'avoir un programme fortement ciblé sur des problématiques qui intéressent notre communauté, présente un atout important qui est de nous permettre de dresser chaque année un instantané des problématiques de l'IDM qui font l'objet d'une forte activité aussi bien de la part des académiques que des industriels, et nous permet de proposer une première base pour les débats qui ont lieu à l'issue de chaque journée. La présentation qui sera faite lors de ce séminaire du GDR est notre vision et celle des participants aux journées NEPTUNE. Elle peut être vue comme un élément de débat.
• Jeudi 9 juin, 11h00-12h30, Amphi Appert
   Ileana Ober, Sébastien Gérard
   Modeling Wizards: École d'automne dédiée à la modélisation
• Résumé :
  Lors des rencontres avec les partenaires industriels, ainsi qu'à l'occasions des symposium des enseignants, tels que dans le cadre de la conférence MODELS, on évoque le manque de formation des équipes en termes de notions de modélisation comme l'une des raisons principales de la non-généralisation de l'utilisation de la modélisation. L'organisation d'écoles pour les doctorants est un moyens pour palier à ce problème. Nous présentons ici des retours sur l'organisation de la première édition d'une école d'automne dédiée à la modélisation. Cette école, qui est en train d'être intégrée à la prochaine édition européenne de la conférence MODELS, se propose de devenir un forum d'échange pour les jeunes chercheurs.
• Jeudi 9 juin, 16h00-17h30, Amphi Migeon
   Damien Cassou, Emilie Balland, Charles Consel, Julia Lawall
   Faire levier sur les architectures logicielles pour guider et vérifier le développement d'applications SCC
• Résumé :
  Une architecture logicielle décrit la structure d'un système informatique en spécifiant ses composants et leurs interactions. Projeter une architecture logicielle sur une implémentation est une tâche reconnue difficile. Un élément crucial de cette projection est la description architecturale des interactions entre les composants. La caractérisation de ces interactions peut être plutôt abstraite ou très concrète, fournissant plus ou moins de support de programmation et de possibilités de vérifications statiques. Dans cet exposé, nous explorons un point dans l'espace de conception entre les spécifications abstraites et concrètes des interactions de composants. Nous introduisons la notion de contrat d'interactions qui exprime les interactions autorisées entre composants. Cette déclaration architecturale permet la génération de support de programmation, et favorise diverses vérifications. Nous instancions notre approche sur un langage de description d'architectures pour les applications Sense/Compute/Control et décrivons les stratégies de compilations et de vérifications associées.
• Jeudi 9 juin, 11h00-12h30, Amphi Migeon
   Pierre Castéran, Vincent Filou, Allyx Fontaine
   Preuves formelles de systèmes de calculs locaux
• Jeudi 9 juin, 11h00-12h30, Amphi Migeon
   Paolo Herms, Claude Marché, and Benjamin Monate
   A Certified Weakest Precondition Calculus
• Résumé :
  Deduction-based software verification tools have reached a maturity level allowing them to be used in industrial context where a very high level of assurance is required. This raises the question of the level of confidence we can grant to the tools themselves. In this paper we focus on Dijkstra's weakest precondition calculus which is a central component in several verification tools. We develop, in the Coq proof assistant, a version of this calculus, prove it correct and extract from it an executable version.
• Jeudi 9 juin, 11h00-12h30, Amphi Migeon
   Thomas Jensen, Florent Kirchner, et David Pichardie
   Spécification et validation des politiques de copies d'objet
• Résumé :
  Dans les langages orientés objets, l'échange de données mutables avec du code inconnu est un sujet délicat, en raison du risque de création d'un espace de données accessible à un attaquant. Pour parer à cette éventualité, plusieurs normes de programmation recommandent d'effectuer des copies défensives avant d'accepter ou de renvoyer des références à un objet mutable interne. En revanche, l'implémentation de méthodes de copie telles que clone() est laissé à la charge du développeur. Celle-ci risque alors de ne pas fournir de copie assez profonde, et est sujette à redéfinition par une sous-classe malveillante. Actuellement aucun mécanisme ne permet de sécuriser la copie d'objet. Notre travail propose un système d'annotation de types permettant la définition modulaire de politiques de copie pour des programmes orientés objet. Ces politiques définissent le niveau maximal de partage autorisé entre un objet et son clone. Nous présentons un mécanisme de vérification statique qui garantit que toutes les classes respectent leur politique de copie, y compris dans le cas où des méthodes de copie sont redéfinies, et dont nous établissons la correction sémantique en Coq. Ce mécanisme est implémenté et validé expérimentalement sur les méthodes de clone de plusieurs librairies Java.
• Jeudi 9 juin, 16h00-17h30, Amphi Migeon
   Sébastien Mosser, Gunter Mussbacher, Mireille Blay-Fornarino et Daniel Amyot
   Une approche orienté aspect allant du modèle d'exigences au modèle de conception
• Résumé :
  Des approches orientées aspects sont aujourd'hui disponibles à chaque phase du développement d'un logiciel : analyse des exigences, conception, ou encore implémentation. Passer d'une phase à l'autre en conservant les aspects identifiés au préalable reste un défi majeur, pourtant peu étudié. Nous proposons dans un article publié à AOSD'11 une approche itérative et dirigée par les préoccupations, permettant de transformer un modèle d'exigences orienté aspect en un modèle de conception lui aussi orienté aspect, et ceci de manière automatique. Cette approche est mise en oeuvre en utilisant AoURN (use case maps) pour le modèle d'exigence et Adore pour le modèle de conception (orchestrations SOA). Elle permet l'encapsulation continue des préoccupations identifiées lors des exigences, transformées en artefact de conception. Nous proposons de plus une boucle de rétro-action permettant de remonter dans les modèles d'exigences des défauts constatés dans le modèle de conception, supportant ainsi un processus de développement itératif.
• Jeudi 9 juin, 16h00-17h30, Amphi Appert
   Euriell Le Corronc, Bertrand Cottenceau et Laurent Hardouin
   Flow Control with (Min,+) Algebra
• Résumé :
  According to the theory of Network Calculus based on the (min,+) algebra, analysis and measure of worst-case performance in communication networks can be made easily. In this context, this paper deals with traffic regulation and performance guarantee of a network, i.e. with flow control. More precisely, the optimal window size of a window flow controller is given by considering the following configuration: The data stream (from the source to the destination) and the acknowledgments stream (from the destination to the source) are assumed to be different and the service provided by the network is assumed to be known in an uncertain way, more precisely it is assumed to be in an interval.
• Jeudi 9 juin, 11h00-12h30, Amphi Appert
   Reda Bendraou, Marcos Aurélio Almeida da Silva, Xavier Blanc and Marie-Pierre Gervais
   Early Deviation Detection in Modeling activities of MDE Processes
• Jeudi 9 juin, 16h00-17h30, Amphi Migeon
   Gwenaël Delaval et Éric Rutten
   Modèles réactifs pour le contrôle de reconfiguration dans le modèle à composants Fractal
• Résumé :
  Nous présentons une méthode pour la conception de contrôleurs de reconfiguration dans le modèle à composants Fractal. Cette méthode permet d'obtenir une boucle de contrôle assurant automatiquement des propriétés de sûreté concernant les interactions entre composants, telles que l'exclusion mutuelle, ou le fait d'interdire ou d'imposer certaines séquences. Nous utilisons un langage de programmation pour les systèmes réactifs, muni d'un mécanisme de contrats permettant d'exprimer les propriétés à assurer. La compilation de ce langage inclut une phase de synthèse de contrôleurs discrets, qui permet de générer automatiquement le contrôleur de reconfiguration assurant ces propriétés. Nous montrons la pertinence de cette approche en l'illustrant sur un problème de gestion de ressources pour un serveur HTTP.
• Mercredi 8 juin, 11h00-12h30, Amphi Appert
   Julien Henry
   Analyse statique de programme par Interprétation Abstraite
• Résumé :
  L'analyse statique consiste à trouver à la compilation des propriétés sur un programme, en particulier l'ensemble des valeurs possibles pour chacunes des variables durant l'exécution. Ceci permet par exemple de prouver que le programme ne va pas faire de divisions par 0, ne va pas avoir de débordements arithmétiques, ou encore à calculer des invariants de boucle, etc. Trouver l'ensemble exact des valeurs possibles pour les variables est impossible, c'est pourquoi on a recours à des surapproximations : on calcule un ensemble plus grand, qui contient toutes les valeurs possibles des variables pendant l'exécution, mais aussi d'autres valeurs pour simplifier l'analyse : c'est le cas de l'Interprétation Abstraite, qui est une méthode bien connue de vérification statique. L'objectif est alors de limiter les plus possible ces surapproximations, de sorte à avoir un résultat aussi proche possible du résultat exact.
• Mercredi 8 juin, 11h00-12h30, Amphi Lebon
   Jannik Laval, Usman Bhatti, Nicolas Anquetil, and Stéphane Ducasse
   Software Maintenance Analysis and Understanding of the Software Structure
• Mercredi 8 juin, 11h00-12h30, Amphi Appert
   Fabien Coelho, François Irigoin
   Compiling for a Heterogeneous Vector Image Processor
• Résumé :
  We present a new compilation strategy, implemented at a small cost, to optimize image applications developed on top of a high level image processing library for an heterogeneous processor with a vector image processing accelerator. The library provides the semantics of the image computations. The pipelined structure of the accelerator allows to compute whole expressions with dozens of elementary image instructions, but is constrained as intermediate image values cannot be extracted. We adapted standard compilation techniques to perform this task automatically. Our strategy is implemented in PIPS, a source-to-source compiler which greatly reduces the development cost as standard phases are reused and parameterized for the target. Experiments were run on the hardware functional simulator. We compile 1217 cases, from elementary tests to full applications. All are optimal but a few which are mostly within a mere accelerator call of optimality. Our contributions include: 1) a general low cost compilation strategy for image processing applications, based on the semantics provided by library calls, which improves locality by an order of magnitude; 2) a specific heuristic to minimize execution time on the target vector accelerator; 3) numerous experiments that show the effectiveness of our strategy.
• Mercredi 8 juin, 11h00-12h30, Amphi Lebon
   Tom Mens, Benoît Vanderose, Leandro Doctors, and Flora Kamseu
   Etudes empiriques sur la qualité d'un logiciel lors de son évolution ? l'approche MoCQA
• Résumé :
  Des études empiriques sont nécessaires pour mieux comprendre l'impact de l'évolution et de la maintenance sur la qualité des systèmes logiciels. Plus spécifiquement, elles permettent de comprendre quelles sont les caractéristiques principales affectant la qualité d'un système logiciel lors de son évolution (p.ex., la complétude, la cohérence, la fiabilité, la présence de la documentation et des tests, le respect des conventions de codage, la présence de design patterns et l'absence de antipatterns). Certaines de ces caractéristiques peuvent être mesurées de manière objective (c'est-à-dire, en utilisant des méthodes et outils de mesure logicielle), alors que d'autres peuvent seulement être estimées de manière subjective (par une analyse ou inspection humaine). Nous proposons l'utilisation du framework MoCQA, pour « Model-Centric Quality Assessment », permettant de générer des modèles de qualité opérationnels, adaptés aux besoins spécifiques des projets à évaluer, et permettant de combiner et d'aligner des mesures objectives avec des évaluations subjectives. Nous utiliserons ce framework pour effectuer des études empiriques sur des groupes d'étudiants en informatique dans plusieurs universités en Belgique, en France et ailleurs. La réplication d'une même étude permettra d'avoir un échantillon suffisamment grand pour en tirer des conclusions statistiquement significatives.
• Mercredi 8 juin, 11h00-12h30, Amphi Lebon
   Simon Allier , Salah Sadou, Houari A. Sahraoui, Régis Fleurquin
   D'une application orientée objet vers une application à base de composants via une architecture à base de composant
• Résumé :
  Les applications orientées objet (OO) de taille importante sont souvent complexes et par conséquent coûteuses à entretenir. En effet, elles s'appuient sur le concept de classe, dont la granularité est fine, et ont, entre elles, de nombreuses dépendances plus ou moins explicites. Le paradigme composants logiciels offre un espace de projection bien structurée, de haut niveau d'abstraction, qui permet ainsi une bonne compréhension des applications OO par le biais de vues architecturales. Il devient, ainsi, intéressant d'utiliser cette représentation comme cible d'un processus complet de réingénierie des applications OO. L'automatisation de ce processus est un sujet d'actualité très prometteur. Dans cet article, nous proposons une méthode pour transformer automatiquement une application 00 opérationnelle en son équivalent orientée composants opérationnelle.
• Vendredi 10 juin, 9h00-10h30, Amphi Appert
   Frédéric Dadeau, Pierre-Cyrille Héam, Rafik Kheddam
   Génération de tests à partir de mutations de protocoles de sécurité en HLPSL
• Résumé :
  Nous présentons dans cet article l'application de techniques de génération de tests pour des protocoles de sécurité utilisant la mutation de modèles. Les protocoles sont écrits en HLPSL (High-Level Protocol Specification Language) et sont modifiés dans l'objectif d'introduire des fautes ou des choix d'implantation du protocole. Les mutants sont ensuite analysés par un outil de vérification de protocoles qui conclura soit à la sûreté du protocole (i.e. le protocole est insensible à la mutation considérée), soit à la présence d'une faille en renvoyant un trace d'attaque qui pourra être utilisée comme cas de test pour une implantation du protocole.
• Vendredi 10 juin, 9h00-10h30, Amphi Migeon
   Iovka Boneva, Anne-Cécile Caron, Benoît Groz, Yves Roos, Slawek Staworko, Sophie Tison
   Vues de sécurité pour documents XML
• Résumé :
  Les travaux présentés concernent l'exécution de requêtes de sélection et de mises à jour sur des vues de sécurité non matérialisées, définies sur des documents XML. Dans le cas d'une requête de sélection de noeuds, nous montrons qu'on peut toujours traduire une requête RegularXPath sur une vue (elle-même définie avec RegularXPath), en une requête RegularXPath sur le document source. Dans le cas de mises à jour, nous considérons des vues un peu différentes, définies par des langages réguliers de scripts d'édition qui permettent de supprimer des sous-arbres et de renommer des noeuds. Dans ce cas, nous montrons qu'on peut résoudre le problème de la traduction de mises à jour sur une vue lorsqu'on ne donne aucune contrainte sur le document XML.
• Vendredi 10 juin, 11h00-12h30, Amphi Appert
   Frédéric Peschanski
   Principes et Pratiques de la Programmation Concurrente en Pi-calcul
• Vendredi 10 juin, 11h00-12h30, Amphi Appert
   Chong Li, Gaëtan Hains
   SGL - Programmation parallèle hétérogène et hiérarchique
• Résumé :
  Cet article présente un modèle pour la programmation parallèle à base de diffusion-contraction et réalisé sous la forme d'un langage impératif simple appelé scatter-gather language ou (SGL). Sa conception est basée sur l'experience avec la programmation BSP. Les nouvelles caractéristiques de SGL sont motivées par l'évolution de la dernière décennie vers les architectures parallèles multi-niveaux et hétérogènes contenant des processeurs multi-coeurs, des accélérateurs graphiques et les réseaux de routage hiérarchiques. La conception de SGL est conforme au modèle Multi-BSP de Valiant, tout en offrant une interface de programmation encore plus simple que les primitives de BSML (bulk-synchronous parallel ML). SGL semble couvrir un grand sous-ensemble des algorithmes BSP tout en centralisant la sémantique des communications. Comme tous les systèmes inspirés de BSP, il permet l'équilibrage de charge systématique et des performances prévisibles, portables et évolutives.
• Vendredi 10 juin, 9h00-10h30, Amphi Appert
   Sébastien Bardin, Philippe Herrmann, and Franck Védrine
   Refinement-based CFG Reconstruction from Executables
• Résumé :
  We address the issue of recovering a both safe and precise approximation of the Control Flow Graph (CFG) of a program given as an executable file. The problem is tackled in an original way, with a refinement-based static analysis working over finite sets of constant values. Requirement propagation allows the analysis to automatically adjust the domain precision only where it is needed, resulting in precise CFG recovery at moderate cost. First experiments, including an industrial case study, show that the method outperforms standard analyses in terms of precision, efficiency or robustness.
• Vendredi 10 juin, 11h00-12h30, Amphi Migeon
   Marie de Roquemaurel, Thomas Polacsek, Jean-Paul Bodeveix, Mamoun Filali
   Assistance à la conception de modèles à l'aide de contraintes
• Résumé :
  La conception système est une des premières étapes du processus de conception dite amont. Lors de cette étape, il s'agit de raisonner à un haut niveau de granularité (en faisant abstraction du code) en terme des fonctionnalités à implanter et de l'architecture cible. Pour assister cette phase de conception, nous proposons une approche basée sur les techniques de l'IDM. Le passage à l'échelle de cette approche est envisagé à l'aide d'outils issus de la programmation par contraintes. Nous avons adopté le méta modèle Ecore pour la description des modèles et le langage OCL pour l'expression des contraintes. Nous présentons dans cet article des approches différentes pour exprimer le problème des contraintes sur un modèle, puis nous exposons les apports d'une approche dans la lignée de la programmation par contraintes.
• Vendredi 10 juin, 11h00-12h30, Amphi Migeon
   Christophe Junke,
   Critères de tests pour les automates de modes et application au langage Scade 6
• Résumé :
  Les automates de modes de Scade 6 apportent au langage Lustre la notion d'états et de transitions tout en conservant l'approche flots de données du langage synchrone. Nous étudions et adaptons les critères d'automates usuels au cas particulier des automates de modes. Nous proposons une traduction de ces critères en termes LUSTRE avec horloges, afin de les couvrir avec l'outil de génération de séquences de tests GATeL. Cette traduction pour le moment manuelle repose sur celle des modèles Scade 6 vers LUSTRE, qui existe déjà par ailleurs. Les critères de couverture structurelle des automates peuvent alors être combinés à des critères fonctionnels exprimés par des objectifs de tests, et servir à la génération automatique de séquences de tests couvrantes dans GATeL.
• Vendredi 10 juin, 9h00-10h30, Amphi Appert
   Johan Oudinet(6), Alain Denise, Marie-Claude Gaudel, Richard Lassaigne, and Sylvain Peyronnet
   Exploration uniforme de modèles: application au model-checking de formules LTL
• Résumé :
  Grosu and Smolka have proposed a randomised Monte-Carlo algorithm for LTL model-checking. Their method is based on random exploration of the intersection of the model and of the Buchi automaton that represents the property to be checked. The targets of this exploration are so-called lassos, i.e. elementary paths followed by elementary circuits.During this exploration outgoing transitions are chosen uniformly at random. Grosu and Smolka note that, depending on the topology, the uniform choice of outgoing transitions may lead to very low probabilities of some lassos. In such cases, very big numbers of random walks are required to reach an acceptable coverage of lassos, and thus a good probability either of satisfaction of the property or of discovery of a counter-example. In this paper, we propose an alternative sampling strategy for lassos in the line of the uniform exploration of models presented in some previous work. The problem of finding all elementary cycles in a directed graph is known to be difficult: there is no hope for a polynomial time algorithm. Therefore, we consider a well-known sub-class of directed graphs, namely the reducible flow graphs, which correspond to well-structured programs and most control-command systems. We propose an efficient algorithm for counting and generating uniformly lassos in reducible fowgraphs. This algorithm has been implemented and experimented on a pathological example. We compare the lasso coverages obtained with our new uniform method and with uniform choice among the outgoing transitions.
• Vendredi 10 juin, 11h00-12h30, Amphi Migeon
   Philippe Dhaussy, Fredéric Boniol, Pierre-Yves Pillain, Yves Le Traon, Benoit Baudry
   Formalisation de contextes et d'exigences pour la validation formelle de logiciels embarqués
• Résumé :
  Un défi bien connu dans le domaine des méthodes formelles est d'améliorer leur intégration dans les processus de développement industriel. Dans le contexte des systèmes embarqués, l'utilisation des techniques de vérification formelle nécessitent tout d'abord de modéliser le système à valider, puis de formaliser les propriétés devant être satisfaites sur le modèle et enfin de décrire le comportement de l'environnement du modèle. Ce dernier point que nous nommons est souvent négligé. Il peut être, cependant, d'une grande importance afin de réduire la complexité de la preuve. Dans notre contribution, nous cherchons à proposer à l'utilisateur une aide pour la formalisation de ce contexte en lien avec la formalisation des propriétés. Dans ce but, nous proposons et expérimentons un langage (DSL), nommée CDL (Context Description Language), pour la description des acteurs de l'environnement, basée sur des diagrammes d'activités et de séquence et des patrons de définition des propriétés à vérifier. Les propriétés sont modélisées et reliées à des régions d'exécution spécifiques du contexte. Nous illustrons notre contribution sur un exemple et décrivons des résultats sur plusieurs applications industrielles embarquées.
• Vendredi 10 juin, 11h00-12h30, Amphi Appert
   Jean Fortin et Frédéric Gava
   BSP-Why: an intermediate language for deductive verification of BSP programs
• Vendredi 10 juin, 9h00-10h30, Amphi Migeon
   Y. Boichut, J.-M. Couvreur, D. Nguyen
   Systèmes de Réécriture Fonctionnels pour le Model-Checking Symbolique

Posters et démos du GDR GPL

• Mercredi 8 juin, 15h30-16h30, Hall Polytech, Mercredi 8 juin, 15h30-16h30, Hall Polytech
   Diana Allam, Herve Grall and Jean-Claude Royer
   Towards a unified formal model for service orchestration and choreography
• Mercredi 8 juin, 15h30-16h30, Hall Polytech, Mercredi 8 juin, 15h30-16h30, Hall Polytech
   Pascal André, Mohamed Messabihi and Gilles Ardourel
   COSTO / Kmelia : a Platform to Specify and Verify Component and Service Software
• Mercredi 8 juin, 15h30-16h30, Hall Polytech, Mercredi 8 juin, 15h30-16h30, Hall Polytech
   Vanea Chiprianov, Yvon Kermarrec and Siegfried Rouvrais
   Construction collaborative de services de télécommunications: un processus dirigé par les modèles pour la génération d'outils
• Mercredi 8 juin, 15h30-16h30, Hall Polytech, Mercredi 8 juin, 15h30-16h30, Hall Polytech
   Julien Cohen, Akram Ajouli and Rémi Douence
   Program Transformation based Views for Modular Maintenance
• Mercredi 8 juin, 15h30-16h30, Hall Polytech, Mercredi 8 juin, 15h30-16h30, Hall Polytech
   Antoine Beugnard and Ali Hassan
   Cloud Components for Highly Distributed Environments