Actuellement, la technologie des services Web évolue rapidement, en étant soutenue par les grands acteurs du domaine des systèmes d'information. Les applications basés sur services Web sont faiblement couplées et utilisables de façon automatique via l'utilisation d'un ensemble de normes basées sur XML. Hormis la description syntaxique des messages, il est nécessaire d'avoir une description sémantique du comportement des services. En effet, lors de la conception d'un service ou lors d'une composition de services, il est important de vérifier la conformité avec un cahier des charges. L'enrichissement des descriptions des services par l'inclusion de leurs comportements est de plus en plus important. Ce comportement peut être décrit par des protocoles métier représentant les séquences possibles d'échanges de messages. Les services Web utilisent des politiques de contrôle d'accès (ACP) pour restreindre l'accès à des consommateurs autorisés. Ces politiques doivent faire partie de la description du service. Dans cette thèse, l'analyse d'interopérabilité en termes de contrôle d'accès après la formalisation des services Web annotés avec les politiques de contrôle d'accès est réalisée. Nous présentons une approche pour intégrer les outils de vérification dans l'architecture de contrôle d'accès de façon à garantir une interaction sans erreurs. Les politiques et les crédits sont présentés comme une ontologie afin de bénéficier de la flexibilité offerte par subsomption sur des concepts. La chorégraphie des services Web est utilisée dans la phase de conception d'applications pair à pair complexes dans lesquelles chaque pair peut être implémenté par un service Web. Par conséquent, la sélection des services Web pour l'implémentation de chorégraphie en utilisant l'approche de vérification de compatibilité avec contrôle d'accès est l'un des objectifs de notre recherche. Dans ce travail, les modèles de protocole métier du service Web sont étendus en ajoutant des informations au message sur chaque transition du service dans lequel ce message sera envoyé ou reçu. Nous définissons et vérifions la compatibilité des services Web afin de voir si (et comment) plusieurs services peuvent avoir des interactions en fonction de leurs protocoles. Cette approche aidera les concepteurs à choisir des services Web de manière simple et à vérifier s'ils peuvent mettre en œuvre la chorégraphie nécessaire en vérifiant la compatibilité avec notre approche.

Ce travail est une contribution à l'étude du système homme-machine, dont l'avènement est le postulat que l'homme est, d'une certaine manière, contraint de cohabiter avec un partenaire trop discipliné et trop algorithmique. L'homme et la machine sont côte à côte pour gérer et contrôler les systèmes que l'on utilise dans la vie de chaque jour, surtout des systèmes de grandes complexités, où l'état d'esprit "homme-machine" est bien clair. Les activités de l'homme, montrant son rôle et sa place, se matérialisent soit par l'accomplissement du travail que le système technique (machine) est incapable d'accomplir, soit par la surveillance, la récupération d'aléas venant du système technique. A partir de cela, la relation homme-machine devient plus qu'un partenariat, elle se transforme en couple (homme, machine) indissociable, dont la forme et l'organisation sont les garant du bon déroulement du processus de production. Ainsi, l'automatisation des processus industriels devient une sorte de réunion harmonieuse de deux entités pour le bien de tous. Par l'automatisation harmonieuse on entend concevoir des systèmes de plus en plus socio-technique, là où l'homme à sa vrai place. Notre travail s'articule autour d'une vision de conception adéquate des systèmes, homme-machine, qui répond aux exigences d'optimisation des performances de tels systèmes, car la prise en compte de l'élément humain dès l'étape de la conception renforce la stabilité et l'optimalité de toutes les fonctions du système. Cette vision est matérialisée par la proposition d'une méthodologie globale pour la conception et renforcée par une approche de spécification des actions. L'application de cette vision trouve sa place dans le cadre de l'étude de la conception et de la mise en oeuvre d'une cellule de désassemblage en tant qu'un système homme-machine coopératif. Dans ce cadre, deux aspects principaux ont été développés : le premier est le système d'aide à la supervision et à la surveillance, en montrant qu'une construction d'outil d'aide à la conduite passe par l'analyse de comportement décisionnel de l'homme et par la spécification technique et ergonomique des actions du système de supervision et de surveillance. Le deuxième aspect est l'étude du processus d'exécution des tâches robotisées ou partagées avec un robot. Ce travail se justifie par un certain besoin de connaître davantage et de connaître différemment dans un esprit de mieux faire.

L'objectif de cette thèse est de profiter des avantages de deux formes de modélisation complémentaires pour représenter de manière formelle les systèmes d'information (SI). Un SI est un système informatisé qui permet de rassembler les informations d'une organisation et qui fournit des opérations pour les manipuler. Les SI considérés sont développés autour de systèmes de gestion de bases de données (SGBD). Notre motivation est d'utiliser des notations et des techniques formelles pour les concevoir, contrairement aux méthodes actuelles qui sont au mieux semi-formelles. D'une part, EB3 est un langage formel basé sur les traces d'événements qui a été défini pour la spécification des SI. En particulier, EB3 met en avant le comportement dynamique du système. D'autre part, B est un langage formel basé sur les états qui se prête bien à la spécification des propriétés statiques des SI. Nous avons défini une nouvelle approche, appelée EB4, qui bénéficie à la fois des avantages d'EB3 et B. Dans un premier temps, les processus décrits en EB3 sont utilisés pour représenter et pour valider le comportement du système. Ensuite, la spécification est traduite en B pour spécifier et vérifier les principales propriétés statiques du SI. Enfin, nous avons défini des techniques de synthèse automatique de transactions BD relationnelles à partir du modèle de données d'EB3 pour compléter le cycle de développement du SI.

Les Infrastructures Virtuelles (VIs) ont émergé de la combinaison de l'approvisionnement des ressources informatiques et des réseaux virtuels dynamiques. Grâce à la virtualisation combinée des ressource de calcul et de réseau, le concept de VI transforme l'Internet en un réservoir mondial de ressources interconnectées. Avec l'innovation des VIs viennent aussi des nouveaux défis nécessitant le développement de modèles et technologies, pour assister la migration d'applications existantes d'infrastructures traditionnelles vers des VIs. L'abstraction complète des ressources physiques et l'indéterminisme dans les besoins des applications, en termes de ressources de calcul et de communication ont fait de la composition de VI un problème difficile. En outre, l'allocation d'un ensemble des VIs sur un substrat distribué est un problème NP-difficile. En plus des objectifs traditionnels (par exemple un coût minimal, un revenu croissant), un algorithme d'allocation doit également satisfaire les attentes des utilisateurs (par exemple la qualité de l'allocation). Ce manuscrit contribue aux initiatives de recherche en cours avec les propositions suivantes : i) le Virtual Infrastructure Description Language (VXDL), qui permet aux utilisateurs et aux systèmes de décrire les composants pertinents d'une VI ; ii) un mécanisme qui traduit un flux de travail en une spécification de VI pour faciliter l'exécution d'applications distribuées; iii) une solution pour réduire l'espace de recherche d'une façon automatique qui accélère le processus d'allocation ; et iv) un service offert par des fournisseurs d'infrastructure avec lequel un utilisateur peut déléguer les besoins en fiabilité.

Thèse numérisée par la Division de la gestion de documents et des archives de l'Université de Montréal

Durant ma thèse, j'ai participé à une étude fonctionnelle qui a démontré que p120-RasGAP, une protéine appartenant à la famille GAP (GTPase-activating protein), est le médiateur cytoplasmique de l'éphrine lors de l'atténuation d'ERK1/2. Pour confirmer cela, j'ai réalisé une expérience de co-immunoprécipitation et j'ai démontré que p120-RasGAP s'associe au récepteur de l'éphrine, Eph3, quand celui-ci est activé par un ligand éphrine. Ce résultat indique fortement que les signaux FGF et éphrine convergent au niveau de Ras et qu'ils contrôlent de manière antagoniste son activité. Dès lors, j'ai analysé les autres événements de spécification cellulaire impliquant l'antagonisme FGF/éphrine. Chez l'embryon d'ascidie, le signal FGF est décrit comme inducteur du destin neural dans les cellules ectodermiques qui, en absence du signal FGF, adoptent le destin épidermique. L'induction neurale des ascidies a lieu au stade 32 cellules et se traduit par la spécification de quatre précurseurs neuraux (ERK+) parmi les 16 cellules ectodermiques. J'ai démontré que le signal éphrine/Eph/RasGAP antagonise le signal FGF pour générer une activation d'ERK1/2 de type tout ou rien parmi les cellules ectodermiques. Enfin, en collaboration avec Philip Abitua, doctorant dans le laboratoire du Dr. Mike Levine (UC Berkeley), nous démontrons que l'antagonisme entre les signaux éphrine et FGF est impliqué dans la régionalisation antéro-postérieure de la plaque neurale

Le développement d'un système a pour objectif de répondre à des exigences. Aussi, le succès de sa réalisation repose en grande partie sur la phase de spécification des exigences qui a pour vocation de décrire de manière précise et non ambiguë toutes les caractéristiques du système à développer.Les spécifications d'exigences sont le résultat d'une analyse des besoins faisant intervenir différentes parties. Elles sont généralement rédigées en langage naturel (LN) pour une plus large compréhension, ce qui peut mener à diverses interprétations, car les textes en LN peuvent contenir des ambiguïtés sémantiques ou des informations implicites. Il n'est donc pas aisé de spécifier un ensemble complet et cohérent d'exigences. D'où la nécessité d'une vérification formelle des spécifications résultats.Les spécifications LN ne sont pas considérées comme formelles et ne permettent pas l'application directe de méthodes vérification formelles.Ce constat mène à la nécessité de transformer les spécifications LN en spécifications formelles.C'est dans ce contexte que s'inscrit cette thèse.La difficulté principale d'une telle transformation réside dans l'ampleur du fossé entre spécifications LN et spécifications formelles.L'objectif de mon travail de thèse est de proposer une approche permettant de vérifier automatiquement des spécifications d'exigences utilisateur, écrites en langage naturel et décrivant le comportement d'un système.Pour cela, nous avons exploré les possibilités offertes par un modèle de représentation fondé sur un formalisme logique.Nos contributions portent essentiellement sur trois propositions :1) une ontologie en OWL-DL fondée sur les logiques de description, comme modèle de représentation pivot permettant de faire le lien entre spécifications en langage naturel et spécifications formelles; 2) une approche d'instanciation du modèle de représentation pivot, fondée sur une analyse dirigée par la sémantique de l'ontologie, permettant de passer automatiquement des spécifications en langage naturel à leur représentation conceptuelle; et 3) une approche exploitant le formalisme logique de l'ontologie, pour permettre un passage automatique du modèle de représentation pivot vers un langage de spécifications formelles nommé Maude.

Malgré les progrès importants effectués en matière de conception de logiciels et l'existence de méthodes de développement éprouvées, il faut reconnaître que les défaillances de systèmes causées par des logiciels restent fréquentes. Il arrive même que ces défaillances concernent des logiciels critiques et provoquent des dommages significatifs. Considérant l'importance des intérêts en jeu, et le fait que la garantie de logiciel "zéro défaut" est hors d'atteinte, il est donc important de pouvoir déterminer en cas de dommages causés par des logiciels les responsabilités des différentes parties. Pour établir ces responsabilités, un certain nombre de conditions doivent être réunies: (i) on doit pouvoir disposer d'éléments de preuve fiables, (ii) les comportements attendus des composants doivent avoir été définis préalablement et (iii) les parties doivent avoir précisé leurs intentions en matière de répartition des responsabilités. Dans cette thèse, nous apportons des éléments de réponse à ces questions en proposant un cadre formel pour spécifier et établir les responsabilités en cas de dysfonctionnement d'un logiciel. Ce cadre formel peut être utilisé par les parties dans la phase de rédaction du contrat et pour concevoir l'architecture de logs du système. Notre première contribution est une méthode permettant d'intégrer les définitions formelles de responsabilité et d'éléments de preuves dans le contrat juridique. Les éléments de preuves sont fournis par une architecture de logs dite "acceptable" qui dépend des types de griefs considérés par les parties. La seconde contribution importante est la définition d'une procédure incrémentale, qui est mise en ?uvre dans l'outil LAPRO, pour l'analyse incrémentale de logs distribués.

Il est communément admis que 70 % des coûts du cycle de vie d’un produit sont engagés dès la phase de spécification. Or, aujourd’hui, dans chacune des relations contrac-tuelles client-fournisseur, le fournisseur doit faire face à un amas d’exigences à partir duquel il est difficile de prendre des décisions stratégiques avisées. Pour aider les sous-traitants, nous proposons une méthode outillée de synthèse des exigences, laquelle est supportée par un environnement numérique basé sur les sciences des données. Des modèles de classification extraient les exigences des documents. Les exigences sont ensuite analysées au moyen des techniques de traitement du langage naturel afin d’identifier les défauts de qualité qui mettent en péril le reste du cycle de vie. Pour faciliter leur exploitation, les exigences, dépourvues de leurs principaux défauts, sont non seulement classifiées automatiquement au sein de catégories métiers grâce aux techniques d’apprentissage machine, mais aussi segmentées en communautés au moyen des récentes avancées en théorie des graphes. Chacune des communautés d’exigences est caractérisée par un ensemble configurable de critères d’aide à la décision, dont l’estimation collaborative est assurée par des experts représentant les diverses fonctions de l’entreprise. Enfin, une synthèse graphique des estimations est restituée au décideur via un tableau de bord de résumés statistiques descriptifs facilitant la prise de décisions informées. La validation théorique et empirique de notre proposition corrobore l’hypothèse que les sciences des données est un moyen de synthétiser plusieurs centaines ou milliers d’exigences. / It is broadly accepted that 70 % of the total life cycle cost is committed during the specification phase. However, nowadays, we observe a staggering increase in the number of requirements. We consider the tremendous volume of requirements as big data with which sub-contractors struggle to make strategic decisions early on. Thus, we propose to methodologically integrate data science techniques into a collaborative requirement mining framework, which enables decision-makers to gain insight and discover opportunities in a massive set of requirements. Initially, classification models extract requirements from prescriptive documents. Requirements are subsequently analysed with natural language processing techniques so as to identify quality defects. After having removed the quality defects, the analyst can navigate through clusters of requirements that ease the exploration of big data. Each cluster gathers the requirements that belong to a functional area (mechanics, electronics, IT, etc.). Each domain expert can therefore easily filter out the requirements subset that is relevant for him. A complementary approach consists in detecting communities of requirements by analysing the topology of a graph. Each community owns a customisable set of decision-making criteria which are estimated by all functional areas. A dashboard of statistical visuals distils the estimation results from which a decision maker can make informed decisions. We conclude that the theoretical and empirical validation of our proposition corroborates the assumption that data science is an effective way to gain insight from hundreds or thousands of requirements.

Malgré les progrès importants effectués en matière de conception de logiciels et l'existence de méthodes de développement éprouvées, il faut reconnaître que les défaillances de systèmes causées par des logiciels restent fréquentes. Il arrive même que ces défaillances concernent des logiciels critiques et provoquent des dommages significatifs. Considérant l'importance des intérêts en jeu, et le fait que la garantie de logiciel "zéro défaut" est hors d'atteinte, il est donc important de pouvoir déterminer en cas de dommages causés par des logiciels les responsabilités des différentes parties. Pour établir ces responsabilités, un certain nombre de conditions doivent être réunies: (i) on doit pouvoir disposer d'éléments de preuve fiables, (ii) les comportements attendus des composants doivent avoir été définis préalablement et (iii) les parties doivent avoir précisé leurs intentions en matière de répartition des responsabilités. Dans cette thèse, nous apportons des éléments de réponse à ces questions en proposant un cadre formel pour spécifier et établir les responsabilités en cas de dysfonctionnement d'un logiciel. Ce cadre formel peut être utilisé par les parties dans la phase de rédaction du contrat et pour concevoir l'architecture de logs du système. Notre première contribution est une méthode permettant d'intégrer les définitions formelles de responsabilité et d'éléments de preuves dans le contrat juridique. Les éléments de preuves sont fournis par une architecture de logs dite "acceptable" qui dépend des types de griefs considérés par les parties. La seconde contribution importante est la définition d'une procédure incrémentale, qui est mise en ?uvre dans l'outil LAPRO, pour l'analyse incrémentale de logs distribués. / Despite the effort made to define methods for the design of high quality software, experience shows that failures of IT systems due to software errors remain very common and one must admit that even critical systems are not immune from that type of errors. One of the reasons for this situation is that software requirements are generally hard to elicit precisely and it is often impossible to predict all the contexts in which software products will actually be used. Considering the interests at stake, it is therefore of prime importance to be able to establish liabilities when damages are caused by software errors. Essential requirements to define these liabilities are (1) the availability of reliable evidence, (2) a clear definition of the expected behaviors of the components of the system and (3) the agreement between the parties with respect to liabilities. In this thesis, we address these problems and propose a formal framework to precisely specify and establish liabilities in a software contract. This framework can be used to assist the parties both in the drafting phase of the contract and in the definition of the architecture to collect evidence. Our first contribution is a method for the integration of a formal definition of digital evidence and liabilities in a legal contract. Digital evidence is based on distributed execution logs produced by "acceptable log architectures". The notion of acceptability relies on a formal threat model based on the set of potential claims. Another main contribution is the definition of an incremental procedure, which is implemented in the LAPRO tool, for the analysis of distributed logs.