L'évolution de l'Internet comme support de communication entre les applications et les organisations a révolutionné les méthodes de coopération classiques. Les technologies réseaux actuelles, notamment les services Web, permettent le développement de nouveaux paradigmes de coopération. En effet, les entreprises peuvent dans un premier temps externaliser leurs procédés métiers comme des services Web pour former dans un deuxième temps ce qu'on appelle une entreprise virtuelle par compositions de services externalisés. Mais, comme souvent en informatique, ce qui est supposé apporter de la facilité apporte aussi son lot de complexité et de questions. Cela va de la pertinence des langages utilisés pour décrire les compositions de services, leur formalisation, leur vérification formelle avant et après l'exécution, au problème de maintenir une qualité de services constante. L'objectif de cette thèse est de proposer une approche rigoureuse pour la spécification, la modélisation, la vérification et la validation des compositions de services Web. Le travail effectué a permis la mise en place de techniques de preuves pour les services Web pour répondre à de nouveaux challenges liés essentiellement à la composition et la vérification. L'approche développée consiste en : (i)la définition d'un langage de spécification de la composition pour assurer sa vérification formelle, (ii) l'extension du langage de composition transformé pour prendre en compte les aspects de communication entre des compositions différentes, (iii) l'extraction et la spécification des propriétés à vérifier avant et après l'exécution de la composition, (iv) la vérification de la composition (vérification a priori et vérification a posteriori), et (v) l'utilisation des spécifications des déviations détectées pour découvrir des services qui peuvent tomber en panne ou devenir indisponibles en cours d'exécution. / The proliferation of the Internet as a communication medium between applications and organizations has revolutionized the classic methods of cooperation. The current network technologies, including Web services, allow the development of new paradigms of cooperation. Indeed, enterprises can outsource their business processes as Web services to form what is called a virtual enterprise by compositions of outsourced services. However, as so often in computer science applications, which is supposed to bring the facility provides also its set of complexity and questions. This covers the relevance of the language used to describe the compositions of services, their formalizations, their formal verification before and after running the composition process, and the need of maintaining a constant quality of services. The aim of this dissertation is to develop a rigorous approach to specifying, modelling, verifying and validating the behaviour of Web service compositions with the goal of simplifying the task of designing coordinated distributed services and their interaction requirements. More precisely, we have proposed a semantic framework that provides a foundation for addressing the existing limitations in the context of Web services compositions by supporting the following functionalities: (i) to formally specify requirements for BPEL processes. The requirements specify behavioural properties of the composition process, or assumptions about the behaviour of the composition as a whole and its constituent services, (ii) to extend the approach to include models of service choreography with multiple interacting Web services compositions, from the perspective of a collaborative distributed composition development environment, (iii) to verify these requirements against process executions. The requirements verification can be done either a-priori, i.e., at design time, or a-posteriori, i.e., after runtime, (iv) to use the specifications of the violated requirements to generate queries for discovering services that could substitute for malfunctioning services or services that may become unavailable or fail to meet certain requirements.

Alors que les études effectuées sur la biosynthèse de l’amidon ont permis,depuis une vingtaine d’années, une compréhension approfondie de ce mécanisme,les travaux sur la dégradation sont aujourd’hui assez peu développés et restreintsessentiellement au modèle de l’amidon transitoire chez Arabidopsis thaliana chez quiune approche de génétique inverse est mise en oeuvre. Dans ce contexte, nousavons entrepris une démarche complémentaire de génétique formelle chezChlamydomonas reinhardtii, organisme modèle permettant l’étude du métabolismede l’amidon transitoire et de réserve, dans le but d’identifier de nouvelles fonctionsnotamment impliquées dans la régulation du processus catabolique. L’applicationd’un crible à l’iode en deux étapes a permis l’isolement de 62 souchespotentiellement déficientes pour la dégradation de l’amidon parmi plus de 32000transformants. L’identification des gènes touchés a mis en évidence des fonctionsdéjà caractérisées chez le modèle Arabidopsis, telles que les protéines Mex, Bam1et Dpe2, confirmant ainsi la force du crible et validant la démarche entreprise. Lacaractérisation d’autres mutants nous permet d’envisager l’identification de nouvellesfonctions impliquées dans la dégradation de l’amidon ou dans la régulation de ceprocessus chez les végétaux. En parallèle, la caractérisation de la granulométrie desamidons produits par nos mutants augure également de la découverte de fonctionsimpliquées dans le déterminisme de la taille des grains d’amidon. / Starch biosynthesis has been widely studied for more than twenty years andthe understanding of this process is now quite complete. Meanwhile, studies onstarch catabolism have mainly been restricted to one single organism, Arabidopsisthaliana, a plant model for transitory starch metabolism studies through reversegenetics. We then decided to apply a complementary forward genetics approach inthe unicellular microalga Chlamydomonas reinhardtii in order to decipher thecatabolism of both transitory and storage starches. Using random mutagenesis and atwo-step iodine screening, we were able to isolate 62 putative catabolic mutantsamong more than 32000 insertional transformants. The localization of the foreignDNA insertion sites allowed the identification of mutations for key catabolic activitiessuch as Mex, Bam1 and Dpe2, which were already described in Arabidopsis,revealing the strength of our phenotypic screening procedure. The preliminarycharacterizations performed on the other mutants defective for previouslyuncharacterized functions may define new functions affecting starch catabolism orregulation of this process in microalgae. . Some of these mutants are also harboringaltered size distributions of their starch granules and may represent a valuablematerial for understanding the mechanisms controlling the starch granule sizesdetermination in Chlamydomonas reinhardtii.

Les ontologies sont diversement employées notamment dans les domaines du Web sémantique, de l’ingénierie des connaissances, … En effet, elles permettent de partager, de diffuser et d’actualiser les connaissances d’un domaine. Afin de construire ces ontologies, notre méthodologie utilise tout d’abord des méthodes de Traitement Automatique de la Langue Naturelle (TALN) et d'Extraction d'Information (IE) pour extraire des données préparées à partir de chaque ressource du domaine (corpus de textes, bases de données, thesaurus). Puis, ces données sont fouillées avec les méthodes de fouilles : l'Analyse Formelle de concepts (AFC) et l’Analyse Relationnelle de Concepts (ARC). L'AFC regroupe des objets partageant les mêmes attributs binaires dans des concepts d'un treillis. L'ARC est une extension de l'AFC qui permet de regrouper des objets partageant les mêmes attributs binaires, mais aussi les mêmes attributs relationnels. L’apposition de contextes (une propriété de l’AFC) permet d’associer ces attributs (binaires et relationnels) à un ensemble de classes prédéfinies et hiérarchisées par les experts du domaine. De cette façon, des définitions étendues sont proposées aux experts du domaine pour ces classes prédéfinies ainsi que de nouvelles classes inexistantes dans la hiérarchie initiale. Ces nouvelles classes peuvent être considérées pertinentes et ajoutées par les experts en tant que nouvelles « unités de connaissances ». Les treillis résultant des méthodes de fouille constituent ce que nous appelons schéma d’ontologie. Ce schéma d’ontologie est ensuite représenté par le langage FLE de la famille des logiques de descriptions afin d’avoir une ontologie. Cette ontologie, implémentée en OWL (Web Ontology Language), a permis à notre système de répondre automatiquement à différentes questions proposées par les experts du domaine (instanciation de concepts, comparaison de concepts,…). Des expériences pratiques ont été menées dans deux domaines d'application que sont l'astronomie et la microbiologie. / Ontologies are used in different fields like the semantic Web or the knowledge engineering. The ontologies allow to share, to diffuse and to update knowledge domain. This thesis propose a methodology to build ontologies using methods of Natural Language Processing (NLP) and Information Extraction (IE) for extracting prepared data from each kind of available resources in the domain (text corpora, databases, thesaurus). Then, these prepared data are mining with the mining methods : Formal Concepts Analysis (FCA) and Relational Concepts Analysis (RCA). The FCA regroups a set of objects sharing the same set of attributes in the same concept. The RCA, an extension of the FCA regroups a set of objects sharing the same attributes and the same relations (relational attributes) in the same concept. The apposition of contexts, a property of the FCA, affects a set of attributes and relational attributes to classes pre-defined and hierarchised by the domain experts. These affectations allow us to present classes and their definitions to the experts of domain as well as new nonexistent classes in the initial hierarchy. These new classes can be considered appropriate and added by experts as new « knowledge units ». The Lattices resulting from the data mining methods are considered as « ontology schema ». This ontology schema is represented in the FLE description logics language to obtain ontology. This ontology is implemented in the OWL language (Web Ontology Language) for allowing us to request it. This methodology was tested in different domains: Microbiology and Astronomy.

A cause de la complexité croissante des systèmes sur puce (SoC), la vérification devient un aspect très important : 70 - 80% du coût de conception est alloué à cette tâche. Plus de 60% des projets de développement d'ASIC doivent être repris à cause des erreurs fonctionnelles, environ 50% des erreurs de conception étant situées au niveau du module. Dans le monde industriel, la vérification est souvent synonyme de simulation - une méthode de vérification naturelle pour les concepteurs, mais qui ne garantit pas l'absence d'erreurs. Une alternative est fournie par la vérification formelle qui prouve mathématiquement qu'un circuit satisfait une spécification. Dans cette thèse, on s'intéresse aux méthodes déductives basées sur la démonstration de théorèmes. La démonstration de théorèmes permet de vérifier formellement des descriptions matérielles de haut niveau et des systèmes réguliers ou très complexes, car la taille de données n'a plus d'importance. Par contre la modélisation de la description matérielle se fait directement en logique, ce qui rend l'accès difficile pour les concepteurs. Notre travail a pour but de faciliter l'introduction des outils de démonstration de théorèmes dans le flot de conception. Nous proposons une méthode automatique de traduction d'un circuit VHDL vers un modèle sémantique basé sur des équations récurrentes par rapport au temps qui peut être l'entrée de tout outil de démonstration de théorèmes et nous définissons une approche de vérification adaptée au modèle. Afin de valider notre proposition, nous avons choisi le démonstrateur ACL2 pour vérifier une bibliothèque de circuits de cryptographie.

Pour satisfaire la demande du marché actuel, plusieurs outils commerciaux de vérification formelle sont apparus ces dernières années. Le niveau le plus abstrait de description accepté dans la plupart de ces outils est le niveau appelé transfert de registres, c'est-à-dire une description avec des cycles d'horloge explicitement définis. Pour rester compétitifs, néanmoins, les concepteurs sont obligés d'élever le niveau d'abstraction et commencent à utiliser des outils de synthèse de haut niveau. Cette thèse a pour objet la vérification formelle des résultats de synthèse de haut niveau par rapport à la spécification initiale décrite en VHDL. Nous proposons une méthodologie de vérification qui épouse le flot de conception et consiste en la vérification de deux étapes principales:<br />l'ordonnancement et l'allocation. La vérification de chaque étape est fondée sur un modèle de machine abstraite que nous avons défini: contrairement au modèle de machine d'états finis classique, il réduit<br />considérablement l'espace d'états d'où les registres de la partie opérative sont exclus. En outre, la machine abstraite est similaire aux descriptions VHDL utilisées lors de la synthèse et offre, par conséquent, un niveau d'abstraction plus élevé de représentation des<br />circuits. La preuve d'équivalence entre la machine abstraite et la machine d'états finis classique justifie la première et constitue une des contributions théoriques de la thèse. Un prototype d'outil basé sur la simulation symbolique a été développé et exécuté sur des benchmarks de la synthèse comportementale. La thèse<br />s'achève sur les problèmes ouverts et les axes de recherche à explorer.

Le disque compact mentionné dans le texte n'est pas disponible en ligne. Il se trouve seulement dans la version imprimée.

Reproduction de : Thèse de doctorat : Education : Lyon 2 : 2002. / Thèse : 2002LYO20040. Titre provenant de l'écran-titre. Bibliogr. Index.

Nous etendons les logiques temporelles du temps alternant ATL et ATL* au moyen de contextes strategiques et de contraintes sur la memoire : la premiere extension permet aux agents de s'en tenir a leurs strategies lors de l'evaluation des formules, contrairement a ATL ou chaque quantificateur de strategies ecrase les strategies anterieurement selectionnees. La seconde extension permet aux quantificateurs de strategies de se restreindre aux strategies sans memoire ou avec memoire bornee. Nous avons l'etudie l'expressivite de nos logiques. Nous montrons qu'elles expriment des proprietes importantes comme l'exstence d'equilibres, et nous les comparons formellement a d'autres formalismes proches (ATL, ATL*, Game Logic, Strategy Logic, ...). Nous avons aborde les problemes de model-checking. Nous donnons un algorithme PSPACE pour la logique n'impliquant que des strategies sans memoire, et un algorithme EXPSPACE pour le cas des strategies a memoire bornee. Dans le cas general, malgre leur forte expresssivite, nous prouvons que leur model-checking reste decidable par un algorithme a base d'automates d'arbres alternants qui permet d'evaluer une formule sur la classe complete des CGS avec n joueurs. / We extend the alternating-time temporal logics ATL and ATL* with strategy contexts and memory constraints: the first extension make agents commit to their strategies during the evaluation of formulas, contrary to plain ATL where strategy quantifiers reset previously selected strategies. The second extension allows strategy quantifiers to restrict to memoryless or bounded-memory strategies. We consider expressiveness issues. We show that our logics can express important properties such as equilibria, and we formally compare them with other similar formalisms (ATL, ATL*, Game Logic, Strategy Logic, ...). We address the problem of model-checking for our logics, especially we provide a PSPACE algorithm for the sublogics involving only memoryless strategies and an EXPSPACE algorithm for the bounded-memory case. In the general case, despite the high expressiveness of these logics, we prove that their model-checking problems remain decidable by designing a tree-automata-based algorithm for model-checking ATLsc on the full class of n-player concurrent game structures.

La méthodologie HILECOP a été élaborée pour la conception formelle de systèmes numériques complexes critiques ; elle couvre donc l'intégralité du processus, allant de la modélisation à la génération de code pour l’implantation sur la cible matérielle (composant électronique de type FPGA), en passant par la validation formelle. Or, si le modèle formel, les réseaux de Petri en l'occurrence, est par essence asynchrone, il est néanmoins exécuté de manière synchrone sur la cible. De fait, les approches d'analyse usuelles ne sont pas adaptées au sens où elles construisent des graphes d'états non conformes à l'évolution d'états réelle au sein de la cible. Dans l'objectif de gagner en confiance quant à la validité des résultats de l’analyse formelle, ces travaux visent à capturer les caractéristiques dites non-fonctionnelles, à les réifier sur le modèle et enfin à considérer leur impact à travers l’analyse. En d’autres termes, l’objectif est d’améliorer l’expressivité du modèle et la pertinence de l'analyse, en considérant des aspects comme la synchronisation d'horloge, le parallélisme effectif, le risque de blocage induit par l'expression conjointe d'un événement (condition) et d'une fenêtre temporelle d'occurrence, sans omettre la gestion des exceptions. Pour traiter tous ces aspects, nous avons proposé une nouvelle méthode d'analyse pour les réseaux de Petri temporels généralisés étendus interprétés exécutés en synchrone, en les transformant vers un formalisme équivalent analysable. Ce formalisme est associé avec une sémantique formelle intégrant toutes les aspects particuliers de l'exécution et un algorithme de construction d'un graphe d'états spécifique : le Graphe de Comportement Synchrone. Nos travaux ont été appliqués à un cas industriel, plus précisément à la validation du comportement de la partie numérique d'un neuro-stimulateur. / The HILECOP methodology has been developed for the formal design of critical complex digital systems; it therefore covers the entire design process, ranging from modeling to code generation for implementation on the hardware target (FPGA type electronic component), via formal validation. However, if the formal model, the Petri nets in this case, is inherently asynchronous, it is nevertheless executed synchronously on the target. In fact, the usual analysis approaches are not adapted in the sense that they construct state graphs that do not conform to the real state evolution within the target. In order to gain confidence in the validity of the results of the formal analysis, this work aims to capture the so-called non-functional characteristics, to reify them on the model and finally to consider their impact through the analysis.In other words, the aim is to improve the expressiveness of the model and the relevance of the analysis, considering aspects such as clock synchronization, effective parallelism, the risk of blocking induced by the expression of an event (condition) and a time window of occurrence, without omitting the management of exceptions.To deal with all these aspects, we have proposed a new method of analysis for extended generalized synchronous executed time Petri nets, transforming them into an analysable equivalent formalism. This formalism is associated with a formal semantics integrating all the particular aspects of the execution and dédicated state space construction algorithm: the Synchronous Behavior Graph.Our work has been applied to an industrial case, more precisely to the validation of the behavior of the digital part of a neuro-stimulator.

Québec Université Laval, Bibliothèque 2016