Séminaires MaREL 2015

  • 19 mars : David Delahaye, CNAM.Sémantique formelle du langage à composants COMPO (travail en commun avec C. Dony et C. Tibermacine)
    Dans cet exposé, nous présenterons nos premiers pas dans l'élaboration d'une sémantique opérationnelle (à grands pas) du langage à composants COMPO. Actuellement, cette sémantique modélise les descripteurs, les composants, les ports, les connexions, ainsi que l'invocation de service via un port requis. Nous présenterons également un certain nombre de questions qui se sont posées à nous lors de la conception de cette sémantique. En particulier, nous parlerons du passage de paramètres (des services), ainsi que de la modélisation de la couche réflexive du langage (qui permet d'exprimer les contraintes d'architecture), et qui nous apparaissent comme des défis significatifs au-delà du langage COMPO lui-même. Enfin, nous évoquerons la mécanisation de cette sémantique en utilisant le l'outil d'aide à la preuve Coq, qui nous permettra non seulement de raisonner sur cette sémantique, mais aussi d'en extraire un interprète certifié.
  • 26 mars, 11h : Gwen Salaün, INP Grenoble. Reliable Deployment, Reconfiguration, and Control of Cloud Applications
    Résumé : Cloud applications consist of a set of interconnected software components distributed over several virtual machines. Setting up, (re)configuring, and monitoring these applications are difficult tasks, and involve complex management protocols. In this talk, I will first present two protocols for deploying and dynamically reconfiguring cloud applications, respectively. I will also present synthesis techniques for generating controllers in charge of coordinating autonomic managers and cloud applications. These approaches have been devised with the support of formal techniques and tools.
  • 9 avril : Stéphane Ducasse. Titre et résumé à venir.
  • 23 avril : Karell Bertet (Laboratoire L3i, Université de La Rochelle ). Structure de Treillis: Panorama des aspects structurels et algorithmiques. Quelques usages en fouille de données et représentation des connaissances.
    Le premier ouvrage de référence de la théorie des treillis est la première édition du livre de Birkhoff en 1940. Cependant, la notion de treillis a été introduite dès la fin du 19ème siècle comme une structure algébrique munie de deux opérateurs appelés borne inférieure et borne supérieure. Depuis les années 2000, l'émergence de l'analyse de concepts formels (FCA) dans divers domaines de l'informatique, que ce soit en extraction et représentation des connaissances a mis en avant les structures de treillis des concepts et de treillis de fermés. L'émergence de cette structure de treillis s'explique à la fois par la part grandissante de l'informatique dans la plupart des champs disciplinaires, ce qui conduit à la production de données en quantité de plus en plus importante ; mais également par la montée en puissance des ordinateurs qui, bien que la taille du treillis puisse être exponentielle en fonction des données dans le pire des cas, rend possible le développement d'un grand nombre d'applications le concernant.
    La taille du treillis reste cependant raisonnable en pratique, et la nécessité d'algorithmes efficaces pour manipuler ces structures est un défi majeur. Dans un cadre applicatif, une exploitation efficace du jeu algorithmique existant pour manipuler ces structures nécessite cependant une bonne connaissance du formalisme et des propriétés structurelles de la théorie des treillis afin d'identifier les outils algorithmiques adaptés pour un problème donné.
    Ce séminaire a pour objectif de présenter un panorama des concepts de base de la théorie des treillis, ainsi que les principaux algorithmes de génération des objets qui la composent. Quelques exemples d'utilisation en classification et représentation des connaissances seront également présentés. 
  • Jeudi 04 juin 2015, 10H, salle E324, bât 4. Mountaz Hascoet (LIRMM) : Modélisation pour la programmation des IHM, de la théorie à la pratique et inversement.
    Un certain nombre de programmes permettent des interactions simples et/ou fluides comme on aimerait en voir plus souvent. Par ailleurs, un certain nombre de modèles et paradigmes existent dans le but de réaliser la programmation des interactions et ces modèles et paradigmes font l'objet de nombreuses discussions. Il reste néanmoins encore de nombreux décalages entre les deux mondes et à de nombreux égards la programmation d'interactions simples et fluides relève encore plus souvent plus de la haute voltige que de modèles discutés, recommandés et publiés. Dans cet exposé, je présenterai un ou deux cas d'étude en commençant par présenter les modèles publiés, ainsi que quelques exemples de programmes associés.
    Suggestions de (re)lecture:
    [1] Glenn E. Krasner and Stephen T. Pope. 1988. A cookbook for using the model-view controller user interface paradigm in Smalltalk-80. J. Object Oriented Program. 1, 3 (August 1988), 26-49.
    [2] Ed H. Chi. 2002. Expressiveness of the data flow and data state models in visualization systems. In Proceedings of the Working Conference on Advanced Visual Interfaces (AVI '02), Maria De Marsico, Stefano Levialdi, and Emanuele Panizzi (Eds.). ACM, New York, NY, USA, 375-378. http://www2.parc.com/istl/projects/uir/publications/items/UIR-2002-09-Chi-AVI-DataFlowState.pdf
    [3] Robert J. K. Jacob, Leonidas Deligiannidis, and Stephen Morrison. 1999. A software model and specification language for non-WIMP user interfaces. ACM Trans. Comput.-Hum. Interact. 6, 1 (March 1999), 1-46.
  • jeudi 25 juin 2015 à 10h00 , LIRMM - BAT4 - E3.24, Anas Shatnawi (LIRMM)
    «Support à la réutilisation par la rétro-ingénierie des architectures et des composants logiciels à partir du code source orienté objet des variantes de produits logiciels et d'APIs»
    La réutilisation est reconnue comme une démarche intéressante pour améliorer la qualité des produits et la productivité des projets logiciels. L'ingénierie des logiciels à base de composants (CBSE en anglais) et l'ingénierie des lignes de produits logiciels (SPLE en anglais) sont considérées parmi les approches les plus importantes permettant de faciliter et de soutenir la réutilisation systématique. L'ingénierie à base de composants permet de construire de nouveaux systèmes logiciels par composition de briques pré-construites appelées composants. L'ingénierie des lignes de produits logiciels permet de dériver (construire) de nouveaux produits par simple sélection de leurs caractéristiques (feature en anglais). Cette dérivation est rendue possible grâce à la représentation et à la gestion de la variabilité et de la similarité des produits d'une même famille. Cependant, une des difficultés vers une large adoption de l'ingénierie des logiciels à base de composants et des lignes de produits est le coût à investir pour construire, à partir de rien, les composants et les artefacts de SPL. Ainsi, les travaux de cette thèse se positionnent dans ce contexte et proposent de réduire ce coût par une démarche basée sur la rétro-ingénierie.

    La première contribution de cette thèse consiste à proposer une approche permettant d'identifier, par l'analyse d'un ensemble de variantes de produit logiciel orienté objet, les éléments du code source pouvant constituer l'implémentation de composants. Au contraire des approches existantes d'identification de composants, basées sur l'analyse d'un seul produit, l'originalité de notre approche consiste en l'analyse de plusieurs variantes de produuits en même temps. Notre objectif est l'amélioration de la réutilisabilité des composants extraits. L'évaluation expérimentale menée dans le cadre de cette thèse a montré la pertinence de cette démarche.

    La deuxième contribution consiste en la proposition d'une approche pour l'extraction d'une architecture à base de composants d'un ensemble de variantes de produit logiciel orienté objet. Il s'agit d'identifier la variabilité des composants architecturaux et de la configuration architecturale. L'identification de la configuration architecturale est principalement basée sur l'utilisation de l'analyse formelle de concepts pour identifier les dépendances entre les éléments architecturaux. L'expérimentation conduite pour l'évaluation de l'approche proposée confirme la pertinence des résultats obtenus grâce à cette approche.

    La troisième contribution de cette thèse permet de restructurer les APIs orientées objet en composants. Nous exploitons la spécificité des classes des APIs d'être conçues pour être utilisées par des applications clientes pour identifier ces composants. Le code source de ces APIs et celui de leurs applications clientes est analysé afin d'identifier des groupes de classes qui peuvent constituer l'implémentation de composants à extraire. L'identification de ces groupes de classes est basée sur l'analyse des liens structurels entre ces classes et sur la probabilité que ces classes soient utilisées ensembles par les applications clientes. Nous montrons à travers les résultats expérimentaux que la restructuration des API orientées objet en composants facilite la réutilisation et la compréhension des éléments de ces APIs.

  • Adel Ferdjoukh , MaREL, Dept Info, LIRMM
    «Génération de modèles»
    jeudi 08 octobre 2015 à 10h30 , LIRMM, B4 - E3.24

    The automated generation of models that conform to a given meta-model is an important challenge in Model Driven Engineering, as well for model transformation testing, as for designing and exploring new meta-models. Amongst the main issues, we are mainly concerned by scalability, flexibility and a reasonable computing time. This talk presents an approach for model generation, which relies on Constraint Programming.
    After the translation of a meta-model into a CSP, our software generates models that conform to this meta-model, using a Constraint Solver. Our model also includes the most frequent types of OCL constraints. Since we are concerned by the relevance of the produced models, we describe a first attempt to improve them. We outperform the existing approaches from the mentioned point of view, and propose a configurable, easy-to-use
    and free-access tool, together with an on-line demonstrator.

  • Chouki Tibermacine , LIRMM, MaREL
    «Regression-Based Bootstrapping of Web Service Reputation Measurement»
    vendredi 06 novembre 2015 à 14h30 , BAT4-E3.23

    In the literature, many solutions for measuring the reputation of web services have been proposed. These solutions help in building service recommendation systems. Nonetheless, there are still many challenges that need to be addressed in this context, such as the "cold start" problem, and the lack of estimation of the initial reputation values of newcomer web services. As reputation measurement depends on the previous reputation values, the lack of initial values can subvert the performance of the whole service recommendation system, making it vulnerable to different threats, like the Sybil attack. In this paper, we propose a new bootstrapping mechanism for evaluating the reputation of newcomer web services based on their initial Quality of Service (QoS) attributes, and their similarity with "long-standing" web services. Basically, the technique uses regression models for estimating the unknown reputation values of newcomer services from their known values of QoS attributes. The technique has been experimented on a large set of services, and its performance has been measured using some statistical metrics, such as the coefficient of determination (R2), Mean Absolute Error (MSE), and Percentage Error (PE).

  • Nicolas Fiorini , Ecole des Mines d'Alès LGI2P équipe KID
    «Les similarités sémantiques au cœur d’approches génériques d’indexation et de classification»
    vendredi 06 novembre 2015 à 16h00 , BAT4-E3.23

    Pour exploiter efficacement une masse toujours croissante de documents électroniques, une branche de l'Intelligence Artificielle s'est focalisée sur la création et l'utilisation de systèmes à base de connaissance. Ces approches ont prouvé leur efficacité, notamment en recherche d'information. Cependant elles imposent une indexation sémantique des ressources exploitées, i.e. que soit associé à chaque ressource un ensemble de termes qui caractérise son contenu. Ces termes peuvent être remplacés par des concepts issus d'une ontologie de domaine, on parle alors d'indexation conceptuelle. Ceci permet non seulement de s'affranchir de toute ambiguïté liée au langage naturel, mais également d’exploiter les liens existants entre ces concepts. Le plus souvent cette indexation est réalisée en procédant à l'extraction des concepts du contenu même des documents. On note, dans ce cas, une forte dépendance des méthodes d’indexation au type de document considéré. Pourtant une des forces des approches conceptuelles réside dans leur généricité. En effet, par l'exploitation d'indexation sémantique, ces approches permettent de traiter de la même manière un ensemble d'images, de gènes, de textes ou de personnes, pour peu que ceux-ci aient été correctement indexés. Les travaux de cette thèse proposent des solutions génériques pour indexer sémantiquement des documents ou des clusters de documents.

    Deux axes de recherche sont suivis dans cette thèse. Le premier est celui de l'indexation sémantique. L'approche proposée exploite l’indexation de documents proches en contenu pour annoter un document cible. Grâce à l'utilisation de similarités sémantiques entre les annotations des documents proches et d'une heuristique efficace, notre approche, USI (User-oriented Semantic Indexer), permet d'annoter des documents plus rapidement que les méthodes existantes tout en assurant une qualité d’indexation comparable. Une attention particulière a été portée dans ces travaux à l’interaction homme-machine et une approche interactive prenant en compte l’impact d’une imprécision humaine a également été proposée. Le second axe de cette thèse concerne la classification de documents en fonction de leurs contenus. Là encore, la méthode est indépendante du type des documents considérés puisqu’ils sont regroupés sur la base de leurs annotations sémantiques. Un autre avantage de cette approche est que les groupes formés sont automatiquement annotés sémantiquement par notre algorithme.

    L'ensemble des développements de cette thèse ont fait l’objet d’un soin particulier concernant leur optimisation algorithmique afin de permettre un passage à l’échelle, leur validation sur des benchmarks existants ou construits spécifiquement et leur mise à disposition pour des développeurs (via des librairies java) et des utilisateurs finaux (via des serveurs Web). Nos travaux ont montré que l'utilisation d’ontologies permet d'abstraire plusieurs processus et ainsi de proposer des approches génériques sans dégrader les performances. Cette généricité n'empêche en aucun cas d'être couplée à des approches plus spécifiques, mais constitue en soi une simplicité de mise en place dès lors que l'on dispose de documents annotés sémantiquement.

  • Pierre Halmagrand , CNAM, CEDRIC
    «Preuves certifiées pour la méthode B»
    lundi 09 novembre 2015 à 14h00 , LIRMM, B4 - E3.24

    Le développement de logiciels sûrs avec la méthode B repose entre autre sur la vérification d'un grand nombre de propriétés mathématiques exprimées dans une théorie des ensembles ad hoc. Pour améliorer la vérification automatique de ces propriétés, nous avons étendu le prouveur automatique de théorème Zenon à la déduction modulo, une extension de la logique du premier ordre qui permet de transformer un ensemble d'axiomes en un système de réécriture. De plus, cette extension, appelée Zenon Modulo, permet de générer des certificats de preuve vérifiable par le vérificateur de preuve Dedukti.

  • Guillaume Bury , CNAM, CEDRIC
    «Types and arithmetic in Zenon»
    lundi 09 novembre 2015 à 14h30 , LIRMM, B4 - E3.24

    Program analysis and verification often involve to verify arithmetic constraints involving different types such as integers, rationals and reals. In order to deal with these constraints, we will show an extension of the tableaux rules to handle typed proof search and linear arithmetic (also called Presburger arithmetic) as well as the associated proof search methods. We will then present the results of the implementation of this proof search method in the automated theorem prover Zenon.

  • Abderrahman MOKNI , LGI2P, Ecole des Mines d'Alès
    «A formal approach to automate the evolution management in component-based software development processes»
    vendredi 13 novembre 2015 à 14h30 , BAT4-E3.23

    Gérer l'évolution des logiciels est une tâche complexe mais nécessaire. Tout au long de son cycle de vie, un logiciel doit subir des changements, pour corriger des erreurs, améliorer ses performances et sa qualité, étendre ses fonctionnalités ou s’adapter à son environnement. A défaut d’évoluer, un logiciel se dégrade, devient obsolète ou inadapté et est remplacé. Cependant, sans évaluation de leurs impacts et contrôle de leur réalisation, les changements peuvent être sources d’incohérences et de dysfonctionnements, donc générateurs de dégradations du logiciel. Cette thèse propose une approche améliorant la gestion de l'évolution des logiciels dans les processus de développement orientés composants. Adoptant une démarche d’ingénierie dirigée par les modèles (IDM), cette approche s’appuie sur Dedal, un langage de description d’architecture (ADL) séparant explicitement trois niveaux d’abstraction dans la définition des architectures logicielles. Ces trois niveaux (spécification, configuration et assemblage) correspondent aux trois étapes principales du développement d’une architecture (conception, implémentation, déploiement) et gardent la trace des décisions architecturales prises au fil du développement. Ces informations sont un support efficace à la gestion de l’évolution : elles permettent de déterminer le niveau d’un changement, d’analyser son impact et de planifier sa réalisation afin d’éviter la survenue d’incohérences dans la définition de l’architecture (érosion, dérive, etc.). Une gestion rigoureuse de l’évolution nécessite la formalisation, d’une part, des relations
    intra-niveau liant les composants au sein des modèles correspondant aux différents niveaux de définition d’une architecture et, d’autre part, des relations inter-niveaux liant les modèles décrivant une même architecture aux différents niveaux d’abstraction. Ces relations permettent la définition des propriétés de consistance et de cohérence servant à vérifier la correction d’une architecture. Le processus d’évolution est ainsi décomposé en trois phases : initier le changement de la définition de l’architecture à un niveau d’abstraction donné ; vérifier et rétablir la consistance de cette définition en induisant des changements complémentaires ; vérifier et rétablir la cohérence globale de la définition de l’architecture en propageant éventuellement les changements aux autres niveaux d’abstraction. Ces relations et propriétés sont décrites en B, un langage de modélisation formel basé sur la théorie des ensembles et la logique du premier ordre. Elles s’appliquent à des architectures définies avec un ADL formel écrit en B dont le méta-modèle, aligné avec celui de Dedal, permet d’outiller la transformation de modèles entre les deux langages. Cette intégration permet de proposer un environnement de développement conjuguant les avantages des approches IDM et formelle : la conception d’architectures avec l’outillage de Dedal (modeleur graphique); la vérification des architectures et la gestion de l’évolution avec l’outillage de B (animateur, model-checker, solver). Nous proposons en particulier d’utiliser un solver B pour calculer automatiquement des plans d’évolution conformes à notre proposition et avons ainsi défini l’ensemble des règles d’évolution décrivant les opérations de modification applicables à la définition d’une architecture. Le solver recherche alors automatiquement une séquence de modifications permettant la réalisation d’un changement cible tout en préservant les propriétés de consistance et de cohérence de l’architecture. Nous avons validé la faisabilité de cette gestion de l’évolution par une implémentation mêlant optimisation et génie logiciel (searchbased software engineering), intégrant notre propre solver pourvu d’heuristiques spécifiques qui améliorent significativement les temps de calcul, pour expérimenter trois scénarios d’évolution permettant de tester la réalisation d’un changement à chacun des trois niveaux d’abstraction.

  • Yoann Bonavero, MaREL
    «Une approche basée sur les préférences et les méta-heuristiques pour améliorer l’accessibilité des pages Web pour les personnes déficientes visuelles»
    vendredi 20 novembre 2015 à 15h00 , BAT4-E3.23

    Lorsque la vue, qui est un important moyen de communication, est altérée, alors l'acquisition de l'information s'en trouve modifiée, dégradée ou limitée. A l'ère du monde numérique, le Web regorge d'informations réparties sur différents sites et mises en forme par les développeurs et designers. De nombreuses pathologies visuelles peuvent entraîner des difficultés dans l'accès à ces informations. Au-delà même de ces informations, l'accès aux outils et services est lui aussi limité. Des difficultés dans la perception des couleurs, des taches dans le champ visuel ou un champ visuel réduit sont tout autant de sources de difficultés. Chaque personne a une vision qui lui est propre. Chez les personnes qui ont une basse vision, les pathologies donnent des évolutions spécifiques chez chacune d'entre elles. De plus les méthodes de compensation acquises sont différentes d'une personne à l'autre. Des outils d'assistance existent depuis de nombreuses années et tentent de répondre aux besoins des personnes ayant une basse vision en proposant des adaptations visuelles. Les principales limites de ces outils résident notamment dans le fait qu'il ne sont pas en capacité de prendre en compte les besoins très spécifiques de chaque personne. Ces travaux de recherche se concentrent donc autour de l'analyse des besoins réels des utilisateurs et de l'élaboration d'une nouvelle approche qui se base sur les préférences personnelles de l'utilisateur. L'objectif final est d'automatiser la transformation des pages Web en fonction des préférences propres à un utilisateur pendant qu'il navigue sur le Web. Divers algorithmes ont été utilisés, notamment des algorithmes évolutionnaires, afin de réaliser des compromis entre les préférences de l'utilisateur et l'apparence originale de la page Web. La thèse développe de manière approfondie les principaux problèmes touchant les personnes en situation de basse vision et des éléments sur les modèles de couleurs et de contrastes. Puis elle présente un langage de modélisation des préférences basé sur la logique, une modélisation du problème comme un problème d'optimisation, des algorithmes de résolution, un démonstrateur, et des expérimentations sur des pages Web réelles.

  • Fethallah Hadjila , Université de Tlemcen
    «Sélection de Services Composés à base d’espérance-maximisation»
    vendredi 20 novembre 2015 à 16h00 , BAT4-E3.23

    Les services web, représentent une implémentation pratique des principes de l’architecture orientée service. La création de compositions de services, sollicite en général une phase de sélection, qui met en jeu des instances équivalentes d’un point de vue fonctionnel, et différentes d’un point de vue QOS. L’objectif de ce travail est de réaliser la sélection de services en prenant en compte des contraintes de QOS globales. Vu que le problème adressé est de nature NP Hard, nous adoptons deux heuristiques, qui ont comme objectif la réduction du nombre d’instances à parcourir.
    En premier lieu, nous réduisons l’espace de recherche en se focalisant sur les services skylines, en deuxième lieu, nous groupons les services similaires en clusters à l’aide de l’algorithme E.M, et la recherche se focalisera uniquement sur les représentants des clusters. En appliquant ces deux stratégies, nous pouvons atteindre des solutions quasi-optimales dans un délai acceptable. Les résultats obtenus sont très encourageants et peuvent être étendus pour d’autres types de workflows.

  • Jacques Malenfant , Université Pierre et Marie Curie, LIP6
    «Systèmes cyber-physiques : quels modèles ? quel processus de développement ? quel génie logiciel ?»
    mercredi 09 décembre 2015 à 14h00 , BAT4-E3.24

    La robotique et les systèmes autonomiques font partie d’un sous-ensemble des systèmes cyber-physiques où un contrôle au sens de l’automatique s’exerce sur un système formé d’éléments logiciels en interaction avec le monde physique. Apparu dans le domaine du temps réel, le terme cyber-physique traduit la nécessité d’une meilleure modélisation comportementale du logiciel, des phénomènes physiques et des interactions entre les deux pour arriver à construire des systèmes corrects et sûrs. Mais sur quels modèles peut-on s’appuyer ? En quoi ces modèles permettent-ils aux ingénieurs logiciel de conduire un processus de développement correct et sûr ? Quel sera le génie logiciel spécifique à ces systèmes ? L’action transversale ALROB entre les GDR Robotique et GPL s’intéresse à ces sujets sur lesquels nous développons dans cette présentation des pistes et défis de recherche.

  • Julien Pagès , MaREL, Dept Info, LIRMM
    «A virtual machine for testing compilation/recompilation protocols in multiple inheritance»
    vendredi 18 décembre 2015 à 14h30 , BAT4-E3.23

    We present a virtual machine with dynamic loading for a full multiple inheritance language in static typing: Nit. The virtual machine has been designed to be a platform for testing various protocols of compilation/recompilation. Indeed, the runtime efficiency of virtual machines are based on dynamic optimizations, and these protocols, which are generally hidden, are the key factor to their efficiency.

Dernière mise à jour le 23/12/2015