Programme des journées nationales 2011 PDF Imprimer
Vie du GDR GPL
Écrit par Yves Ledru   

Programme des journées nationales du GDR GPL 2011

Lille, 8-10 juin 2011, Polytech, Campus universitaire de Lille 1

Le détail des sessions (avec les résumés des exposés) est donné à la fin de cette page.

mercredi 8 juin 8h30-10h30 Ouverture des journées
Isam Sharour, Vice-président recherche de Lille 1
Jean-Christophe Camart, Directeur de, Polytech' Lille
David Simplot-Ryl, Directeur du centre de recherche INRIA-Lille Nord Europe
Sophie Tison, directrice du LIFL
Laurence Duchien (LIFL, Université Lille 1, INRIA Nord-Europe)
Yves Ledru, directeur du GDR GPL


Conférencier invité : 
Prof. Dr. Tom Mens,
Service de Génie Logiciel, Institut d'Informatique, Faculté des Sciences, Université de Mons, Belgique

Titre: Analyse de l'évolution des aspects sociaux dans les projets logiciels
Pause café et posters
mercredi 8 juin 11h-12h30 Session GT  RIMEL
Président de session : Salah Sadou
  • Jannik Laval, Usman Bhatti, Nicolas Anquetil, and Stéphane Ducasse (RMoD Project-Team, INRIA - Lille Nord Europe, USTL - CNRS UMR 8022, Lille)
    "Software Maintenance Analysis and Understanding of the Software Structure"
  • Simon Allier (1,2) , Salah Sadou (1) , Houari A. Sahraoui (2) , Régis Fleurquin (1)
    1: VALORIA, Université de Bretagne Sud, Vannes, France
    2: DIRO, Université de Montréal, Canada
    "D'une application orientée objet vers une application à base de composants via une architecture à base de composant"
  • Tom Mens (1), Benoît Vanderose (2),  Leandro Doctors (1), and Flora Kamseu (2)
    1. Université de Mons, Belgique
    2. Université de Namur (FUNDP), Belgique
    "Etudes empiriques sur la qualité d’un logiciel lors de son évolution – l’approche MoCQA"


Session GT Compilation (2 présentations)
Présidente de session : Laure Gonnord
  • Fabien Coelho, François Irigoin (MINES ParisTech)
    "Compiling for a Heterogeneous Vector Image Processor"
  • Julien Henry (Vérimag)
    "Analyse statique par découverte de chemin"
mercredi 8 juin 12h30-14h Repas
mercredi 8 juin 14h-15h30 Conférencier invité :
Prof. Roberto di Cosmo (Laboratoire PPS, Université de Paris VII)

Titre:  Le defi des distributions de Logiciels Libres
mercredi 8 juin 15h30-16h30 Session Posters/Démos et Pause café

  • Pascal André, Mohamed Messabihi and Gilles Ardourel  (LINA, Université de Nantes - EMN)
    "COSTO / Kmelia : a Platform to Specify and Verify Component and Service Software"
  • Julien Cohen, Akram Ajouli and Rémi Douence     (LINA, EMN-INRIA)
    "Program Transformation based Views for Modular Maintenance     (Poster et Démo) "
  • Antoine Beugnard and Ali Hassan     (Télécom Bretagne)
    "Cloud Components for Highly Distributed Environments"
  • Diana Allam, Herve Grall and Jean-Claude Royer     (LINA, EMN-INRIA)
    "Towards a unified formal model for service orchestration and choreography"
  • Vanea Chiprianov, Yvon Kermarrec and Siegfried Rouvrais     (Télécom Bretagne)
    "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 16h30-17h30 Table ronde  "Libre et open source, tendances, enjeux et impacts pour la recherche et l'économie numérique"
animée par Franck Barbier

avec:

Au-delà d'une réalité technologique, le logiciel libre et open source est une réalité économique. Il devient un enjeu stratégique (peut-être bientôt de souveraineté ?) pour les Etats vu le caractère de plus en plus diffusant du numérique dans les objets et systèmes du quotidien. Ce débat vise tout d'abord à re-préciser les définitions de "libre", "open source", donner les types de licence connues... Après un état des lieux (qu'est-ce qui existe à l'échelle planétaire ? quels sont les acteurs et "moins acteurs"...), les intervenants de la table ronde donneront leur opinion et leur vision sur des questions ouvertes comme : Quels (nouveaux ?) business models ? Tout logiciel produit doit-il être open source et/ou libre ? Qui finance leur production ? Quels schémas d'évolution pour le libre/open source, des organisations (fondations) aux bases de code à versionner, moderniser, porter... Quelles assurances, quelles garanties, quelles économies d'échelle, quelle pérennité... pour les (grands) utilisateurs ? On n'oubliera pas les Etats qui, sur les sujets de défense, mènent une réflexion aujourd'hui poussée sur "sécurité numérique et libre/open source".
mercredi 8 juin 18h30 (réunion LMO)
mercredi 8 juin 20h dîner de gala
jeudi 9 juin 9h-10h30 Président de session : Christel Seguin

Conférencier invité : 
Dr Cédric Fournet
(Microsoft Research)

Titre: Modèles et outils pour la vérification de programmes utilisant la cryptographie
Pause café et posters (voir ci-dessus)
jeudi 9 juin 11h-12h30 Session GT  IDM
Président de session : Mireille Blay-Fornarino
  • Thierry Millan (IRIT) et Agusti Canals (CS Communication&Systèmes) 
    "L’ingénierie Dirigée par les modèles : où en est-on ?"
  • Ileana Ober (IRIT-Université de Toulouse), Sébastien Gérard (CEA-LIST)
    "Modeling Wizards: École d'automne dédiée à la modélisation"
  • Reda Bendraou (1), Marcos Aurélio Almeida da Silva (1), Xavier Blanc (2) and Marie-Pierre Gervais (1,3)
    1. LIP6, UPMC Paris Universitas, France { Cette adresse email est protégée contre les robots des spammeurs, vous devez activer Javascript pour la voir. }
    2. Labri, Université de Bordeaux 1{ Cette adresse email est protégée contre les robots des spammeurs, vous devez activer Javascript pour la voir. }
    3. UPO, Université Paris Ouest, France { Cette adresse email est protégée contre les robots des spammeurs, vous devez activer Javascript pour la voir. }
    "Early Deviation Detection in Modeling activities of MDE Processes"


Session GT  LTP
Présidente de session : Catherine Dubois
  • Thomas Jensen, Florent Kirchner, et David Pichardie (INRIA Rennes -- Bretagne Atlantique)
    "Spécification et validation des politiques de copies d'objet"
  • Paolo Herms(1,2,3), Claude Marché (2,3), and Benjamin Monate (1) 
    1. CEA, LIST, Software Safety Laboratory, Gif-sur-Yvette F-91191
    2. INRIA Saclay - Île-de-France, 4 rue Jacques Monod, Orsay, F-91893
    3. Lab. de Recherche en Informatique, Univ Paris-Sud, CNRS, Orsay, F-91405
    "A Certified Weakest Precondition Calculus"
  • Pierre Castéran, Vincent Filou, Allyx Fontaine (LaBRI, UMR 5800)
    "Preuves formelles de systèmes de calculs locaux "


Repas
jeudi 9 juin 14h-15h Discussion avec Jean-Pierre Cocquerez sur les évolutions et actions de l'INS2I.

Présentation par Yves Ledru des actions en cours dans le GDR GPL
15h-16h Pause café et session posters et démos
jeudi 9 juin 16h-17h30 Session GT  AFSEC 
Président de session : Olivier H. Roux
  • Albert Benveniste (1), Timothy Bourke (1,2), Benoît Caillaud (1), and Marc Pouzet (2)
    1. INRIA, Rennes.
    2. Ecole Normale Supérieure, Paris.
    "Divide and Recycle: Types and Compilation for a Hybrid Synchronous Language"
  • Sandie Balaguer, Thomas Chatain, Stefan Haar
    INRIA & LSV (CNRS & ENS Cachan)
    "Building Tight Occurrence Nets from Reveals Relations"
  • Euriell Le Corronc, Bertrand Cottenceau et Laurent Hardouin (LISA, Université d'Angers)
    "Flow Control with (Min,+) Algebra"
Session GT COSMAL
Président de session : Pascal Poizat
  • Damien Cassou (Software Architecture Group, Hasso-Plattner-Institut, Potsdam, Germany), Emilie Balland, Charles Consel (Labri/INRIA Bordeaux - Sud Ouest), Julia Lawall  (DIKU, University of Copenhagen, Denmark)
    "Faire levier sur les architectures logicielles pour guider et vérifier le développement d'applications SCC"
  • Gwenaël Delaval (LIG/Université de Grenoble) et Éric Rutten (LIG/INRIA Grenoble)
    "Modèles réactifs pour le contrôle de reconfiguration dans le modèle à composants Fractal"
  • Sébastien Mosser (INRIA Lille–Nord Europe, LIFL (UMR CNRS 8022), Univ. Lille 1, France),
    Gunter Mussbacher (SCE, Carleton University, Canada),
    Mireille Blay-Fornarino (I3S (UMR CNRS 6070), Université Nice–Sophia Antipolis, France),
    Daniel Amyot (SITE, University of Ottawa, Canada)
    "Une approche orienté aspect allant du modèle d’exigences au modèle de conception"
jeudi 9 juin 17h30-19h00 Réunion des comités
vendredi 10 juin 9h-10h30 Session GT Forwal (2 présentations)
Présidente de session : Olga Kouchnarenko
  • Iovka Boneva, Anne-Cécile Caron, Benoît Groz, Yves Roos, Slawek Staworko, Sophie Tison (INRIA Lille, LIFL)
    "Vues de sécurité pour documents XML"
  • Y. Boichut, J.-M. Couvreur, D. Nguyen (LIFO, Université d'Orléans)
    "Systèmes de Réécriture Fonctionnels pour le Model-Checking Symbolique"

Session GT MTV2
Président de session : Arnaud Gotlieb
  • Johan Oudinet(6), Alain Denise(1,2, 3), Marie-Claude Gaudel(1,2), Richard Lassaigne (4, 5), and Sylvain Peyronnet (1,2,3)
    1 Univ Paris-Sud, Laboratoire LRI, UMR8623, Orsay, F-91405;
    2 CNRS, Orsay, F-91405;
    3 INRIA Saclay - Ile-de-France, F-91893 Orsay cedex;
    4 Univ. Paris VII, Equipe de Logique Mathematique, UMR7056;
    5 CNRS, Paris-Centre, F-75000
    6 Karlsruhe Institute of Technology (KIT)    
    "Exploration uniforme de modèles: application au model-checking de formules LTL."
  • Sébastien Bardin, Philippe Herrmann, and Franck Védrine (CEA, LIST)
    "Refinement-based CFG Reconstruction from Executables"
  • Frédéric Dadeau (LIFC), Pierre-Cyrille Héam (LIFC), Rafik Kheddam (LCIS) 
    "Génération de tests à partir de mutations de protocoles de sécurité en HLPSL"
Pause café et posters
vendredi 10 juin 11h-12h30 Session GT  MFDL
Président de session :
  • Marie de Roquemaurel (IRIT CNRS, Université de Toulouse)
    Thomas Polacsek (ONERA, Toulouse)
    Jean-François Rolland (IRIT CNRS, Université de Toulouse)
    Jean-Paul Bodeveix (IRIT CNRS, Université de Toulouse)
    Mamoun Filali (IRIT CNRS, Université de Toulouse)
    "Assistance à la conception de modèles à l’aide de contraintes"
  • Philippe Dhaussy  (Laboratoire LISyC, ENSTA Bretagne, Brest)
    Fredéric Boniol   (Onera/Cert, Toulouse)
    Pierre-Yves Pillain (Laboratoire LISyC, ENSTA Bretagne, Brest)
    Amine Raji  (Laboratoire LISyC, ENSTA Bretagne, Brest)
    Yves Le Traon   (Université du Luxembourg, Campus Kirchberg)
    Benoit Baudry  (Equipe Triskell, l'IRISA, Rennes)
    "Formalisation de contextes et d’exigences pour la validation formelle de logiciels embarqués"
  • Christophe Junke (Laboratoire de Sûreté des Logiciels, CEA, LIST)
    "Critères de tests pour les automates de modes et application au langage Scade 6"


Session GT  LaMHa
Président de session : Frédéric Loulergue
  • Jean Fortin et Frédéric Gava (LACL, Univ. Paris-Est) 
    "BSP-Why: an intermediate language for deductive verification of BSP programs"
  • Frédéric Peschanski (UPMC - LIP6 - APR) 
    "Principes et Pratiques de la Programmation Concurrente en Pi-calcul"
  • Chong Li (1,2),  Gaëtan Hains (1,2)
    1 LACL, Université Paris-Est, 94000 Créteil, France
    2 EXQIM SAS, 24 rue de Caumartin, 75009 Paris, France
    "SGL - Programmation parallèle hétérogène et hiérarchique"


Clôture : proclamation du meilleur poster
vendredi 10 juin 12h30
Repas

 

Conférenciers invités

  • Prof. Dr. Tom Mens, Service de Génie Logiciel, Institut d'Informatique, Faculté des Sciences, Université de Mons, Belgique

    Titre:
    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.
  • Dr Cédric Fournet (Microsoft Research)

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

    Avec Tolga Acar, Karthik Bhargavan, Juan Chen, Andy Gordon, Markulf Kohlweiss, Alfredo Pironti, Dan Shumow, Pierre-Yves Strub, et Nikhil Swamy.

    Résumé:
    Malgré les progrès des techniques de vérification, la sécurité des protocoles et autres systèmes cryptographiques reste problématique. Pour permettre aux programmeurs, cryptographes, et formalistes d'y travailler ensemble, nous proposons de vérifier directement les implantations de protocoles, plutôt que leurs spécifications formelles. Nous développons des bibliothèques cryptographiques et des implantations de références en F#, un dialecte de ML, et nous prouvons leurs propriétés en utilisant des vérificateurs de types dépendants (F7, F*) couplés à un solveur SMT (Z3).

    Deux approches coexistent pour la vérification cryptographique. Certains outils sont maintenant capables d'analyser automatiquement des protocoles complexes. Cependant, ils reposent sur des modèles symboliques qui idéalisent le comportement des primitives cryptographiques, supposées parfaitement sures. Les cryptographes leur préfèrent des modèles calculatoires, afin de calculer précisément la complexité et la probabilité de succès des attaques. Ces modèles sont plus réalistes, mais aussi plus difficiles à formaliser et automatiser.

    Dans cet exposé, je présente ces deux approches et je discute leur intégration avec des techniques de vérification plus généralistes. A l'aide de petits protocoles codés en ML, je montre comment vérifier quelques propriétés de secret et d'authenticité par le typage. Je présente aussi deux applications plus importantes: TLS 1.2, le standard pour HTTPS, et DKM, un composant pour chiffrer les données stockées dans les nuages. Voir http://research.microsoft.com/~fournet et http://msr-inria.inria.fr/projects/sec pour plus de détails (papiers, prototypes, applications).


  • Prof. Roberto di Cosmo (Laboratoire PPS, Université de Paris VII)

    Titre:
    Le defi 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?".

 

Table ronde "Libre et open source, tendances, enjeux et impacts pour la recherche et l'économie numérique"

Président de session : Franck Barbier
Participants :

Résumé :
Au-delà d'une réalité technologique, le logiciel libre et open source est une réalité économique. Il devient un enjeu stratégique (peut-être bientôt de souveraineté ?) pour les Etats vu le caractère de plus en plus diffusant du numérique dans les objets et systèmes du quotidien. Ce débat vise tout d'abord à re-préciser les définitions de "libre", "open source", donner les types de licence connues... Après un état des lieux (qu'est-ce qui existe à l'échelle planétaire ? quels sont les acteurs et "moins acteurs"...), les intervenants de la table ronde donneront leur opinion et leur vision sur des questions ouvertes comme : Quels (nouveaux ?) business models ? Tout logiciel produit doit-il être open source et/ou libre ? Qui finance leur production ? Quels schémas d'évolution pour le libre/open source, des organisations (fondations) aux bases de code à versionner, moderniser, porter... Quelles assurances, quelles garanties, quelles économies d'échelle, quelle pérennité... pour les (grands) utilisateurs ? On n'oubliera pas les Etats qui, sur les sujets de défense, mènent une réflexion aujourd'hui poussée sur "sécurité numérique et libre/open source".

Sessions des groupes de travail

AFSEC

Président de session : Olivier H. Roux

  • Albert Benveniste (1), Timothy Bourke (1,2), Benoît Caillaud (1), and Marc Pouzet (2)
    1. INRIA, Rennes.
    2. Ecole Normale Supérieure, Paris.
    "Divide and Recycle: Types and Compilation for a Hybrid Synchronous Language"
  • Sandie Balaguer, Thomas Chatain, Stefan Haar
    INRIA & LSV (CNRS & ENS Cachan)
    "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?
  • Euriell Le Corronc, Bertrand Cottenceau et Laurent Hardouin (LISA, Université d'Angers)
    "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.

Compilation

Présidente de session : Laure Gonnord

  • Fabien Coelho, François Irigoin (MINES ParisTech)
    "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.
  • Julien Henry (Vérimag)
    "Analyse statique par découverte de chemin"
    • 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.

COSMAL

Président de session : Pascal Poizat

  • Damien Cassou (Software Architecture Group, Hasso-Plattner-Institut, Potsdam, Germany), Emilie Balland, Charles Consel (Labri/INRIA Bordeaux - Sud Ouest), Julia Lawall  (DIKU, University of Copenhagen, Denmark)
    "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.
  • Gwenaël Delaval (LIG/Université de Grenoble) et Éric Rutten (LIG/INRIA Grenoble)
    "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.
  • Sébastien Mosser (INRIA Lille–Nord Europe, LIFL (UMR CNRS 8022), Univ. Lille 1, France),
    Gunter Mussbacher (SCE, Carleton University, Canada),
    Mireille Blay-Fornarino (I3S (UMR CNRS 6070), Université Nice–Sophia Antipolis, France),
    Daniel Amyot (SITE, University of Ottawa, Canada)
    "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 œuvre 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.




FORWAL

Président de session : Olga Kouchnarenko

  • Iovka Boneva, Anne-Cécile Caron, Benoît Groz, Yves Roos, Slawek Staworko, Sophie Tison (INRIA Lille, LIFL)
    "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.
  • Y. Boichut, J.-M. Couvreur, D. Nguyen (LIFO, Université d'Orléans)
    "Systèmes de Réécriture Fonctionnels pour le Model-Checking Symbolique"

 

IDM

Président de session :

  • Thierry Millan (IRIT) et Agusti Canals (CS Communication&Systèmes) : "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.

  • Ileana Ober (IRIT-Université de Toulouse), Sébastien Gérard (CEA-LIST)
    "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.
  • Reda Bendraou (1), Marcos Aurélio Almeida da Silva (1), Xavier Blanc (2) and Marie-Pierre Gervais (1,3)
    1. LIP6, UPMC Paris Universitas, France { Cette adresse email est protégée contre les robots des spammeurs, vous devez activer Javascript pour la voir. }
    2. Labri, Université de Bordeaux 1{ Cette adresse email est protégée contre les robots des spammeurs, vous devez activer Javascript pour la voir. }
    3. UPO, Université Paris Ouest, France { Cette adresse email est protégée contre les robots des spammeurs, vous devez activer Javascript pour la voir. }
    "Early Deviation Detection in Modeling activities of MDE Processes"

 

LaMHa

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

  • Jean Fortin et Frédéric Gava (LACL, Univ. Paris-Est) 
    "BSP-Why: an intermediate language for deductive verification of BSP programs"
  • Frédéric Peschanski (UPMC - LIP6 - APR) 
    "Principes et Pratiques de la Programmation Concurrente en Pi-calcul"
  • Chong Li (1,2),  Gaëtan Hains (1,2)
    1 LACL, Université Paris-Est, 94000 Créteil, France
    2 EXQIM SAS, 24 rue de Caumartin, 75009 Paris, France
    "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'expérience 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.

 

LTP

Président de session : Catherine Dubois

  • Thomas Jensen, Florent Kirchner, et David Pichardie (INRIA Rennes -- Bretagne Atlantique)
    "spécification et validation des politiques de copies d'objet"
    • 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.
  • Paolo Herms(1,2,3), Claude Marché (2,3), and Benjamin Monate (1) 
    1. CEA, LIST, Software Safety Laboratory, Gif-sur-Yvette F-91191
    2. INRIA Saclay - Île-de-France, 4 rue Jacques Monod, Orsay, F-91893
    3. Lab. de Recherche en Informatique, Univ Paris-Sud, CNRS, Orsay, F-91405
    "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.
  • Pierre Castéran, Vincent Filou, Allyx Fontaine (LaBRI, UMR 5800)
    "Preuves formelles de systèmes de calculs locaux "
    • Résumé : 
      Nous présentons une formalisation en Coq de la thèorie des Calcusl Locaux,
      un modèle de l'algorithmique distribué basé sur les réétiquetages de graphes.
      Cette formalisation a permis  de prouver formellement quelques algorithmes
      classqques, mais aussi de prouver des propriétés caractéristiques de sous-classes
      d'algorithmes.

MFDL

Président de session :

  • Marie de Roquemaurel (IRIT CNRS, Université de Toulouse)
    Thomas Polacsek (ONERA, Toulouse)
    Jean-François Rolland (IRIT CNRS, Université de Toulouse)
    Jean-Paul Bodeveix (IRIT CNRS, Université de Toulouse)
    Mamoun Filali (IRIT CNRS, Université de Toulouse)
    "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.
  • Philippe Dhaussy  (Laboratoire LISyC, ENSTA Bretagne, Brest)
    Fredéric Boniol   (Onera/Cert, Toulouse)
    Pierre-Yves Pillain (Laboratoire LISyC, ENSTA Bretagne, Brest)
    Amine Raji  (Laboratoire LISyC, ENSTA Bretagne, Brest)
    Yves Le Traon   (Université du Luxembourg, Campus Kirchberg)
    Benoit Baudry  (Equipe Triskell, l'IRISA, Rennes)
    "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.
  • Christophe Junke (Laboratoire de Sûreté des Logiciels, CEA, LIST)
    "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.

 

MTV2

Président de session : Arnaud Gotlieb

  • Johan Oudinet(6), Alain Denise(1,2, 3), Marie-Claude Gaudel(1,2), Richard Lassaigne (4, 5), and Sylvain Peyronnet (1,2,3)
    1 Univ Paris-Sud, Laboratoire LRI, UMR8623, Orsay, F-91405;
    2 CNRS, Orsay, F-91405;
    3 INRIA Saclay - Ile-de-France, F-91893 Orsay cedex;
    4 Univ. Paris VII, Equipe de Logique Mathematique, UMR7056;
    5 CNRS, Paris-Centre, F-75000
    6 Karlsruhe Institute of Technology (KIT)    
    "Exploration uniforme de modèles: application au model-checking de formules LTL."
    • 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.
  • Sébastien Bardin, Philippe Herrmann, and Franck Védrine (CEA, LIST)
    "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.
  • Frédéric Dadeau (LIFC), Pierre-Cyrille Héam (LIFC), Rafik Kheddam (LCIS) 
    "Génération de tests à partir de mutations de protocoles de sécurité en HLPSL" 
    • 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.

RIMEL

Président de session : Salah Sadou

  • Jannik Laval, Usman Bhatti, Nicolas Anquetil, and Stéphane Ducasse (RMoD Project-Team, INRIA - Lille Nord Europe, USTL - CNRS UMR 8022, Lille)
    "Software Maintenance Analysis and Understanding of the Software Structure"
  • Simon Allier (1,2) , Salah Sadou (1) , Houari A. Sahraoui (2) , Régis Fleurquin (1)
    1: VALORIA, Université de Bretagne Sud, Vannes, France
    2: DIRO, Université de Montréal, Canada
    "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.
  • Tom Mens (1), Benoît Vanderose (2),  Leandro Doctors (1), and Flora Kamseu (2)
    1. Université de Mons, Belgique
    2. Université de Namur (FUNDP), Belgique
    "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.

Posters

  • Pascal André, Mohamed Messabihi and Gilles Ardourel  (LINA, Université de Nantes - EMN)
    "COSTO / Kmelia : a Platform to Specify and Verify Component and Service Software"
  • Julien Cohen, Akram Ajouli and Rémi Douence     (LINA, EMN-INRIA)
    "Program Transformation based Views for Modular Maintenance     (Poster et Démo) "
  • Antoine Beugnard and Ali Hassan     (Télécom Bretagne)
    "Cloud Components for Highly Distributed Environments"
  • Diana Allam, Herve Grall and Jean-Claude Royer     (LINA, EMN-INRIA)
    "Towards a unified formal model for service orchestration and choreography"
  • Vanea Chiprianov, Yvon Kermarrec and Siegfried Rouvrais     (Télécom Bretagne)
    "Construction collaborative de services de télécommunications: un processus dirigé par les modèles pour la génération d’outils"
Mise à jour le Lundi, 06 Juin 2011 17:07