La production de circuits numériques est devenue impossible sans l’aide des ordinateurs. La méthodologie HILECOP assiste les ingénieurs dans la conception et la production de circuits numériques dans le contexte des systèmes critiques, i.e. systèmes dont le malfonctionnement peut résulter en la perte de vies humaines, des catastrophes naturelles, des désastres économiques, etc. A titre d’exemple, la société Neurinnov1 applique la méthodologie HILECOP pour la production de neuroprothèses, considérées comme des dispositifs médicaux hautement critiques par la loi de régulation de l’UE2. Dans HILECOP, les ingénieurs produisent un modèle de circuit numérique. Ils utilisent un formalisme graphique qui regroupe les diagrammes à composant et un type particulier de réseaux de Petri (RdP). Ensuite, le modèle est transformé en une représentation textuelle intermédiaire décrite en langage VHDL (Very high speed integrated circuit Hardware Description Language). Finalement, un compilateur/synthétiseur industriel génère un circuit numérique physique, i.e. un ASIC ou sur carte FPGA, depuis la représentation VHDL. Ici, l’utilisation des RdPs est liée au contexte des systèmes critiques. Les RdPs permettent la vérification de propriétés sur les modèles de circuits numériques grâce à l’application de techniques de model-checking. Cependant, une des transformations décrite dans la méthodologie HILECOP pourrait altérer le comportement (ou sémantique) des modèles initiaux, invalidant ainsi les précédentes étapes de vérification. Le but de cette thèse est de prouver que la transformation modèle-vers-texte de HILECOP, qui génère une description VHDL depuis un modèle de circuit numérique, préserve le comportement des modèles d’entrée, i.e.: pour tout modèle passé en entrée de la transformation, la description VHDL résultante se comporte de la même manière. Pour prouver cette propriété, nous nous inspirons des travaux menés sur la vérification formelle de compilateurs (notamment sur le compilateur C certifié CompCert [1]). Notre approche est celle de la vérification déductive interactive avec assistants de preuve. Dans ce contexte, les étapes pour établir la propriété de préservation de comportement de la transformation sont: (1) formaliser la sémantique d’execution de la représentation source, (2) de la représentation cible, (3) décrire la transformation, et (4) prouver un théorème de préservation sémantique. Même en suivant ce processus clairement détaillé, les spécificités de la transformation modèle-vers-texte de HILECOP (comparaît notamment aux compilateurs) apportent de nouvelles questions recherches et des challenges à chaque étape. Dans cette thèse, nous utilisons l’assistant à la preuve Coq pour nous accompagner tout au long du processus. Finalement, nous avons prouvé que la transformation de HILECOP préserve le comportement de tous les modèles initiaux. La mécanisation complète de la preuve avec Coq est un travail en cours.

1. https://neurinnov.com/
2. https://eur-lex.europa.eu/eli/reg/2017/745/2020-04-24
[1] Xavier Leroy. “A Formally Verified Compiler Back-End”. In: Journal of Automated Rea-
soning 43.4 (Nov. 4, 2009), p. 363.

Alors qu'une proposition de loi souhaite faire converger transition numérique et transition écologique, réduire l'empreinte énergétique des apps mobiles semble pertinent. Mais trouver les racines du mal n'est pas si simple et il faut être capable de mesurer pour pouvoir agir en conséquence. Dans ce séminaire, je présenterai deux outils de mesures distincts mais complémentaires : (1) ecoCode pour mesurer la qualité du code d'un projet Android et (2) powDroid pour mesurer la consommation d'énergie pendant l’exécution d'une app Android.

L’idée de cet exposé est de présenter très simplement la correspondance de Curry-Howard, qui relie (par deux isomorphismes) les preuves et les programmes.

Le contexte de ces travaux est le développement de logiciels pour l'aide à la décision en agronomie par notre collaborateur industriel ITK. Ces logiciels aident les agriculteurs à comprendre et anticiper l'état des cultures grâce à diverses prédictions de simulateurs. Chaque simulateur possède ses propres paramètres à fournir en entrée et reçus en sortie de simulation, avec par exemple le simulateur de production demandant des données différentes du simulateur de la maladie pour la vigne tout en partageant aussi des données communes telles que la météo. Le projet sur lequel nous travaillons a pour but de construire une ligne de produits logiciels qui permettra : i) une dérivation simple de nouveaux produits (par les équipes IT) à partir de nouveaux simulateurs (faits par les équipes d'agronomes), et ii) de simplifier la maintenance de la base de code existante chez ITK. Le processus d'extraction peut être laborieux et prendre beaucoup de temps. C'est pourquoi nous étudions les moyens d'automatiser ce processus en se concentrant sur les schémas de données décrivant les paramètres à fournir en entrée et reçus en sortie des simulations. Nous avons fait l'hypothèse que l'analyse formelle de concept (FCA) est un outil utile pour l'extraction de la variabilité des logiciels, avec par exemple la mise en évidence des points communs et des spécificités de ces logiciels nous permettant d'assister les équipes d'IT et d'agronomes dans la construction de nouveaux logiciels et simulateurs. Cet exposé présente nos travaux sur ce processus permettant d'extraire la variabilité. C'est un processus basé sur une série de pré-traitements permettant l'utilisation d'outils d'analyse formelle de concepts. Ces outils sont utilisés pour construire un AOC-Poset, une structure conceptuelle dérivée d'un treillis de concept dans laquelle nous avons identifié les caractéristiques communes et variables des simulateurs à partir de leurs schémas de données. Nous avons implémenté ce processus, l'avons expérimenté sur une collection de 6 simulateurs et avons obtenu des résultats prometteurs pour la future construction de la ligne de produit.

La maintenance et l’évolution sont des activités inévitables dans le cycle de vie d’un logiciel. Elles sont également très coûteuses. Certaines études estiment jusqu’à 80 % le coût de ces activités par rapport au coût global d’un projet logiciel. Dans ces activités, une part non négligeable est dédiée à la compréhension des programmes. Cette tâche est estimée par certaines études à plus de 50 % du coût de la maintenance.

Afin de faciliter la compréhension du code, il faudrait disposer d’outils qui permettent d’en identifier les parties les plus complexes. A partir de ces éléments, les développeurs pourraient envisager de faire du refactoring afin de diminuer la complexité du code et donc d’en diminuer le coût de maintenance.

Dans l’état de l’art, on trouve des outils, comme SonarQube, qui proposent des métriques pour la mesure de la complexité du code, comme la complexité cognitive. Malheureusement, cette métrique n’est pas correctement formalisée et fournit des résultats qui ne sont pas toujours pertinents.

Afin d’améliorer la fiabilité de ces résultats, nous avons élaboré notre propre métrique et développé un module open-source qui permet d'analyser plus finement la complexité des programmes. Nous proposons de faire une courte démonstration de l’usage de ce module lors de ce séminaire et de discuter de la pertinence des résultats obtenus, ainsi que de leurs inévitables limites.

Enfin, nous tracerons quelques perspectives pour l’avenir:

• Définir une méthodologie permettant de définir plus précisément la notion de complexité cognitive.
• Obtenir des résultats expérimentaux permettant d’estimer la validité de la métrique ainsi définie.

In this talk, I will present the main research I have conducted or participated in for the last 15 years in the field of knowledge discovery from data. Introducing a problem in neuroscience will rise the need of distinguishing (i) data and pattern formalization, (ii) algorithms for mining patterns and (iii) measures for assessing the interestingness of a pattern or a set of patterns. We'll start accordingly by presenting a number of contributions in Formal Concept Analysis, providing a convenient way to formalize what we manipulate in pattern mining. Then, we'll dive into algorithmic issues when enumerating patterns of different natures (especially numerical) that come along as well as two major propositions : mining patterns with a Monte Carlo tree search (MCTS) and mining numerical patterns in the lattice of all discretizations. To better understand the problem of designing pattern quality measures, we'll review a certain number of applications I participated in over the last years (neuroscience, video game analytics, social media analytics) , before focusing on applications in Software Engineering (SQL workload analysis, incident triaging), and other perspectives to be handled in an industrial context in company Infologic, a software editor I work for).

Les projets open-source possèdent, de part leur nature, de nombreuses spécificités dont celle d'impliquer une multiplicité de contributeurs aux profils variés et provenant d'horizons divers. Cette diversité s'exprime, par exemple, dans les types de contributions réalisées par contributeurs. Ces contributions peuvent aller de simples relevés de bugs à l'implémentation de tout ou partie du logiciel. Les projets open-source sont souvent disponibles sur des dépôts de code en ligne (GitHub, GitLab, etc.), cela permet l'extraction d'une grande quantité d'informations allant du code source aux métadonnées accompagnant les dépôts (contributeurs, commits, tickets, etc.). Dans nos travaux, nous focalisons nos recherches sur les contributeurs ayant un impact sur l'architecture à l'exécution du logiciel. Dans ces architectures, les composants à utiliser sont décrits dans des descripteurs de déploiement ou par le biais d'annotations spécifiques. Lors de l'exécution, un mécanisme d'inversion de contrôle est activé; les composants sont alors automatiquement instanciés et les dépendances entre ceux-ci résolues.

Ces éléments nous amènent à la question suivante : comment détecter les développeurs ayant un impact sur l'architecture à l'exécution du logiciel ?

Cette présentation montre qu'il est possible d'extraire et d'étudier différents profils de contributeurs en se basant sur une métrique originale de mesure de la contribution architecturale.Nous utilisons pour cela une approche empirique.
Sur la base de ces travaux, nous présentons également une méthode de classification supervisée permettant de détecter les contributeurs expérimentés ayant un impact sur l'architecture à l'exécution. Cette méthode est basée sur l'apprentissage de profils de développeurs provenant d'un jeu de données étiqueté de contributeurs à des projets open-source auxquels nous avons associé des métriques logicielles.
Enfin, nous présentons les résultats de ces deux approches et nous traçons quelques perspectives.

Les algèbres de Kleene concurrentes (CKA) fournissent un cadre algébrique pour raisonner sur les programmes concurrents. Au cours de ces dernières années, nous avons étudié différentes manières d'enrichir ce modèle afin de capturer une classe plus large de problèmes de vérification.

Dans cet exposé, je présenterai tout d'abord les bases de CKA, avec ses présentations axiomatiques et combinatoires, et les résultats de décidabilité correspondants. Je ferais ensuite un bref panorama de certaines extensions du modèle, en considérant des aspects tels que le flot de contrôle, la cohérence des accès mémoire, et l'exclusion mutuelle.

Ce travail est le fruit de collaborations avec Tobias Kappé, Jana Wagemaker, Simon Docherty, Fabio Zanasi, Jurriaan Rot, Alexandra Silva, David Pym, Damien Pous, et Georg Struth.

In this talk we will discuss some semantic methods to certify the correctness of some optimization and approximation techniques for functional programs. The so-called free theorems provide libraries of equivalence-preserving program transformations which admit a semantic justification through the theory of parametric polymorphism. These transformations have been widely applied to certify optimization techniques (e.g. for compilation). In spite of their well-established semantic grounding, computing new free theorems can be difficult, and we lack a general understanding of the equational theory arising from these transformations. To this end we describe a method to extract new free theorems by computing a class of type isomorphisms based on parametric polymorphism and its categorical understanding.

In the second part of the talk we consider optimization problems in which a program is replaced by one which is not equivalent but only approximately similar. These problems are common in fields involving probabilistic and numerical computation, where efficiency is often traded for accuracy. We will discuss a quantitative semantic framework to certify approximate program transformations which extends methods like the free theorems via the replacement of program equivalence with program metrics.

La théorie de la démonstration fournit une boîte à outils essentielle pour les systèmes de preuves, et pour la recherche automatique des preuves.
Cependant, le manque d'homogénéité des syntaxes des systèmes de preuve et assistants de preuve rend difficile la comparaison et l'échange de preuves entre les différents formalismes.

Pour résoudre ce problème, je présente la théorie des preuves combinatoires (combinatorial proofs), une syntaxe graphique qui permet d'échanger et comparer des preuves entre plusieurs systèmes, et d'identifier les preuves qui diffèrent pour des choix non déterministes négligeables.

En conclusion, je montre comment la syntaxe des preuves combinatoires peut être utilisée pour fournir des certificats de preuve, c'est-à-dire, des objets syntactiques qui contiennent toutes les informations essentielles d'une preuve, permettant de vérifier sa correction.

Les systèmes hybrides sont des systèmes qui intègrent, au même niveau, des composantes discrètes (programmes) et des composantes continues (phénomènes physiques). Beaucoup de systèmes du quotidien rentrent dans cette catégorie, des voitures autonomes aux ampoules connectées, incluant des systèmes critiques, où la vie d'êtres humains entre en jeu.

La certification de ce type de système est rendue difficile par leur nature : l'informatique classique s'adapte plutôt bien à la partie discrète seule, et la théorie du contrôle permet de travailler sur la partie continue; mais intégrer ces deux aspects simultanément dans la démarche de conception et de validation de ces systèmes est un défi important et complexe.

Dans le cadre de nos travaux, nous avons mis au point un cadre formel qui permet la modélisation de systèmes hybrides, intégrant, au même niveau dans le modèle et la vérification, des éléments discrets et continus. Ce cadre s'accompagne de patrons de conception formels, qui permettent de faciliter le développement et la validation de ces systèmes, avec un haut niveau d'abstraction. Ce cadre est validé par son utilisation sur divers études de cas.

Geometry has always had an important role in the evolution of the foundation of mathematics. For example, Euclid introduced the axiomatic method with his Elements. While Euclid's work was considered as a paradigm of rigorous argumentation for over 2000 years, Moritz Pasch pointed out the need for an additional axiom in 1882. Since Automath, the first logical framework designed in 1967, a plethora of proof assistants have been developed, allowing, amongst other things, to avoid such implicit assumptions. In this talk, we investigate how a proof assistant can be used to study the foundations of geometry. We start by focusing on ways to axiomatize Euclidean geometry and their relationship to each other. We also expose a new proof that Euclid’s parallel postulate is not derivable from the other axioms of first-order Euclidean geometry. This independence proof leads us to refine Pejas' classification of parallel postulates. We do so by not only considering continuity axioms, but also decidability properties to determine whether two versions of this postulate are equivalent or not. It requires that “we take the extreme measure of shutting out the entreaties of our intuitions and imaginations”. To help us in this task, a proof assistant allows us to use a perfect tool which possesses no intuition: a computer. Then, we present our progress towards obtaining an independent version of Tarski's axioms. Finally, we report on the advance of the project of proving the isomorphism between two models of hyperbolic geometry formalized in two different proof assistants.

Large distributed systems with an emphasis on adaptability are now considered a necessity in many domains, yet reconfiguration of these systems is still largely carried out in an ad hoc fashion, a process that is both inefficient and error-prone. This presentation will discuss a SMT-based technique to solve the planification problem for the reconfiguration of distributed systems in a component-based model. Specifically, given some tasks to execute and a desired final state of the system, we will show how to compute a reconfiguration plan that guarantees satisfaction of inter-component dependencies and is also optimized for parallel execution.

Security protocols are short distributed programs designed to achieve various security goals such as privacy and authenticity, even if the communications between participants occur on compromised or insecure channels, like the Internet. To achieve these goals, protocols usually rely on cryptographic primitives, like encryption, signature or hash functions, and tools have been developed to automatically prove their security.

Unfortunately, with the rise of the RFID or NFC technologies, new security protocols have been designed to ensure new security requirements, and existing tools do not apply to prove their security.
For instance, regarding the contactless payment protocols or the keyless systems, a new security goal is to ensure the physical proximity of the card to the reader to avoid relay attacks. To do so, the protocols, called distance-bounding protocols, rely on physical properties, like the transmission delay or the network topology, which are usually ignored in existing models and tools.

In this talk I will present a framework which makes the automatic analysis of these protocols possible.

Un Business Process (BP) est un ensemble d’activités organisées pour atteindre un objectif. Business Process Model and Notation (BPMN), (modèle de procédé d’affaire et notation) est un standard ISO qui permet de modéliser à la fois des processus uniques mais également des collaborations où la communication coordonne les processus dans différentes organisations. Il y a eu un grand effort pour fournir une sémantique formelle pour BPMN et de construire des outils de vérification pour cette dernière. Malgré ces efforts, certaines fonctionnalités avancées de BPMN, à savoir la communication, les constructions liées au temps ou encore les multi-instances de processus, sont souvent mises de côté. Cela devient un réel problème car BPMN s’intéresse désormais à les domaines hors de la portée original, par exemple pour l’IoT où la communication et le temps jouent un rôle important. Plusieurs études ont ainsi montré l’expressivité de ce standard et son potentiel pour la modélisation et la génération de code dans ce cadre. Dans cette présentation, nous proposons une sémantique formelle pour un sous-ensemble de BPMN. Cette sémantique prend en compte non seulement les passerelles habituelles, mais également les sous-processus, la communication inter-processus et les constructions liées au temps. Contrairement aux approches transformationnelles, qui donnent une sémantique au BPMN en le mappant à un modèle formel (par exemple, des systèmes de transition ou des réseaux de Petri), notre approche est basée sur une formalisation directe en logique du premier ordre qui est ensuite réalisée de manière simple dans le langage formel TLA+. Nous nous appuyons sur TLA+ modèle checker, TLC, pour fournir aux concepteurs de processus un cadre de vérification, fbpmn, que l'on peut utiliser pour vérifier les propriétés spécifiques du BPMN et du workflows. Notre outils et notre base de données de modèles sont open source et disponibles gratuitement en ligne.

La logique de l’énergie de Stéphane Lupasco est celle du tiers-inclus. Restée relativement confidentielle, elle apparaît aujourd’hui bien adaptée à la description de la réalité - cf. « Logic in Reality » (Brenner 2010).
Au cœur de notre recherche sur la « Transformation des Organisations », le principe d’antagonisme associé à cette logique nous a permis de modéliser le principe de transformation, à l'aide de 3 attracteurs, puis celui d'organisation, à l'aide de 4 boucles. De cette modélisation nous avons dérivé trois résultats opérationnels : un instrument d'observation de la transformation de l'organisation, un langage de description associé, une interprétation des chemins de transformation.
En 2017, nous avions présenté une nouvelle approche d'organisation de l'information — GIST, pour Graine d'Information et Schéma de Transformation — première version de ce langage de description.
A la source de ce langage, nous montrerons comment la logique de l’énergie, qui englobe et étend la logique binaire, nous a conduit à définir une allagmatique, c’est à dire une « théorie des opérations » d’après Gilbert Simondon.

La logique linéaire (Girard, 1987) est apparue comme un raffinement de la logique intuitionniste , sensible aux ressources. L’implication (la fonction) A => B est décomposé en (!A) -o B ou !A est A disponible signifie 0-n copies de A, et -o l’implication linéaire, qui consomme la ressource: U et U-o V entrainent V mais la ressource U a disparu dans l’application de cette règle. Du point de vue de la programmation fonctionnelle, cela permet de partager les calculs. Mais la logique linéaire permet aussi de modéliser les changements d’états, comme dans la programmation impérative ou les réseaux de Petri, comme cela a été remarqué dès les débuts de la logique linéaire (Gehlot & Gunter, 1989):
les places sont des propositions A, B, C,…,
n-jetons dans la place A est vu comme « A et A… et A » n-fois,
une transition consommant 2 jetons de A, 1 de B pour produire 1 jeton dans C et 2 dans D est vue comme l’implication linéaire (A et A et B) -o (C et D et D)
un marquage avec 3 jetons dans A et 2 dans B est vu comme (A et A et A et B et B).
Dans un réseau de Petri P ainsi codé en logique linéaire, un marquage M1 est accessible à partir d’un marquage M0 si et seulement si la logique linéaire dérive M1 à partir de M0 et (!T1 et !T2 et .. et !Tn) où les Ti représentent les transitions qui peuvent être utilisées plusieurs fois. 

L’intérêt de la représentation en logique linéaire des réseaux de Petri, notamment pour la la correspondance entre preuve normale et exécution optimale (Engberg et Winskel 1997, Pradin et al. 1999). Je me suis pour ma part intéressé à la représentation des exécutions vraiment parallèles (true concurrency) où (T|T’) ne se réduit pas à « (T puis T’) ou non déterministe (T’ puis T) »: il y a un ordre partiel sur les transitions et celle qui peuvent être exécutées simultanément son effectivement exécutées simultanément. Cela nécessite de considérer une variante non commutative de la logique linéaire. (Retoré 2004)

@article{EW97,
Author = {Engberg, Uffe and Winskel, Glynn},
Journal = {Annals of Pure and Applied Logic},
Language = {English},
Number = {2},
Pages = {101--135},
Title = {Completeness results for linear logic on {P}etri nets.},
Volume = {86},
Year = {1997}}

@inproceedings{GG89,
Author = {Vijay Gehlot and Carl Gunter},
Booktitle = {Applications of {P}etri nets},
Editor = {G. De Michelis},
Page = {174-191},
Title = {Nets as tensor theories},
Year = {1989}}

@article{CKGV99,
Author = {Brigitte Pradin-Ch{\'e}zalviel and Luis Allan K{\"u}nzle and Fran{\c c}ois Girault and Robert Valette},
Journal = {APII - Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s},
Number = {8-9},
Pages = {943--958},
Title = {Calculating duration of concurrent scenarios in time {P}etri nets},
Volume = {33},
Year = {1999}}

@inproceedings{Ret04petri,
Author = {Christian Retor{\'e}},
Booktitle = {Logic Colloquium 99},
Editor = {Jan van Eijck and Vincent van Oostrom and Albert Visser},
Isbn = {1-56881-203-5},
Note = {Complete version INRIA RR-4288 (2001) http://www.inria.fr},
Pages = {152--181},
Publisher = {ASL and A. K. Peters},
Series = {Lecture Notes in Logic},
Title = {A description of the non-sequential execution of Petri nets in partially commutative linear logic},
Year = {2004}}

En IDM, un métamodèle représente la syntaxe abstraite du Langage de Modélisation Spécifique au Domaine (DSML). Il se compose d’une partie structurelle qui détient les concepts de base du domaine et leurs relations, et d’une partie contraintes (OCL) qui s’applique sur la partie structurelle pour préciser la sémantique du domaine.
Malheureusement, beaucoup de concepteurs de métamodèles ne se focalisent que sur la partie structurelle, à savoir les métaclasses et les relations entre elles. Ceci est dû au fait que l’étape de formalisation de la sémantique du domaine sous forme de contraintes OCL est souvent une tâche très complexe. Par conséquent, à partir d’un métamodèle comprenant seulement la partie structurelle, il serait possible de créer des instances de modèles qui sont syntaxiquement corrects, mais qui ne respectent pas la sémantique du domaine. L'objectif principal de notre travail est d'étudier des métamodèles existants dans la littérature ayant des contraintes OCL (tel que UML). L'étude est axée sur les structures de métamodèles sur lesquelles les contraintes OCL sont appliquées dans le but de caractériser les structures nécessitant souvent des contraintes OCL et les raisons de l'ajout de certaines contraintes.

The Web of Things (WoT) promotes joint usage of smart embedded and Web technologies. However, the increasing amount of connected objects makes the WoT a complex, large, and dynamic environment. Indeed, the WoT brings together elements such as sensors, devices, networks, protocols, data and applications to deliver services for stakeholders. These services operate in the context of the interaction between stakeholders and these elements. Such context then becomes a key source of information that includes data of various nature and sometimes uncertain, thus leading to complex situations. In this paper, we focus on the development of intelligent web services. The key ingredients to make a service intelligent are context diversity, the necessity of a semantic representation to manage complex situations and the capacity to reason with uncertain data. In this perspective, we propose a framework for intelligent services dealing with various contexts, which proactively predict future situations and reactively respond to real-time situations in order to support decision-making. For semantic representation of context data, we use PR-OWL, which is a probabilistic ontology based on Multi-Entity Bayesian Networks (MEBN). PR-OWL is flexible enough to represent complex, dynamic, and uncertain contexts, which is a key requirement for the development of intelligent web services. In this paper, we introduce an architecture for intelligent web service associated to PR-OWL. We demonstrate our contribution with an intelligent plant watering use case to show how our architecture supports proactive and reactive context reasoning in terms of WoT.

Fault localisation problem is one of the most difficult processes in software debugging. The current constraint-based approaches draw strength from declarative data mining and allow to consider the dependencies between statements with the notion of patterns. Tackling large faulty programs is clearly a challenging issue for Constraint Programming (CP) approaches. Programs with multiple faults raise numerous issues due to complex dependencies between faults making the localisation quite complex for all of the current localisation approaches. In this talk we present first our recent works on constraint based data mining (CBDM). In the second part of the talk, we present how CBDM can be applied to solve (multiple) fault localisation problem.

Depuis 2013, nous nous intéressons à la conception
d’un modèle à composants pour les systèmes cyber-physiques
et autonomiques. Parmi les points durs de ce type de systèmes,
le test, la vérification et la validation requièrent des modèles
de comportements complexes et des moyens de simuler l’environnement
cyber-physiques pour exécuter le système dans des conditions
réalistes. Notre angle d’attaque sur le problème consiste à définir
au niveau de chaque composant un modèle de comportement, de composer
ces modèles lors de la composition des composants et de les utiliser
selon une approche « modèle à l’exécution » pour tester, vérifier et
valider. Plus encore, disposer de modèles exécutables ouvre d’autres
possibilités comme l’identification (au sens du contrôle) du système
au déploiement, la détermination des lois de commande, l’auto-adaptation
dynamique, la vérification à l’exécution, etc. L’exposé introduira les
modèles de comportement utilisés et leur réification sous la forme de
modèles exécutables. Un exemple concret nous servira de fil rouge bout
en bout et mènera à une démonstration de l’état actuel de nos travaux.

Nous nous proposons de faire un récapitulatif des méthodes de preuve automatique en géométrie et, étant donné un prouveur de théorème automatique généraliste en logique du second ordre auquel on fourni l'axiomatisation de Tarski, comment améliorer ses performances sur une base de théorème de géométrie. Pour cela nous emploierons la sélection de prémisse grâce au deep learning avec l'aide d'un réseau neuronal convolutif et du word embedding.

Ce travail a pour objectif de mettre en place des outils de machine learning dans le système de preuve interactif Coq. Nous nous sommes concentrés essentiellement sur la manière de caractériser les buts à prouver (dans le système Coq) en jeux de features, c’est à dire en caractéristiques pertinentes de ces buts, et avons examiné l’impact du choix de ces features sur la performance des algorithmes.
La plupart des algorithmes de machine learning nécessitant en effet pour fonctionner des données transformées.
Nous avons donc extrait les buts (conclusions + hypothèses) des preuves depuis coq pour en constituer une base de données. Nous avons ensuite appliqué nos n prédicats à ces buts de manière à les transformer en vecteurs de n booléens.
Finalement nous avons testé nos caractérisations des buts sur différents algorithmes de machine learning. Un développé par nos soins et d'autres appartenant à des bibliothèques python.

Software Product Lines (SPLs) are Software Engineering methodologies that manage the development and evolution of families of product variants. They aim at handling the commonality and variability of these products. SPLs reduce the development cost, time-to-market, and increase overall quality of the product variants.

But Small and Medium-sized Enterprises (SMEs) can find the development of an SPL to be expensive and challenging, especially the process regarding the domain engineering. They can be forced to hire or train dedicated SPL-experts to work on the SPL development. This extra cost can be a significant obstacle toward the adoption of this technology by these enterprises.

We present our work on a new approach to reduce and facilitate the adoption of the SPL techniques in SMEs. The goal of this approach is to automatically and incrementally build SPLs. This is based on an original combination of existing extractive and reactive approaches.

Digital systems are said to be critical when a malfunction
on their side puts human lifes at risk.
The design of such systems often relies on formal models
from which safety and correctness properties can be checked.
The HILECOP methodology for the design and implementation
of critical digital systems proposes Synchronously executed Petri Nets (SPNs)
as a formalism to model the behavior of systems.
In the HILECOP workflow, source code for hardware description (VHDL) is
generated from Petri net models to finally implement the digital system
on a physical circuit.
Then, it remains to be proved that the behavior of the digital system
described with Petri nets is preserved in the generated VHDL code.
In this talk, we present, as a first step towards the establishment of this proof,
our modeling of SPNs and their semantics, i.e their evolution
rules, using the Coq proof assistant.

Les Technologies de l’Information et de la Communication, et en
particulier le Web, ont permis le développement d’outils utilisés au
quotidien pour de nombreux usages tels que l’accès à l’information,
les services de commerce, les services administratifs, ou la vie
sociale(forums, réseaux sociaux). Ces outils sont une chance pour
réussir une société inclusive, apportant des solutions d’intégration
pour les personnes selon leurs différences. Cependant s’ils sont mal
conçus ou mal employés, ils peuvent devenir une source d’exclusion
supplémentaire. Dans cette lancée, l’établissement de standards et
d’initiatives comme le WCAG et WAI-ARIA proposés par l’organisation
W3C a été une avancée technique et politique. Cependant les
développeurs ne les respectent pas toujours, et même lorsqu’ils les
respectent, ce n’est pas toujours suffisant pour assurer une
accessibilité effective. Des outils sont également disponibles dans
les navigateurs web et dans les systèmes d’exploitation, comme la
loupe, le lecteur de pages (transcription vocale), les filtres
modifiant les couleurs (par exemple le filtre d’inversion de
couleurs), des feuilles de styles spécifiques ou des plugins
d’accessibilité dans les navigateurs. Ces dispositifs proposent des
modifications globales, qui ne prennent pas en compte les problèmes
spécifiques d’un utilisateur final. Des travaux proposent au contraire
des adaptations personnalisées et cherchent à la fois à satisfaire
les préférences d’un utilisateur et à préserver autant que possible
l’esprit du design initial de la page. Dans cette optique l’outil EWPA
(http://ewpa.lirmm.fr/) a vu le jour. Cet outil récupère les
préférences des utilisateurs à travers une interface web et se sert
des algorithmes génétiques pour déterminer les nouvelles couleurs qui
satisfassent ses préférences. Cependant, la récupération des
préférences des utilisateurs est faite de façon explicite, et le
calcul de l’adaptation dépasse 10 s sur une partie des
configurations testées, ce qui n’est pas très acceptable en pratique.
Dans les soucis d’améliorer l’outil, nous avons modélisé les options
d’accessibilités des systèmes d’exploitation les plus répandus à
travers les Features Models, par la suite nous nous servons de
l’Analyse Formelle de Concepts, et des ontologies pour déterminer les
points communs qui serviront à améliorer l’interface d’EWPA afin
qu’elle permette le recueil des préférences des utilisateurs au moins
de façon semi-automatique. Par ailleurs, dans les soucis d’améliorer
le temps de calcul de l’adaptation, nous étudions l’approche par la
programmation par contraintes.

Dans cette présentation, nous montrons les challenges qui se posent lorsque l'on veut faciliter à des non-experts le développement d'applications robotiques personnalisées à partir de codes pré-existants. Nous souhaitons appliquer l'approche par Lignes de Produits dans le contexte d'un robot Turtlebot et des codes existants dans ROS (Robotic Operating System).

L'exposé propose une vision synthétique des techniques d'apprentissage automatique/fouille de données (AA/FD), appliquées en particulier au génie logiciel, dont les objets (programmes) sont par définition très structurés. À partir d'un cadre dans lequel de nombreuses approches AA/FD peuvent être plongées, nous ferons un point sur des réussites et échecs du passé, et évoquerons les pistes qui, aujourd'hui, semblent les plus prometteuses.

La prédiction en termes de qualité de service (QoS) est une tâche importante dans la sélection et la recommandation des Services Web.

Les approches existantes en matière de prédiction de la qualité de service reposent sur deux méthodes distinctes : le filtrage par contenu ou le filtrage collaboratif. Dans les deux cas, ces approches utilisent des données externes ou des interactions passées entre utilisateurs et services pour prédire les scores de qualité de service manquants ou futurs.

Dans cet article, nous nous intéressons à la factorisation matricielle (filtrage collaboratif) pour la prédiction de la qualité de service (avec des modèles à facteurs latents). L'idée de base de la factorisation matricielle consiste en l’apprentissage d’un modèle compact pour les utilisateurs et les services. Ensuite, la prédiction de la qualité de service est calculée par le produit scalaire entre le modèle latent de l'utilisateur et le modèle latent du service.

Pour ce faire, nous proposons une approche pour la prédiction de la qualité de service, en utilisant un réseau de neurones, un auto-encodeur, dont l’apprentissage se fera sur un dataset standard WSDream.

Les entreprises et les organisations sont plus que jamais mises au défi par leur environnement qui évolue et sollicite de nouveaux services. Dans ce contexte, les systèmes d’information, d’entreprise (SIE) en particulier, revêtent une importance particulière pour les raisons suivantes : (1) ils restent l’un des derniers leviers permettant d’accroître les performances, la qualité et la compétitivité de l’entreprise, dans un monde professionnel où une limite de performance et de qualité est due à la capacité uniforme des outils industriels dans une économie mondialisée et (2) le SI peut augmenter la valeur du produit grâce à des services numériques supplémentaires (construits sur des données associées au produit) afin de mieux répondre aux besoins des clients. Cet intérêt pour un SI performant est également vrai pour les autres types d’organisations humaines et sociales.

Cependant, l'utilisation des SI atteint une limite dans les environnements collaboratifs car les méthodes de gestion des entreprises/organisations divergent et les SI sont construits à partir d’ensembles de ressources souvent peu flexibles qui ne sont pas créés avec un objectif d'interopérabilité. Par conséquent, nous devons rendre les SI plus interopérables afin de réaliser des gains nécessaires en termes de capacités d’adaptation, d’évolution et de performance. Cette présentation peut être résumée comme suit : (1) Elle propose un cadre conceptuel dirigé par la modèles, et (2) Elle décrit des travaux existants basés sur les modèles réalisés à l’université de Bordeaux puis poursuivis avec l’IMT Mine d’Ales, et examine l’apport de la simulation pour observer des comportements attendus du futur SI. Ces approches basées sur les modèles doivent surmonter des barrières d’interopérabilité par une approche liant méthodologie et technologie et ce pour parvenir à une prochaine génération de SI.

Les lignes de produits logiciels et une nouvelle génération de middleware et d’architectures orientées services, nées récemment, ont aidé à définir, mettre en œuvre et exécuter des systèmes capables d’adapter leur comportement en fonction de changements propres à eux ou de changements qui interviennent dans leur environnement et dans leurs conditions d'exécution. Il s’agit ici d’une méthode bien plus radicale que la production unitaire de logiciels sur mesure et l’utilisation de simples adaptations contrôlées par des paramètres.

L'émergence de tels mécanismes (production de masse de systèmes personnalisés et auto-adaptation de ces systèmes) a de profondes implications dans le développement de logiciels. En particulier, il permet (i) le développement au niveau industriel de logiciels pouvant fonctionner dans un large éventail de contextes sans avoir à énumérer comment le système doit se comporter dans chaque environnement ; et (ii) le développement de logiciels pouvant être conçus et pouvant fonctionner en présence d’incertitudes quant aux contextes qui peuvent survenir lors de l'exécution.

Pour combiner les avantages de ces deux mécanismes je propose un cadre à deux dimensions appelé VariaMos. La première dimension est l’approche par ingénierie des lignes de produits logiciels dont les deux principaux processus sont : l’ingénierie de domaine et l’ingénierie d’application. La seconde dimension concerne un nouveau processus appelé ingénierie d’adaptation, qui, couplée aux deux autres processus, constitue la méthode de l’ingénierie des lignes de produits dynamiques. VariaMos a été outillé afin de permettre la conception, la simulation et le développement de systèmes à forte variabilité selon ces deux dimensions. Durant le séminaire, je montrerai ce cadre, son implémentation et ses perspectives d’amélioration et d’évolution.

Le cycle de vie d’un projet logiciel se compose en général de plusieurs phases successives. Premièrement, il y a la phase de développement de la version initiale. Ensuite survient la phase d’évolution, où le logiciel est activement mis à jour. Ensuite, la phase de "servicing" a lieu. Durant cette phase, le logiciel ne subit plus que des corrections mineures qui permettent de le maintenir en état de fonctionnement. Finalement, le logiciel est abandonné. Il est admis que la phase la plus coûteuse est celle d’évolution. Elle occasionne en général entre 60 et 80% du coût total d’un logiciel. Ainsi, cette phase d’évolution logicielle fait l’objet de recherches intensives dans le domaine du génie logiciel.

La recherche en évolution logicielle vise à mieux comprendre les tenants et aboutissants de cette phase ainsi qu’à créer des outils pour réduire sa complexité. À la base de toute cette recherche, il y a un objectif fondamental : être capable d’analyser comment les logiciels évoluent. Actuellement, les travaux conduits dans ce domaine se basent en grande majorité sur l’analyse de l’évolution textuelle du code des logiciels. Le principe de cette analyse est de modéliser le code comme étant une suite de lignes de texte. Pour trouver les changements entre deux versions, il faut alors calculer une des plus courtes séquences d’actions d’édition de type ajouter une ligne et supprimer une ligne qui transforme la version source en la version cible. Cette manière de procéder est très grossière car elle donne des résultats au niveau du texte (le développeur a ajouté la ligne "public void foo() {") plutôt qu’au niveau de la structure (le développeur a ajouté une nouvelle fonction). En outre, les actions d’édition considérées ne permettent pas de capturer plusieurs façons d’éditer le code fréquemment utilisées par les développeurs comme déplacer un élément de programme ou renommer un élément de programme.

Dans cette présentation je présenterai une technique ambitieuse que j'ai développé dans mes travaux : l'analyse de l'évolution syntaxique du code des logiciels, qui améliore l'analyse textuelle et permet des nouvelles applications pour faciliter le développement logiciel. Je présenterai ensuite mes perspectives de recherche.

Proposition d'un projet de recherche, centré sur l'ingénierie des modèles et un terrain d'application : les apprenants dans un dispositif d'une FOAD (Formation Ouverte et A Distance).
Proposition d'une modélisation informatique basée sur le traçage des activités pour aider l'apprenant et encourager son engagement dans l'action collective afin de soutenir son apprentissage. La conception d'un outil d'analyse des traces d'interactions pour permettre de valoriser le partage des connaissances ainsi que l'enrichissement du dispositif global innovant de formation e-learning (activités et données éducationnelles), au gré de l'apprentissage individuel.

L'interprétation abstraite est une théorie d'approximation par excès basé sur la manipulation d'ensemble de valeurs. Cette dernière permet le développement d'une analyse statique dite "robuste", afin de pouvoir estimer les possibles valeurs que contient un programme. Il sera donc intéressant de voir son application dans le domaine de la sécurité.

Le projet Knomana (Knowledge management on pesticides plants in Africa) vise à recenser les connaissances sur les usages de plantes naturellement pesticides déjà utilisées en Afrique et à les rassembler dans la base de connaissances PPAf pour ensuite pouvoir les exploiter de manière simple.

Chaque usage de plante est décrit au moyen de plus de 30 attributs et la base compte plus de 10 000 ligne de connaissances, ce qui représente une grande quantité d'information. Le type d'utilisateur susceptible de vouloir se servir de ces connaissances est très varié (producteurs, consultants, chercheurs, etc).

Il est donc nécessaire de mettre en place une solution qui permettrait à tout ces utilisateurs qui n'ont pas tous la même aisance avec les outils numériques ni les mêmes besoins envers ces connaissances, de naviguer et d'explorer de manière simple les données collectées. L'utilisation de la méthode d'analyse relationnelle de concepts (ARC) permet une organisation des données sous forme de treillis de concepts et ainsi pouvoir répondre à des questions auxquelles une base de données classique ne saurait répondre. La navigation dans des treillis volumineux étant très difficile, une approche incrémental est proposée pour une construction progressive des treillis afin d'en faciliter la navigation et pour une meilleur exploitation.

Berger-Levrault développe des solutions pour les administrations, les collectivités locales et les entreprises.

Elle possède des applications client/serveur qu’elle souhaite rajeunir.

En particulier, le front-end est développé en GWT et doit migrer vers Angular 6.

Mon travail est d’aider l’entreprise à effectuer la migration de ses applications.

Entre autre, je travaille sur un outil, permettant d’effectuer la migration de manière semi-automatique, qui s’appuie sur un méta-modèle représentant une application graphique.

Durant ce travail de stage encadré par D. Delahaye et D. Andreu, j'ai étudié le formalisme et la sémantique des réseaux de Petri SITPN (Synchronous Interpreted Time Petri Nets) relatifs à la méthodologie outillée Hilecop qui est utilisé pour configurer des circuits électroniques de types composants logiques programmables, utilisés dans des dispositifs médicaux implantables (neuroprothèses). Suite à cette étude j'ai utilisé l'assistant de preuves Coq pour spécifier et implanter un animateur desdits réseaux de Petri en développant des preuves formelles de correction et complétude.

GRIMM (Generating Realistic Instances for Meta-Model) est un outil développé au LIRMM, permettant d’assister un utilisateur lors de la conception d’un méta-modèle. Pour cela, il génère, de manière combinatoire, un ensemble de modèles conformes à celui-ci. Il tire parti de la Programmation par Contraintes pour exprimer à la fois le méta-modèle ainsi que des contraintes OCL (Object Constraint Langage) pour générer des instances syntaxiquement valides. C'est un outil utile dans le monde de l'ingénierie dirigée par les modèles car il permet de visualiser des instances d'un système avec des exemples.

Ces exemples ainsi générés seront conformes au méta-modèle mais peuvent ne pas représenter correctement ce système qui est modélisé. L’ajout nouvelle de contraintes OCL permet d’exprimer plus de détails du système et d'affiner la modélisation. L’expression de contraintes OCL peut être difficile car un expert de domaine peut avoir des difficultés à les décrire ou bien elles sont implicites et donc omises par l’expert. Il est communément admis qu'il est plus facile pour un expert d’accepter ou réfuter des exemples que de formaliser des contraintes.

Il existe plusieurs outils pouvant faire de l’acquisition de contraintes tels que QUACQ (QUick ACQuisition Système) ou Contraint Seeker. Ces deux outils permettent d’assister un utilisateur lors de la modélisation d’un problème avec la Programmation Par Contraintes (PPC). Pour cela, ils se basent sur des exemples positifs et négatifs pour inférer des contraintes.

Le sujet de ce stage consiste à trouver une approche qui permet d’acquérir des contraintes OCL en utilisant l’outil GRIMM ainsi que des outils d’acquisition de contraintes. L’outil GRIMM permettrait de générer des exemples à partir d’un méta-modèle et des contraintes OCL. Ces exemples seraient évalués par l’expert. Enfin les modèles évalués peuvent être utilisés par des outils d’acquisition de contraintes qui proposera des contraintes additionnelles. Le processus pourra être répété jusqu’à ce qu’un nombre suffisant de contraintes OCL soient trouvées.

La géométrie euclidienne est une théorie mathématique qui a intéressé de nombreux scientifiques à travers les siècles. L'enjeu de ce stage a été d'utiliser une axiomatisation connue (axiomatisation de Tarski) de la géométrie pour expérimenter la déduction modulo théorie, une méthode de preuve automatique se basant sur des règles de réécriture, sur un benchmark de 1240 lemmes. Nous verrons les résultats que nous avons obtenus grâce au logiciel de déduction automatique intégrant la déduction modulo théorie Zipperposition.

Dans les systèmes complexes plus que dans tout autre système, l'étape d'ingénierie des exigences est primordiale.
En effet, si le système ne répond pas aux exigences, dans le meilleur des cas il ne sera pas utilisé, mais dans le pire des cas, les conséquences peuvent être dramatiques.

Si les approches formelles permettraient de résoudre cette question, elles ne sont utilisées la plupart du temps que dans les systèmes critiques, les exigences étant majoritairement exprimées en langue naturelle.
Avec une représentation formelle des exigences tout au long de la conception du système, il serait possible de s'assurer, potentiellement à l'aide d'outils automatiques, que le système créé est le bon système.

Alors, comment faire en sorte que les exigences soient exprimées de façon plus formelle ?

Tout d'abord, il faut prendre en compte que les exigences sont le lien entre les différentes parties prenantes d'un projet, qui ne sont pas tous des experts – c'est pour cette raison que la langue naturelle est la plus utilisée.
De plus, même parmi les experts impliqués dans le projet, tous n'ont pas forcément des compétences en méthodes formelles.

C'est sur ces verrous que portent mes travaux de thèse.

L'idée est de proposer un langage dédié qui permet d'exprimer toutes les exigences, de leur représentation en langue naturelle à une représentation plus formelle.
En définissant la sémantique de ces exigences, mais aussi de leurs liens, l'utilisation d'outils de preuves doit ainsi permettre de détecter les éventuelles incohérences dans la conception dès le début du projet.

Par ailleurs, les différentes parties prenantes dans un système complexe viennent de différents milieux. Ainsi, des électroniciens peuvent côtoyer des informaticiens, ou même des ingénieurs mécaniciens.
Ces différents acteurs ont l'habitude d'utiliser des outils de leur domaine, et nous proposons d'utiliser l'ingénierie dirigée par les modèles pour permettre de créer des ponts entre ces différents mondes et notre langage.

A number of software architecture recovery approaches were proposed in the literature but only few of them targeted the recovery of runtime architecture models. Moreover, only few approaches provide strategies to manage the complexity of the recovered architecture models, especially in the case of large software systems. We propose a method to build runtime architecture models of object-oriented systems. The method combines static and dynamic analysis to build an Object Graph (OG) that includes information regarding allocation site execution probabilities and lifespans of objects. This information is used to manage the complexity of the recovered object graphs by making it possible for the designer to focus for example on the most likely and durable objects. In addition, composition/ownership relations between objects are exploited to embed composite structures into the OG nodes. This enables to support a hierarchical visualization of the recovered architecture. We implemented a prototype of the method and experimented it on a case study. The results of this experimentation showed that the recovered OG contributes in reducing the complexity of the runtime architecture and in handling some comprehension tasks.

Designing or renovating inheritance hierarchies in the domain of programming or in the domain of modeling still remains a tricky task. It involves integrating domain concepts sometimes with no clear frontier, finding the good abstractions and avoiding duplicated information.
In this presentation, we review research work that addressed this topic with the use of Formal and Relational Concept Analysis since the seminal paper of R. Godin and H. Mili at OOPSLA'93.
We overview the different historical steps and the current issues and perspectives.

Originally conceived as a technique to improve internal code quality, refactoring can also help to improve non-functional attributes of software, such as usability or accessibility. This is specially useful for addressing issues (bad smells, in the jargon) on already running applications. During this talk, I will present the work carried out at LIFIA for improving web usability and accessibility through the use of client-side web refactoring, which can be applied without altering the application’s code. Special focus will be made in Kobold, an automated agent capable of discovering usability smells and fixing them through refactoring.

La croissance rapide des nouvelles technologies de l’information et de la communication (TIC) impose l’adoption de ces technologies dans les différents services, y compris les services administratifs. Ces derniers peuvent fournir des informations à ses citoyens via l’Internet.

L'Internet devrait fournir aux utilisateurs ayant une déficience visuelle les mêmes besoins qu'il offre aux utilisateurs voyants. En dépit des progrès significatifs dans les TIC, les utilisateurs aveugles et malvoyants rencontrent toujours des obstacles lors de l'accès au contenu Web et aussi pour mettre en ligne leurs informations. Pour cette raison, les sites Internet doivent respecter un certain nombre de normes et certains critères d'accessibilité.

L’objectif de notre travail est de trouver des moyens informatiques adéquats et faciles pour les utilisateurs malvoyants pour leurs faciliter les tâches de navigation tout en les optimisant, d'une part en contribuant à compenser les problèmes liés directement à la non-conformité des pages web et d'autre part en optimisant la recherche pour ces personnes. Les principales étapes de notre travail sont : premièrement on optimise la recherche d’information, ensuite on améliore l’interprétation des pages web en négligeant les parties inutiles et à la fin on aide le webmaster malvoyant pour créer un site web accessible.

Après l’étude de chaque étape nous voulons choisir et tester la métaheuristique évolutionnaire bio-inspirée qui est l’algorithme des lucioles (FireFly Algorithm, FF) dans la phase d’optimisation de la recherche d’information (RI) pour la reformulation des requêtes.

This talk presents our contributions in what is referred to as extractive Software Product Line (SPL) adoption. The objective was to propose approaches to migrate existing similar product variants, created using the clone-and-own approach, into an SPL. Instead of designing variability, our work focused on variability inference. The first part of our work considered static variability inference, which is based on the analysis of the structural (or static) information of the product variants, including, for instance, the source code, models, requirements, documentation etc. In addition to the structural information, product variants can also be defined by the dynamic information on their execution. The execution traces are the main source of such information. When execution traces are available, it is possible to analyze them to infer the behavior of these product variants, which can be used to infer the SPL behavior. The second part of our work is thus related to dynamic variability inference, which refers to variability inference using the dynamic information. Our contributions were implemented and integrated within the BUT4Reuse tool. BUT4Reuse is freely available at https://but4reuse.github.io.

Le cloud computing fait désormais partie des habitudes. Il implique l'utilisation d'outils distribués, tolérants aux fautes, et horizontalement scalables.
Si certaines approches permettent de transformer des bases de données ACID existantes pour les utiliser sur un cloud de manière transparente du point de vue des applications, d'autres bases se permettent se sacrifier quelques unes de leurs caractéristiques pour en améliorer les propriétés de tolérance aux fautes, de réactivité, et de scalabilité. Ces nouvelles bases proposent de nouveaux modèles de données, et permettent l'écriture d'applications qui peuvent hériter de leurs propriétés de tolérance aux pannes, de réactivité, et de sacalabilité horizontale.
L'usage veut également que pour l'écriture d'une application utilisant une base de données, l'on utilise une couche d'abstraction pour accéder aux données, connue sous le nom d'Object Relational Mapping (ORM). Cette couche permet d'adapter le modèle de données proposé par la base (souvent un modèle relationnel) au modèle de données manipulé dans le langage de programmation utilisé pour construire l'application. Cette couche d'abstraction permet aux développeurs d'oublier certains des détails correspondant à la communication avec la base.
Toutefois, ces ORMs sont dans leur grande majorité prévus pour une adaptation au modèle de données relationnel. De plus, certains des détails abstraits par les ORMs peuvent impacter les propriétés de tolérance aux fautes, de réactivité et de scalabilité horizontales, voire faire oublier ces aspects programmeur. Nous discuterons ici de la création d'un ORM spécialisé pour la création d'applications destinée à être posées sur un cloud, et dont la cible sera une base non relationnelle distribuée.

Les treillis de Galois et les treillis de concepts sont des structures clefs de l'Analyse Formelle de Concepts (AFC), qui est une méthode d'analyse de données spécialisée dans l'extraction d'un ensemble ordonné de concepts au sein d'un ensemble de données. Cet ensemble de données, appelé un contexte formel, est composé d'objets décrits par des attributs.
Ce cadre d'analyse est appliqué à différentes tâches, incluant la recherche d'information, la fouille de données ou l'alignement d'ontologies. L'Analyse Relationnelle de Concepts (ARC) est une extension de l'AFC qui prend en compte des ensembles de données composés de multiples relations décrivant des objets de différentes catégories par des attributs ou des liens avec d'autres objets. L'ARC génère une famille de treillis de concepts, exactement un treillis par catégorie d'objets et les concepts de ces treillis sont connectés par des attributs relationnels formés par abstraction des liens initiaux. Cette famille de treillis de concepts est une vue particulière sur les données, qui révèle des règles d'implications entre groupes de liens et des connections entre des groupes d'objets classés d'après leurs liens. Dans cet exposé, nous introduisons l'ARC et nous expliquons ses forces et ses limites. Puis nous donnons des exemples de certaines de ses applications dans différents domaines.

L'évolution logicielle est une pratique importante dans les entreprise qui représente 90% du travail fait sur les systèmes.
Du fait de cette prédominance, il est important de pouvoir proposer des solutions avancées à tous les défis de l'évolution.
C'est le domaine que j'explore dans ma recherche.
J'aborderai particulièrement le cas des "grandes évolutions" comme une restructuration d'un système, ou une migration.
Si ces grandes évolutions arrivent plus rarement, elles mobilisent d'importantes ressources et présentent de ce fait un risque accru.
De plus le fait qu'elles sont moins fréquentes signifie que les développeurs sont moins expérimentés ce qui accroît encore les risques.
Dans cette présentation, je poserais le problème et présenterai deux recherches que nous avons effectuées dans le groupe RMod.

Un des principaux objectifs de l'ingénierie logicielle est l'automatisation de la réutilisation afin de produire des applications de qualité plus rapidement et à moindre coût. L'Ingénierie des lignes de produits logicielles dirigées par les modèles est une approche fournissant des solutions pour réutiliser systématiquement et automatiquement des artefacts génériques durant le développement d'un logiciel. Plus spécifiquement, certaines solutions améliorent la réutilisabilité des artefacts de la ligne de produits en les concevant selon les spécifications de l'Architecture Dirigée par les Modèles. Cependant, les approches existantes se concentrent sur de hauts niveaux d'abstraction qui sont indépendants des plateformes mais fournissent une réutilisation limitée d'artefacts spécifiques à une plateforme donnée. De ce fait, la variabilité spécifique aux plateformes est soit ignorée soit partiellement gérée. Ces limitations interfèrent avec les gains en productivité promis par la réutilisation.
Dans ce séminaire, nous expliquons dans un premier temps l'idée principale de la combinaison de l'Architecture Dirigée par les Modèles avec l'Ingénierie des Lignes de Produits Logicielles. Puis, nous proposons une meilleure compréhension de la variabilité spécifique aux plateformes en identifiant des points de variation dans différents aspects d'un logiciel basé sur la catégorisation du modèle de représentation "4+1". Enfin, nous proposons de gérer intégralement la variabilité spécifique aux plateformes en construisant le Modèle Spécifique aux Plateforme d'une application avec deux sous-modèles : le Modèle Transverse obtenu par transformation du modèle de l'application de plus haut niveau d'abstraction et le Modèle de Structure d'Application obtenu par réutilisation d'artefacts variables spécifiques aux plateformes. L'approche a été expérimentée sur deux applications industrielles concrètes. Les résultats obtenus confirment que notre solution améliore de manière significative la productivité d'une ligne de produits.

Product line engineering aims to reduce the cost and effort to develop new related softwares. The migration from existing software variants to a software product line is a valuable but arduous task that necessitates to extract a variability model from descriptions of already developed softwares. We will talk about extracting variability information with FCA and the possibilities offered by FCA extensions in product line reverse engineering.

Theorem provers have now become very big pieces of code, implementing complex algorithms in an efficient manner, and relying on various optimizations to achieve great results. However, this means that there is no guarantee that their results are correct. The easiest way to overcome that problem is to output formal verifiable proofs, but there unfortunately, there exists only very few provers that acutally do that. We will talk about how formal proof output was achieved in the mSAT SAT solver, and the derived ArchSat SMT solver.

Dans cet exposé, nous allons présenter Zipperposition, un outil de déduction automatique pour la logique du premier ordre basé sur la superposition. Cet outil a été étendu à la Déduction modulo théorie, qui permet de transformer les axiomes d'une théorie en calculs (règles de réécriture), et qui permet par là-même d'améliorer la recherche de preuve. Nous allons ensuite décrire la théorie des ensembles de la méthode B (une méthode formelle industrielle basée sur la preuve en particulier) exprimée comme une théorie adaptée à la Déduction modulo théorie (en transformant les axiomes en règles de réécriture quand c'est possible). Enfin, nous allons donner quelques résultats expérimentaux obtenus sur plus de 300 problèmes de théorie des ensembles, qui font partie de la formalisation ensembliste de la méthode B (Chapitre 2 du B-Book)

GIST, pour Graine d'Information et Schéma de Transformation, est une nouvelle approche d'organisation de l'information.
Elle positionne la gestion de l'information à l'interface entre la data (approche machine) et le document (approche humaine).
Elle préserve et ouvre les degrés de liberté dans le traitement de l’information, en s'appuyant sur la mise en relations de Graines d'Information.
Les Graines d'information sont des unités sémantiques holoniques.
Prioritairement manipulables par l'humain, elles appellent des possibilités d'assistance algorithmique, à partir d'un langage en cours de définition.
GIST permet de modéliser "ki-fé-koi" avec 11 types de graines et 3 types de relations. La modélisation est compatible avec schema.org.
Les usages sont multiples, à titre d'exemple : représentation des compétences et de l'activité d'un réseau d'acteurs, veille technologique, gestion de projets...
Après un premier prototype, GIST a été implémenté début 2017 dans une application web mobile (iOS et Android) pour le réseau Apidae tourisme (régions Auvergne Rhône Alpes, PACA).
Conduit selon l'approche du "Design thinking", le projet intègre 4 systèmes : représentation, accompagnement, action et évaluation.
Dans sa première version, l'application suppose l'appartenance au réseau Apidae, mais elle sera prochainement accessible à tous, gratuitement, en Open Source.
L'exposé est proposé en 4 parties :
- introduction sur la genèse des Graines d'information
- présentation illustrée avec l'application ApiApp
- caractéristiques et potentiel de GIST
- axes de recherche en cours

This talk will present the approach we are following in order to sketch out a high level view of a software code base. The general idea is to explore the many incremental changes that are archived in the version control system (svn, git, ...) in order to combine the time dimension with the spatial one (software structure represented as a graph). We want to characterize the stream of changes that composes the software rather than one of its specific state in time.

The general idea is to consider the source code base as a regular data set and explore it with through a data mining perspective. In the end we want to generate a synthetic view (dashboard) that helps to understand the project and make business decisions without being necessarly knowledgeable in software development.

This is the second part of the talk.
In the first part, we presented an approach for recovering layered views of existing software systems. We re-examined the layered style to extract a set of fundamental principles which encompass a set of constraints that a layered system must conform to at design time and during its evolution. These constraints are used to guide the recovery process of layered architectures. In particular, we translate the problem of recovering the layered architecture into a quadratic assignment problem (QAP) based on these constraints, and we solve the QAP using a heuristic search algorithm. We presented and discussed the results of the experimentation with the approach on four open source software systems.
In this second part, we will present an approach that supports the understanding of software evolution at the architectural level. This approach relies on the idea that an architectural tactic can be mapped to a number of operational representations, each of which is a transformation described using a set of elementary actions on source code entities. These operational representations make it possible to:
1) detect architectural tactics’ application (or cancellation) by analyzing different versions of the source code of analyzed systems
2) understand the architectural evolution of these systems.
We will present the results of our approach through the analysis of the evolution of an open source software system.

This talk will be organized into two parts. In the first part, we will present an approach for recovering layered views of existing software systems. We re-examine the layered style to extract a set of fundamental principles which encompass a set of constraints that a layered system must conform to at design time and during its evolution. These constraints are used to guide the recovery process of layered architectures. In particular, we translate the problem of recovering the layered architecture into a quadratic assignment problem (QAP) based on these constraints, and we solve the QAP using a heuristic search algorithm. We will present and discuss the results of the experimentation with the approach on four open source software systems.
In the second part, we will present an approach that supports the understanding of software evolution at the architectural level. This approach relies on the idea that an architectural tactic can be mapped to a number of operational representations, each of which is a transformation described using a set of elementary actions on source code entities. These operational representations make it possible to:
1) detect architectural tactics’ application (or cancellation) by analyzing different versions of the source code of analyzed systems
2) understand the architectural evolution of these systems.
We will present the results of our approach through the analysis of the evolution of an open source software system.

L'Ingénierie des Systèmes (IS) est une approche pluridisciplinaire et collaborative pour structurer et mener à bien la conception puis le développement de systèmes complexes. L’IS promeut à la fois une approche processus éprouvée et la mise en œuvre de modèles en cours de conception faisant alors apparaître l’Ingénierie Système Basée sur des Modèles (ISBM ou Model-Based Systems Engineering - MBSE). Les modèles permettent, d’une part, de représenter et de communiquer sur le système en cours de conception vu à différents stades de maturité, selon plusieurs points de vue, voire quelquefois en se focalisant sur un aspect tel que la performance par exemple. Des langages de modélisation dit « métier » (Domain Specific Modelling Languages ou DSML) sont spécifiquement créés pour fournir ces modèles. D’autre part, les modèles doivent permettre autant que possible à toutes les parties prenantes de vérifier et de valider que le système, tel qu’il est représenté, répond à leurs attentes par exemple en termes de sûreté de fonctionnement, de coûts de production et d'utilisation ou de disponibilité. Afin de pouvoir utiliser ces modèles en confiance pour atteindre ce deuxième objectif, il est d’abord nécessaire de s’assurer de leurs qualités respectives e.g. de leur cohérence, du fait que certains principes ou règles de modélisation propres à un point de vue ont bien été respectées ou encore de leur pertinence au regard du système en cours de conception. Pour cela, la vérification et la validation (V&V) sont deux processus cruciaux en ISBM. Ils supportent et interagissent fortement avec les processus dits de conception puis de développement et de déploiement éventuel du système. Leur rôle est à la fois de s’assurer des qualités attendues des modèles mais aussi de fournir des justifications aux activités de décision et de choix en cours de conception. Il faut donc pouvoir disposer ici de DSML qui faciliteraient alors la mise en œuvre de ces activités de V&V. Pour cela, un DSML possède une syntaxe et une sémantique. La sémantique est généralement fournie via des approches formelles externes, en se basant sur des techniques de transformations. Ces dernières sont, à notre sens, une limitation pour le déploiement des stratégies de V&V dans le contexte de l’ISBM. En réponse à cette limitation, nous proposons un nouveau langage de méta-modélisation nommé xviCore (noyau exécutable, vérifiable et interopérable) permettant la conception et la V&V des langages de modélisation métier (DSMLs) et des modèles qui sont faits avec. xviCore fournit les concepts et les principes pour définir puis vérifier et valider la syntaxe et la sémantique en phase de construction de tels DSML. xviCore combine trois métalangages : un métalangage orienté objet pour décrire la syntaxe des DSMLs avec un métalangage de comportement et un métalangage des propriétés formelles pour décrire la sémantique des DSMLs. xviCore permet la mise en place d’une stratégie de V&V «directe» en lieu et place des approches externes. Elle est basée d'une part sur la simulation (l'interprétation ou exécution des modèles) et d'autre part sur la vérification de propriétés formelles. Concernant l'outillage, nous proposons une implantation du métalangage xviCore complet dans l'environnement Eclipse sous la forme d'un ensemble de plugins.

pré-soutenance de HDR : les langages à base de composants dans le génie logiciel ; la soutenance HDR est prévue le 8/11

Cette présentation traite des langages de modélisation exécutables, parfois appelés iDSML ou xDSML. Après avoir rappelé leur définition et leurs rôles dans le développement d’applications, cette présentation s’intéressera à leur utilité pour aborder la problématique de l’adaptation logicielle dynamique.

La programmation orienté composants permet de répondre en partie aux
problématiques de réutilisabilité et de maintenance de programme
auxquelles l'industrie du logiciel fait face. Dans cet exposé, nous
allons aborder la programmation orientée composant du point de vue
formel : nous verrons comment donner une sémantique formelle des
instructions clé de COMPO, en insistant plus particulièrement sur le
passage de paramètres. Nous présenterons également un typage statique
pour COMPO qui a la particularité d'être correct vis-à-vis de la
sémantique. Ces travaux vont dans le sens d'un langage sûr et ont
conduit à l'écriture d'un interpréteur certifié pour le noyau non
réflexif de COMPO.

Dependent type theories have proven to be useful in several fields including,
for example, formalisation of mathematics (c.f., recent development in homotopy type theory), interactive theorem proving (c.f., proof assistants), and computational linguistics
(c.f., formal linguistic semantics).
In this talk, I shall first give a brief and gentle introduction to type theory
and then discuss some recent work in its development and applications.

L'exposé traitera de l'orchestration automatisée de services, prenant en en compte les évolution des APIs, dans un écosystème dédié (par exemple ici saleforce.com) avec des services manipulant un même système d'information global matérialisé par des bases réelles différentes (donc avec une problématique de bases de données hétérogènes).

Service Oriented Architecture (SOA) is an architectural design paradigm which facilitates composing flexible and reusable service-oriented assets. Before the advent of SOA, several software systems were developed using older technologies. It is advantageous to modernize those software systems towards service-based ones. In this sense, I will present a service identification and packaging approach based on a service quality measurement model.
Besides, one of the most distinguishing features of a service-oriented application is the ability to dynamically reconfigure and adjust its behavior to cope with changing environment during execution. To tackle this issue, I will present an Architecture Description Language (ADL) called DSOPL-ADL that describes a variant-rich service-based architecture in which dynamic reconfigurations are specified at architecture level. Moreover, the description is enriched with context and variability information, in order to enable a variability-based self-reconfiguration of architecture in response to context changes at runtime.

La composition de services web avec prise en compte de la QOS incertaine est l’une des problématiques majeures du calcul orienté service (SOC). En effet, la fluctuation permanente des performances des services web, complique de plus en plus la tâche de sélection des compositions optimales. De ce fait, nous ferons recours à des approches non déterministes pour gérer et modéliser les critères de QOS incertains. Dans ce travail, nous présentons trois heuristiques pour sélectionner les Top-k compositions dominantes. La première est articulée sur le concept skylines probabilistes, la deuxième solution se base sur la notion des skylines P-dominants, et la troisième approche se base sur les skylines fuzzy-dominants. Une étude empirique est présentée pour évaluer les performances de chaque heuristique.

La droite d'Harthong-Reeb est un modèle numérique du continu basé sur les entiers. La construction de cette droite en utilisant les $\Omega$-entiers permet de décrire les objets mathématiques réels de manière discrète et constructive.
En informatique graphique, on est souvent amené à transformer des objets (images) par des applications affines réelles (rotations, translations, similitudes...). Des discrétisés (à une échelle donnée) de ces applications, appelées applications quasi-affines ont été définies et étudiées. Nous présentons la formalisation en Coq du cadre numérique permettant la modélisation de ces applications et l'établissement de certaines de leurs propriétés de base.

Automated semantic web service composition is one of the critical research challenges of service-oriented computing, since it allows users to create an application simply by specifying the inputs that the application requires, the outputs it should produce, and any constraints it should respect. The composition problem has been handled using a variety of techniques, from Artificial Intelligence (AI) planning to optimization algorithms. However no approach so far has focused on handling three composition dimensions simultaneously, producing solutions that are: (1) fully functional (i.e. fully executable) by using a mechanism of semantic matching between the services involved in the solutions, (2) are optimised according to non-functional Quality of Service (QoS) measurements, and (3) respect global QoS constraints. This paper presents a novel approach based on a Harmony Search (HS) algorithm that addresses these three dimensions simultaneously through a fitness function, to select the optimal or near optimal solution in semantic web service composition. In our approach, the search space is modeled as a Planning Graph structure which encodes all the possible composition solutions for a given user request. An experimentation of the approach conducted with an extended version of the Web Service Challenge 2009 dataset showed that our approach is efficient and effective to extract the optimal or near optimal composition in diverse scenarios.

Chercheur à l’IMS UMR 5218 à l'Université de Bordeaux, j’ai développé une expertise en modélisation et simulation de systèmes complexes et en ingénierie des systèmes dirigée par les modèles. J’ai co-encadré des travaux sur la modélisation de systèmes complexes et leurs transformations en modèles exécutables (simulation DEVS/HLA, appel de services). Je m’intéresse par ailleurs à la découverte de modèles à partir de systèmes existants obsolètes dans le cadre de processus de réingénierie. J’ai également développé des travaux en appariement de modèles, par interopérabilité sémantique (matching d’ontologies) dans le cadre du Projet SIMID. Enfin je suis l’initiateur et coordinateur d’une plateforme de simulation de réseaux sociaux multidimensionnels.

Dans cette présentation, je détaillerai tout d’abord la partie des travaux sur l’interopérabilité sémantique. Plus précisément, ces travaux s'insèrent dans le cadre de recherches pour le « Model Driven Engineering ». En particulier ceux que j’ai effectués sur la transformation de modèles par « matching » de Meta modèles et les transformations ATL s’intègrent avec les travaux d’ingénierie des modèles. Ces travaux de « matching » d’ontologie basés sur une combinaison de « matchers » syntaxiques, lexicaux et sémantiques peuvent apporter un complément aux approches de « mining ». Enfin je présenterai les travaux utilisant la simulation pour : 1. Redécouvrir le processus informationnel de systèmes obsolètes et 2. Observer le comportement des modèles de réseaux sociaux que je mène actuellement à l’IMS.

The Isabelle/HOL proof assistant includes two counterexample generators,
Quickcheck and Nitpick. Quickcheck started as a clone of the original
QuickCheck for Haskell, whereas Nitpick is based on finite model
finding. Nitpick suffers from three main limitations: (1) It is too tied
to its frontend (Isabelle/HOL); (2) it is too tied to its backend
(Alloy/Kodkod); (3) it is often imprecise (i.e., it fails to find some
countermodels).
Nunchaku is a complete rewrite of Nitpick as a stand-alone OCaml tool.
It has a rich input syntax, with polymorphic higher-order logic,
(co)datatypes, (co)inductive predicates, (co)recursive functions, and
will support other features such as quotient types. An Isabelle
frontend already exists, and work will soon commence on frontends for
Coq (based on type theory), the TLA+ Proof System (based on set theory),
and other proof assistants. The SMT solver CVC4 is used as a backend,
but the modular architecture will make it possible to try out other
backends (e.g. Alloy/Kodkod, Paradox, Vampire). More precise
approximation domains, notably for higher-order functions, will increase
the precision. Nunchaku already implements numerous encodings to lower
the input formulas closer and closer to the SMT language, and features
a clean, modular architecture.

The Web service selection process is not a trivial task, because of the increasing number of Web services on Internet. Non-functional (Quality of Service) characteristics are frequently used to compare functionally similar Web services, but these attributes, if they are up-to-date, which is not frequently the case, do not reflect the end-user's perception about the service. Some Web service directories present users' feedbacks, as text comments. These are carefully read by developers to get users' perception about services. These feedbacks represent thus a good indicator of the (subjective) quality of a given service. In order to avoid the long and tedious task of searching and analyzing users' feedbacks, in this work, we propose a method to automatically assessing an approximation of the quality of Web services from these feedbacks. This method text-mines the comments of users, representing their feedbacks, to measure the polarity (neutral, positive or negative) and its intensity (very positive or postive, for instance). It aggregates different scores measured on each comment to calculate a global score for a given Web service. Compared to existing works, this method takes into consideration complex text structures (adjective phrases, for example). Further, additional information (like followers, developers, articles and developed mashups) related to the Web service, collected from the same directories, is used to increase the precision of our method. For validating our work, we conducted an experimentation on a large dataset composed of comments on Web services collected from the ProgrammableWeb API directory.

Cet exposé s'adresse essentiellement aux curieux qui veulent comprendre sur des exemples simples les différents principes cachés derrière la preuve de programme.

Les doctorants de première année parlent de leurs travaux de thèse !

• Jessie Carbonnel : Etude exploratoire de la variabilité dans les lignes de produits par Analyse Relationnelle de Concepts
• Anthony Ferrand : Etude des applications hybrides sur plateforme mobile
• Anfel Selmadji : D'une application à objets vers une application à composants pour une exécution sur le cloud
• Frédéric Verdier, ACELYS : Réutilisation et Adaptation de Modèles dans une Démarche de Développement Basée sur la Représentation et la Gestion de la Variabilité
• Soumia Zellagui : Réusinage de code d'applications à objets pour un meilleur découplage

Après avoir rappelé les principaux concepts des systèmes cyber-physiques (automates hybrides) et leurs enjeux, nous tentons d'analyser les conditions dans lesquelles ce thème scientifique et technique pourrait être enseigné dans les formations d'informatique de l'université de Montpellier ; parmi les points abordés :
- quels thèmes étudier, avec quels publics et quels niveaux de formation
- quels objectifs pour nos étudiants
- dispose-t-on des compétences pour assurer les enseignements
- quels intérêts pour nos disciplines de recherche

le support pdf de la présentation

Dans cet exposé, nous discuterons des sémantiques formelles pour les langages de programmation. En particulier, nous nous intéresserons aux sémantiques opérationnelles, plus proches de l'implantation, et nous introduirons notamment, pour l'exemple, un petit langage dont nous donnerons la sémantique opérationnelle naturelle (dite "à grands pas"). Enfin, nous évoquerons la mécanisation de la formalisation de ces sémantiques en utilisant l'outil d'aide à la preuve Coq, qui nous permettra non seulement de raisonner sur ces sémantiques, mais aussi d'en extraire des interprètes certifiés.

Modelling component behaviour and system architectures of software intensive systems is widely recognised as a complex task during the specification and design phases, especially for critical and reactive systems. In order to tackle these issues, we propose an incremental development framework which helps designers to identify and to verify model development states and development steps. Development states are model observation points, while development steps define the type of development applied between two states which can be of two types: enrichment or refinement. A set of verification techniques is associated to the development of models in order to guarantee that the current model conforms to the model obtained during the previous step. Conformance relations are based on the analysis of liveness properties. They have been implemented in a tool named IDCM. The incremental development and verification of UML models is formalised by a UML profile (FINE) and is supported by a tool.

Large object-oriented applications have complex and numerous dependencies, and usually do not have explicit architectures. Therefore they are hard to maintain, and parts of them are difficult to reuse. Component-based development paradigm emerged for improving these aspects and for supporting effective maintainability and reuse. It provides better understandability through a high-level architecture view. Thereby migrating object-oriented applications to component-based ones will contribute to improve these characteristics. In this paper, we propose an approach to automatically transform object-oriented applications to component-based ones. More particularly, the input of the approach is the result provided by software architecture recovery: a component-based architecture description. Then, our approach transforms the object-oriented source code in order to produce deployable components. We focus in this paper on the transformation of source code related to instantiation and inheritance dependencies between classes that are in different components. We experimented the proposed solution in the transformation of a collection of Java applications into the OSGi framework. The experimental results are discussed in this paper.

More information about this paper can be found at:
http://2015.gpce.org/event/gpce2015-migrating-large-object-oriented-applications-into-component-based-ones-instantiation-and-inheritance-transformation

edukera est une application en ligne permettant de résoudre des exercices
de mathématiques. Sa réalisation a nécessité la mise en place d'une
interface web ergonomique d'élaboration de raisonnements, ainsi que
l'intégration du moteur de logique formelle COQ.

La présentation abordera plusieurs aspects du sujet :
démonstration de l'application
architecture technique de l'application
considérations pédagogiques (retours d'expérience en universités)

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

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.

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.

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.

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.

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.

Le développement de logiciels surs 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.

(Ce séminaire aura un repetita le mardi 9/11/15 à 11h30)

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.

(Ce séminaire aura un répétita mardi 10/11/15 à 11h)

Le développement de logiciels surs 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.

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.

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).

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.

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.

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.

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.

Le Web des objets nous promet l'émergence de systèmes cyber-physiques reposant sur les langages et protocoles du Web pour interconnecter un très grand nombre d'objets hétérogènes et fournir de manière autonome des applications à forte valeur ajoutée. En effet, les technologies du Web, l'informatique orientée services et les langages du Web sémantique ont facilité les échanges de machine à machine.
Cependant, l'utilisation conjointe des dispositifs physiques et des données qu'ils produisent dans le Web présente encore de nombreux enjeux, liés aux problèmes d'interopérabilité, de respect de la vie privée et aux différences fondamentales, en particulier au niveau architectural, entre les technologies du Web et les objets connectés.

Dans ce séminaire, nous effectuerons un tour d'horizon des principaux enjeux actuels, avant de présenter quelques contributions relatives au besoin d'interopérabilité et au respect de la vie privée lors des échanges de données entre objets connectés, contributions qui s'inscrivent dans une architecture logicielle permettant d'établir le lien entre les objets connectés et le Web. À partir de ces contributions nous dégagerons plusieurs perspectives de recherche.

Dans cette présentation j'aimerais réfléchir à la notion d’évaluation de la recherche que nous produisons et aussi en premier lieu du chercheur. Les évaluations auxquelles nous participons prennent-elles reellement en compte la complexité du fait d’avoir comme résultats autre chose que des articles.
Quelle notion d’impact devons nous prendre et avons-nous conscience du coût et de la valeur d’avoir des utilisateurs réels?
Dans l’équipe RMOD nous accordons de la valeur à produire des artefacts que des gens normaux utilisent.
Nous développons Moose (http://www.moosetechnology.org, an open-source meta described reengineering platform) et Pharo (http://www.pharo.org, a new open-source Smalltalk-inspired language and IDE).
Je présenterai un panorama des travaux de recherche en cours sur ces deux plateformes.

Stéphane Ducasse est directeur de recherche Inria et dirige l'équipe RMOD (http://rmod.inria.fr/).
Ses travaux de recherche portent sur la conception et les langages à objets, les langages et machines virtuelles réflexives,
la maintenance et l'évolution de large applications (visualisation, métriques, MDE). Il a notamment développé le concept de "trait" introduit dans de nombreux langages opérationnels (AmbientTalk, Pharo-Smalltalk, Perl-6, PHP 5.4, Ruby et JavaScript).
Il est un des développeurs de Pharo (http://www.pharo.project.org/) un langage open-source inspiré de Smalltalk et de Moose une plate-forme de re-engeneering multi-langages (http://www.moosetechnology.org/). Il est un des fondateurs de la start-up Synectique (http://www.synectique.eu).

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.

Dans cet exposé en deux parties, nous présenterons tout d'abord 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. Dans une seconde partie, nous parlerons de la formalisation du langage de description d'architectures basé sur les composants Dedal en utilisant la méthode B. Ce langage repose sur une approche en trois niveaux d'abstraction (spécification, implantation, et déploiement), et nous montrerons comment le raffinement de la méthode B permet de modéliser très directement les relations entre ces trois niveaux. Nous verrons également sur un exemple comment l'outil de déduction automatique de l'Atelier B se comporte, et comment on pourrait l'améliorer en utilisant la plate-forme de preuve réalisée dans le cadre du projet ANR BWare.
(Travaux réalisés en commun avec :

• C. Dony, C. Tibermacine, pour la 1ère partie ;
• A. Mokni, M. Huchard, C. Urtado, S. Vauttier, pour la 2ème partie.)