Le test exploratoire (TE) est défini comme l'apprentissage, la conception et l'exécution simultanés des tests, tout à fait l'opposé du test scénarisé (TS) prédéfini. L'applicabilité de cette nouvelle approche ne cesse pas d'augmenter dans l'industrie du test de logiciel. Malgré cette expansion et le succès de quelques entreprises qui s'ouvrent dans le domaine de développement du logiciel dans ses expériences d'adoption et d'utilisation de TE, les contextes et les facteurs favorables pour l'adoption de l'approche dans une méthodologie de test ne sont pas toujours bien établis. L'absence des preuves claires de sa productivité annoncée par quelques praticiens dans la littérature s'ajoute à la problématique. Ce travail est une étude exploratoire visant deux objectifs. Premièrement, étudier et analyser les contextes favorisant l'utilisation de TE comme une méthodologie primaire de test à la place des tests scénarisés en élaborant une analyse comparative entre le TE et le TS. Deuxièmement, évaluer sa productivité dans une étude empirique par rapport au TS. Nous avons élaboré un cadre conceptuel de comparaison dans lequel nous avons identifié cinq dimensions: o Les caractéristiques d'utilisation: les raisons de l'utilisation, les caractéristiques du logiciel, le type d'environnement d'affaires, les ressources financières et le temps disponible pour les tests; o Les caractéristiques de gestion: la planifIcation, le contrôle et le suivi des tests, la communication dans le projet de test et la relation avec le client; o Les caractéristiques techniques: les activités de test, l'oracle de test, les risques du logiciel et la couverture de test; o Les caractéristiques du personnel: les caractéristiques des testeurs, la culture de l'organisation; o La productivité: le nombre de défauts détectés, l'importance de défauts détectés. Ce cadre a été utilisé comme base dans l'analyse comparative du TE et du TS. Dans cette analyse, nous avons comparé une approche disciplinée de TS guidé par les patrons de documentation IEEE 829 et une approche libre, semi planifiée de TE représentée par l'approche Session Based Exploratory Testing (SBET). Dans cette comparaison, la productivité a été évaluée par le biais d'une étude empirique que nous avons mise en oeuvre, dans les laboratoires informatiques de L'UQÀM. Malgré les limites du contexte de cette étude empirique, nous avons pu dégager quelques conclusions utiles. Les résultats permettent de montrer que certains facteurs de contexte du projet de test peuvent empêcher l'utilisation de TE comme une méthode principale de test. Nous avons conclu que l'absence de contrôle de couverture de test restreint en plus le type des projets où le TE pourrait être utilisé. Aussi, l'expertise et les qualifications nécessaires pour exécuter le TE pourraient empêcher son utilisation dans les projets de tests où ces qualifications sont manquantes. Les résultats de l'étude empirique ont supporté l'hypothèse relative à l'importance des défauts détectés. D'autres recherches quantitatives sur la productivité de TE sont nécessaires, dont ce travail pourra servir comme point de départ.

Le test exploratoire (TE) est défini comme l'apprentissage, la conception et l'exécution simultanés des tests, tout à fait l'opposé du test scénarisé (TS) prédéfini. L'applicabilité de cette nouvelle approche ne cesse pas d'augmenter dans l'industrie du test de logiciel. Malgré cette expansion et le succès de quelques entreprises qui s'ouvrent dans le domaine de développement du logiciel dans ses expériences d'adoption et d'utilisation de TE, les contextes et les facteurs favorables pour l'adoption de l'approche dans une méthodologie de test ne sont pas toujours bien établis. L'absence des preuves claires de sa productivité annoncée par quelques praticiens dans la littérature s'ajoute à la problématique. Ce travail est une étude exploratoire visant deux objectifs. Premièrement, étudier et analyser les contextes favorisant l'utilisation de TE comme une méthodologie primaire de test à la place des tests scénarisés en élaborant une analyse comparative entre le TE et le TS. Deuxièmement, évaluer sa productivité dans une étude empirique par rapport au TS. Nous avons élaboré un cadre conceptuel de comparaison dans lequel nous avons identifié cinq dimensions: o Les caractéristiques d'utilisation: les raisons de l'utilisation, les caractéristiques du logiciel, le type d'environnement d'affaires, les ressources financières et le temps disponible pour les tests; o Les caractéristiques de gestion: la planifIcation, le contrôle et le suivi des tests, la communication dans le projet de test et la relation avec le client; o Les caractéristiques techniques: les activités de test, l'oracle de test, les risques du logiciel et la couverture de test; o Les caractéristiques du personnel: les caractéristiques des testeurs, la culture de l'organisation; o La productivité: le nombre de défauts détectés, l'importance de défauts détectés. Ce cadre a été utilisé comme base dans l'analyse comparative du TE et du TS. Dans cette analyse, nous avons comparé une approche disciplinée de TS guidé par les patrons de documentation IEEE 829 et une approche libre, semi planifiée de TE représentée par l'approche Session Based Exploratory Testing (SBET). Dans cette comparaison, la productivité a été évaluée par le biais d'une étude empirique que nous avons mise en oeuvre, dans les laboratoires informatiques de L'UQÀM. Malgré les limites du contexte de cette étude empirique, nous avons pu dégager quelques conclusions utiles. Les résultats permettent de montrer que certains facteurs de contexte du projet de test peuvent empêcher l'utilisation de TE comme une méthode principale de test. Nous avons conclu que l'absence de contrôle de couverture de test restreint en plus le type des projets où le TE pourrait être utilisé. Aussi, l'expertise et les qualifications nécessaires pour exécuter le TE pourraient empêcher son utilisation dans les projets de tests où ces qualifications sont manquantes. Les résultats de l'étude empirique ont supporté l'hypothèse relative à l'importance des défauts détectés. D'autres recherches quantitatives sur la productivité de TE sont nécessaires, dont ce travail pourra servir comme point de départ. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Test, Test scénarisé, Test exploratoire, Session Based Exploratory Test (SBET).

Ces travaux de recherche présentent un nouveau cadre formel pour intégrer le diagnostic de fautes multiples et la reconfiguration. L'idée principale est d'utiliser STRIPS (Stanford Research Institute Problem Solver), un langage formel pour la planification automatisée qui peut intégrer les relations cause_effect et le mécanisme de raisonnement automatique dans un modèle. Le processus de diagnostic de fautes multiples et son module de vérification de cohérence sont basés sur le langage STRIPS. En outre, le modèle de faute est introduit dans le module de vérification de cohérence pour empêcher les diagnostics impossibles. Le langage STRIPS peut définir qualitativement le modèle de faute, sans nécessiter une connaissance précise et détaillée des composants défaillants. A partir des résultats du diagnostic, la reconfiguration met à jour le modèle du système. Elle vérifie que le modèle permet de réaliser les objectifs à partir d’une approche basée sur la vérification de modèle. Les objectifs sont pour ceci, exprimés à l’aide une logique temporelle. / This research presents a new formal framework for integrating multi-fault diagnosis and reconfiguration. The main idea is to use the STRIPS (STanford Research Institute Problem Solver), a formal language for automated planning which can integrate the cause_effect knowledge and the automated reasoning mechanism into one model. The multi-fault diagnostic process and its consistency-checking module are all based on the models defined by STRIPS actions. Moreover, the fault models are introduced into the consistency-checking module for preventing the impossible diagnoses. The STRIPS can qualitatively define the fault models without requiring detail and precise knowledge of faulty components. According to the results of diagnosis, the reconfiguration updates the system’s model. It uses the model checking to verify whether the updated model satisfies the desired objectives. These objectives are described by a temporal language.

Les compilateurs optimisants pour les langages de programmation sont devenus des logiciels complexes et donc une source de bugs. Ceci peut être dangereux dans le contexte de systèmes critiques comme l'avionique ou la médecine. Cette thèse s'inscrit dans le cadre de la compilation vérifiée optimisante dont l'objectif est d'assurer l'absence de tels bugs. Plus précisément, nous étudions sémantiquement une représentation intermédiaire SSA (Single Static Assignment) particulière, Sea of Nodes, utilisée notamment dans le compilateur optimisant HotSpot pour Java. La propriété SSA a déjà été étudiée d'un point de vue sémantique sur des représentations simples sous forme de graphe de flot de contrôle, mais le sujet des dépendances entre instructions a seulement été effleuré depuis une perspective formelle. Cette thèse apporte une étude sémantique de transformations de programmes sous forme Sea of Nodes, intégrant la flexibilité en termes de dépendances de données entre instructions. En particulier, élimination de zero-checks redondants, propagation de constantes, retour au bloc de base séquentiel et destruction de SSA sont étudiés. Certains des sujets abordés, dont la formalisation d'une sémantique pour Sea of Nodes, sont accompagnés d'une vérification à l'aide de l'assistant de preuve Coq. / Optimizing compilers for programming languages have become complex software, and they are hence subject to bugs. This can be dangerous in the context of critical systems such as avionics or health care. This thesis is part of research work on verified optimizing compilers, whose objective is to ensure the absence of such bugs. More precisely, we semantically study a particular SSA intermediate representation, Sea of Nodes, which is notably used in the optimizing compiler HotSpot for Java. The SSA property has already been studied from a semantic point of view on simple intermediate representations in control flow graph form, but the subject of dependencies between instructions has just been skimmed from a formal perspective. This thesis brings a semantic study of transformations of programs in Sea of Nodes form, integrating the flexibility regarding data dependencies between instructions. In particular, redundant zero-check elimination, constant propagation, transformation back to sequential basic block, and SSA destruction are studied. Some of the approached topics, including the formalization of a semantics for Sea of Nodes, are accompanied by a verification using the Coq proof assistant.

Des applications compilées en code-octet et encodées dans le format de fichier class sont normalement chargées et exécutées par une machine virtuelle. La vérification du code-octet est un processus utilisé par une machine virtuelle pour renforcer la sécurité des systèmes distribués en garantissant la conformité du code de classes avec les règles du langage. Les algorithmes actuels de vérification du code-octet utilisent des approches comme l'analyse de flot de données, le model checking ou le code-certifié (similaire au proof-carrying code). Mais l'on dénote certains problèmes, en particulier dus aux sous-routines, avec soit des spécifications informelles et incomplètes, soit des algorithmes ne supportant qu'un sous-ensemble du jeu d'instructions du code-octet, ou encore des performances exponentielles proportionnellement à la taille du code des méthodes à vérifier. Dans ce mémoire nous présentons une technique de vérification du code-octet avec sous-routines par code-certifié. Nous présentons en particulier la conception d'un format de certificat, d'un algorithme de calcul de certificat et d'un algorithme de vérification pour l'ensemble du jeu d'instructions du code-octet. Notre algorithme de vérification a une complexité linéaire en proportion de la taille du code des méthodes. Le développement d'un vérificateur et d'un compilateur de certificats a servi à conduire des expérimentations qui montrent que le format de certificat proposé est suffisamment riche pour effectuer la vérification du code-octet. De plus, nous présentons les résultats de l'évaluation du coût en espace mémoire de la certification de classes avec une telle technique. L'observation montre un accroissement relativement faible de la taille d'un échantillon de plus de 35 000 classes suite à leur certification. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Vérification, Code-octet, Code-certifié, Analyse de flot de données, Sous-routines, Java.

Avec la complexité croissante des systèmes sur puce, le processus de vérification devient une tâche de plus en plus cruciale à tous les niveaux du cycle de conception, et monopolise une part importante du temps de développement. Dans ce contexte, l'assertion-based verification (ABV) a considérablement gagné en popularité ces dernières années. Il s'agit de spécifier le comportement attendu du système par l'intermédiaire de propriétés logico-temporelles, et de vérifier ces propriétés par des méthodes semi-formelles ou formelles. Des langages de spécification comme PSL ou SVA (standards IEEE) sont couramment utilisés pour exprimer ces propriétés. Des techniques de vérification statiques (model checking) ou dynamiques (validation en cours de simulation) peuvent être mises en œuvre. Nous nous plaçons dans le contexte de la vérification dynamique. A partir d'assertions exprimées en PSL ou SVA, des descriptions VHDL ou Verilog synthétisables de moniteurs matériels de surveillance peuvent être produites (outil Horus). Ces composants peuvent être utilisés pendant la conception (en simulation et/ou émulation pour le débug et la validation de circuits), ou comme composants embarqués, pour la surveillance du comportement de systèmes critiques. Pour l'analyse en phase de conception, que ce soit en simulation ou en émulation, le problème de la génération des séquences de test se pose. En effet, des séquences de test générées aléatoirement peuvent conduire à un faible taux de couverture des conditions d'activation des moniteurs et, de ce fait, peuvent être peu révélatrices de la satisfaction des assertions. Les méthodes de génération de séquences de test sous contraintes n'apportent pas de réelle solution car les contraintes ne peuvent pas être liées à des conditions temporelles. De nouvelles méthodes doivent être spécifiées et implémentées, c'est ce que nous nous proposons d'étudier dans cette thèse. / With the increasing complexity of SoC, the verification process becomes a task more crucial at all levels of the design cycle, and monopolize a large share of development time. In this context, the assertion-based verification (ABV) has gained considerable popularity in recent years. This is to specify the behavior of the system through logico-temporal properties and check these properties by semiformal or formal methods. Specification languages such as PSL or SVA (IEEE) are commonly used to express these properties. Static verification techniques (model checking) or dynamic (during simulation) can be implemented. We are placed in the context of dynamic verification. Our assertions are expressed in PSL or SVA, and synthesizable descriptions VHDL or Verilog hardware surveillance monitors can be produced (Horus tool). These components can be used for design (simulation and/or emulation for circuit debug and validation) or as embedded components for monitoring the behavior of critical systems. For analysis in the design phase, either in simulation or emulation, the problem of generating test sequences arises. In effect, sequences of randomly generated test can lead to a low coverage conditions of activation monitors and, therefore, may be indicative of little satisfaction assertions. The methods of generation of test sequences under constraints do not provide real solution because the constraints can not be linked to temporal conditions. New methods must be specified and implemented, this's what we propose to study in this thesis.

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.

L'utilisation d'intergiciels pour la réalisation de systèmes temps réel répartis embarqus (TR2E) nécessite la preuve des propriétés de bon fonctionnement de l'intergiciel et une mesure de son impact sur la sémantique du système. Parallèlement, l'intergiciel doit être adaptable et répondre à de nombreuses contraintes (plate-forme d'exécution, ressources, interfaces de communication, ...). Cette thèse propose une architecture adaptable d'intergiciel qui permet 1) l'adaptabilité de ses fonctions élémentaires aux besoins de l'utilisateur, 2) la vérification formelle des propriétés de l'intergiciel. Cette architecture étend celle de l'intergiciel schizophrène. Elle fournit une séparation claire entre la boucle de contrôle et les services fonctionnels de l'intergiciel, facilitant le support de plusieurs politiques de concurrence et de gestions des ressources. Nous avons validé notre proposition en vérifiant formellement les propriétés causales de deux configurations de l'intergiciel, en étendant les mécanismes de l'intergiciel pour proposer une implantation complète des spcifications RTCORBA et DDS, ainsi qu'un guide pour le support d'autres classes d'intergiciels. Enfin, nous proposons une analyse complète des performances, du déterminisme et de l'empreinte mémoire de configurations significatives de l'intergiciel.

La conception basée composants est une nouvelle méthode de construction d'applications et de systèmes distribués. Cette conception par composition pose cependant plusieurs problèmes, dûs aux services non uniformes (dépendants d'un contexte) et aux liens dynamiques d'interconnexion entre les composants. Nous proposons un cadre formel pour la vérification compositionelle de tels systèmes. Nous définissons un langage de type d'interfaces comportementales, qui constitue un contrat comportemental pour le composant et son environnement. Le composant doit respecter ce contrat

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.