Les systèmes logiciels complexes sont omniprésents dans notre vie quotidienne. De ce fait, un dysfonctionnement peut occasionner aussi bien une simple gêne qu'un danger mettant en péril des vies humaines. Le test est l'une des techniques les plus répandues (en particulier dans l'industrie) pour détecter les erreurs d'un système. Lorsque le cahier des charges d'un système est décrit par une spécification formelle, le test de conformité est utilisé pour garantir un certain niveau de confiance dans la correction d'une implémentation de ce système - dans ce cadre, la relation de conformité formalise la notion de correction. Cette thèse se focalise sur le test de conformité pour les systèmes concurrents. Le test de conformité pour les systèmes concurrents utilise principalement des modèles qui interprètent la concurrence par des entrelacements. Néanmoins, cette approche souffre du problème de l'explosion de l'espace d'états et elle n'offre pas la possibilité de tester certaines propriétés de la spécification telle que l'indépendance entre actions. Pour ces raisons, nous utilisons une sémantique d'ordres partiels pour la concurrence. De plus, nous proposons une nouvelle sémantique qui permet à certaines actions concurrentes d'être entrelacées et en force d'autres à être implémentées indépendamment. Nous proposons une généralisation de la relation de conformité ioco où les spécifications sont des réseaux de Petri et leur sémantique d'ordres partiels est donnée par leur dépliage. Cette relation de conformité permet de préserver l'indépendance, dans l'implémentation, des actions spécifiées comme concurrentes. Nous présentons un cadre de test complet pour cette relation. Nous définissons la notion de cas de test globaux gérant la concurrence, réduisant ainsi non seulement la taille des cas de test mais aussi celle de la suite de tests. Nous montrons comment les cas de test globaux peuvent être construits à partir du dépliage de la spécification en s'appuyant sur une traduction SAT, et nous réduisons le problème de la sélection de tests à la sélection d'un préfixe fini de ce dépliage : nous définissons différents critères de sélection à partir de la notion d'événement limite (cut-off event). Enfin, en supposant que chaque processus d'un système distribué possède une horloge locale, nous montrons que la conformité globale peut être testée dans une architecture de test distribuée en utilisant seulement des testeurs locaux ne communiquant pas entre eux. / Complex systems are everywhere and are part of our daily life. As a consequence, their failures can range from being inconvenient to being life-threatening. Testing is one of the most widely accepted techniques (especially in industry) to detect errors in a system. When the requirements of the system are described by a formal specification, conformance testing is used to guarantee a certain degree of confidence in the correctness of an implementation- in this setting a conformance relation formalizes the notion of correctness. This thesis focuses on conformance testing for concurrent systems. Conformance testing for concurrent system has mainly focused on models that interpret concurrency by interleavings. This approach does not only suf- fer from the state space explosion problem, but also lacks the ability to test properties of the specification such as independence between actions. For such reasons, we focus not only on partial order semantics for concurrency, but also propose a new semantics that allows to interleave some actions while forcing others to be implemented as independent. We propose a generalization of the ioco conformance relation, based on Petri nets specifications and their partial order semantics given by their unfoldings, preserving thus independence of actions from the specification. A complete testing framework for this conformance relation is presented. We introduce the notion of global test cases which handle concurrency, reducing not only the size of the test case, but also the number of tests in the test suite. We show how global test cases can be constructed from the unfolding of the specification based on a SAT encoding and we reduce the test selection problem to select a finite prefix of such unfolding: different testing criteria are defined based on the notion of cut-off events. Finally, we show that assuming each process of a distributed system has a local clock, global conformance can be tested in a distributed testing architecture using only local testers without any communication.

Le test de conformité est le processus permettant de contrôler qu'un système possède un ensemble de propriétés souhaitées et se comporte conformément à certaines exigences prédéfinies. Dans ce contexte, les techniques de test passif sont utilisées lorsque le système sous test ne peut être interrompu ou l'accès aux interfaces du système est indisponible. Le test passif s'appuie sur l'observation de l'application pendant l'exécution, et la comparaison de l'observation avec le comportement attendu, défini à travers des propriétés de conformité. L'objectif de cette thèse est la définition d'une méthodologie de validation des protocoles communicants par test passif. Les approches existantes sont issues de travaux basés sur des spécifications à états finis ou de transitions étiquetées et comme tels, ils présument l'existence d'une relation de causalité entre les évènements observés dans la trace du système. Pour le traitement des protocoles basés sur des messages, comme le protocole SIP (fondamental pour les services IMS), telle causalité n’existe pas nécessairement et en outre, elle ne peut être déterminée que par la partie données du protocole. Étant donné que les techniques existantes sont optimisées pour traiter les parties de contrôle, ils présentent des limites pour les tests basés sur des parties de données: expressibilité réduite de propriétés de conformité, entre autres. Dans ce travail nous présentons une approche sur la base des messages et données pour traiter ces problèmes. Les observations dans une trace sont sous la forme de messages. Le comportement attendu est défini de manière ascendante, à partir des critères basés sur les relations entre les champs des données des messages. Des relations temporelles sont définies entre ces critères, par exemple, une propriété peut exiger que certains critères “doit être reconnu pour tous les messages dans la trace”. Notre approche permet d’exprimer des formules sur l’avenir et le passé de la trace, permettant de définir des critères plus généraux que ceux qui utilisent uniquement des parties de contrôle. Des problèmes liés à la satisfaction des propriétés et la déclaration des verdicts de conformité sont également discutés. Bien que l'observation d'un comportement défini comme une propriété est un indice de conformité, l'absence d'observation n'est pas nécessairement indicative d'une faute. Plusieurs solutions à ce problème ont été proposées et mises en œuvre dans ce travail. Enfin, notre travail présente des perspectives intéressantes en termes d'extensibilité pour la détection en ligne ou une expressivité améliorée, mais aussi car une approche basée sur des messages fournit une vision alternative aux techniques de test traditionnelles / Conformance testing is the process of checking that a system possesses a set of desired properties and behaves in accordance with some predefined requirements. In this context, passive testing techniques are used when the system under test cannot be interrupted or access to the system's interfaces is unavailable. Passive testing relies on the observation of the implementation during runtime, and the comparison of the observation with the expected behavior, defined through conformance properties. The objective of this thesis is to define a novel methodology to validate communicating protocols by passive testing. Existing approaches are derived from works with finite-state and labelled transition specifications and as such, they presume there exists a causality relation between the events observed in the implementation (the trace). When dealing with message-based protocols, such as the Session Initiation Protocol (fundamental for IMS services), such causality does not necessarily exist and furthermore, it may only be determined through data parts. Since existing techniques are optimized for dealing with control parts, they present limitations for testing based on data parts: reduced expressibility and succinctness of conformance properties, as well as problems to deal with satisfaction of properties including future conditions. In this work we present a message-based/data-centric approach for dealing with these issues. Observations in a trace are in the form of messages. Expected behavior is defined in a bottom-up fashion, starting from expected criteria that must be fulfilled by one or more messages, defined as constraints between the message data fields. Temporal relations by quantification over the criteria, e.g. a property may require that certain criteria "must be held for all messages in the trace". Our approach allows to express formulas about the future and past of the trace, allowing to define more general criteria than through control parts alone. Issues related to satisfaction of properties and declaration of conformance verdicts are also discussed here. Although observation of a behavior defined as a property is indication of conformance, lack of observation is not necessarily indicative of a fault. Several solutions to this issue have been proposed and implemented in this work. Finally, our work presents interesting perspectives, in terms of extensibility for online detection or improved expressiveness, but also since a message-based approach provides an alternative view to traditional testing techniques

La complexité croissante des systèmes réactifs fait que le test devient une technique de plus en plus importante dans le développement de tels systèmes. Un grand intérêt est notamment accordé au test de conformité qui consiste à vérier si les comportements d'un système sous test sont corrects par rapport à sa spécication. Au cours des dernières années, les théories et outils de test de conformité pour la génération automatique de test se sont développés. Dans ces théories et algorithmes, les spécications des systèmes réactifs sont souvent modélisées par différentes variantes des systèmes de transitions. Cependant, ces théories et outils ne prennent pas explicitement en compte les données du système puisque le modèle sous-jacent de système<br />de transitions ne permet pas de le faire. Ceci oblige à énumérer les valeurs des données avant de construire le modèle de système de transitions d'un système, ce qui peut provoquer le problème de l'explosion de l'espace d'états. Cette énumération a également pour effet d'obtenir des cas de test où toutes les données sont instanciées. Or, cela contredit la pratique industrielle où les cas de test sont de vrais programmes avec des variables et des paramètres. La génération de tels<br />cas de test exige de nouveaux modèles et techniques. Dans cette thèse, nous atteignons deux objectifs. D'une part, nous introduisons un modèle appelé système symbolique de transitions à entrée/sortie qui inclut explicitement toutes les données d'un système réactif. D'autre part, nous proposons et implémentons une nouvelle technique de génération de test qui traite symboliquement les données d'un système en combinant l'approche de génération de test proposée auparavant par notre groupe de recherche avec des techniques d'interprétation abstraite. Les cas de test générés automatiquement par notre technique satisfont des propriétés de correction: ils émettent toujours un verdict correct.

Ce travail se situe dans le cadre de la vérification et de la validation des systèmes répartis, particulièrement les protocoles de télécommunication. Nous nous sommes intéressés au problème de la génération automatique de tests de conformité pour les protocoles de télécommunication et plus précisément à l'utilisation, en amont de TGV (un outil de génération de séquences de test), de techniques d'analyse statique. La génération de test de conformité fondée sur des techniques de vérification par modèles (l'approche employée par TGV) est limitée par le problème d'explosion d'état. Même si ce problème, dans la pratique, peut être contourné (en choisissant le fonctionnement à la volée de TGV), quelque aspects de cette méthode (par exemple la conception des objectifs de test pour un modèle, sans le construire explicitement) posent encore des problèmes. Dans notre thèse on propose une méthodologie de test basée sur des techniques issues des domaines de la vérification et de l'analyse statique. Cette méthodologie consiste en un ensemble de procédures qui ont pour but de simplifier la spécification en tenant compte de sa structure ou de la structure des objectifs de test et cela avant de la génération des cas de test. On réduit ainsi la taille des modèles observables des spécifications. Nous avons étendu aussi le concept de l'objectif de test. Les objectifs de test abstraits ont des contraintes symboliques attachées aux paramètres des signaux d'entrée. À partir des contraintes d'entrée les procédures mentionnées ci-dessus calculent des contraintes pour les paramètres des signaux de sortie des objectifs de test abstraits. Ensuite, des objectifs de test concrets pourront être dérivés et en utilisant l'outil de test existant TGV on pourrait générer des tests de conformité

Notre approche, dans le cadre du test de conformité, se base sur le fait qu'il existe différents niveaux d'abstraction pour définir des tests : les tests exécutables pour une cible technologique et les tests abstraits qui sont indépendants de la technologie. Nos travaux portent sur deux points. <br />Le premier point vise à réduire l'effort alloué à la conception des tests. Pour cela nous définissons un nouveau niveau d'abstraction : les schémas de test qui offrent une abstraction supplémentaire sur les instances et valeurs manipulées. L'outil Tobias a été développé au cours de la thèse pour aider à la conception des schémas de test, les déplier en cas de test abstraits, puis concrétiser ces cas de test. <br />Malheureusement, les principes du langage de schéma de tests entraînent un problème d'explosion combinatoire du nombre de tests. Nous proposons donc diverses approches pour, d'une part, mieux contrôler le nombre de tests produits et, d'autre part, optimiser le temps d'exécution des tests. <br />Ces diverses techniques ont pu être intégrées à l'outil Tobias, nous permettant de réaliser deux études de cas afin de valider notre approche.

L'activité de test est une partie de plus en plus importante dans les développements logiciels. Cette activité de test est souvent longue et répétitive, les travaux entrepris dans cette thèse ont pour objectif de décharger l'ingénieur de test des tâches les plus répétitives de la synthèse de tests. Notre approche, dans le cadre du test de conformité, se base sur le fait qu'il existe différents niveaux d'abstraction pour définir des tests les tests exécutables pour une cible technologique, les tests abstraits qui sont indépendants de la technologie et les objectifs de test qui ne représentent que partiellement le chemin d'un test dans la spécification. Nos travaux portent sur deux points. le premier point vise à réduire l'effort alloué à la conception des tests. Pour cela nous définissons un nouveau niveau d'abstraction : les schémas de test qui offrent une abstraction supplémentaire sur les instances et valeurs manipulées. L'outil TObiAs a été développé au cours de la thèse pour aider à la conception des schémas de test, les déplier en objectifs de test ou en cas de test, puis concrétiser ces cas de test. le deuxième point étudie la portée d'un schéma de test en mesurant sa couverture de la spécification, au niveau d'abstraction du schém de test. Pour ce faire nous étudions les relations entre les niveaux d'abstraction de test et la spécification. Nous présentons l'intérêt de proposer une notion de couverture au niveau des schémas de test en construisant une abstraction de la spécification ainsi que l'outil CoPAS que nous avons créé pour calculer la couverture a priori.

Les travaux présentés dans ce mémoire de thèse s'intéressent à la génération et à la mise en œuvre de séquences de test pour le test de conformité de contrôleurs logiques. Dans le cadre de ces travaux, le Grafcet (IEC 60848 (2002)), langage de spécification graphique utilisé dans un contexte industriel, a été retenu comme modèle de spécification. Les contrôleurs logiques principalement considérés dans ces travaux sont les automates programmables industriels (API). Afin de valider la mise en œuvre du test de conformité pour des systèmes de contrôle/commande critiques, les travaux présentés proposent: - Une formalisation du langage de spécification Grafcet. En effet, l'application des méthodes usuelles de vérification et de validation nécessitent la connaissance du comportement à partir de modèles formels. Cependant, dans un contexte industriel, les modèles utilisés pour la description des spécifications fonctionnelles sont choisis en fonction de leur pouvoir d'expression et de leur facilité d'utilisation, mais ne disposent que rarement d'une sémantique formelle. - Une étude de la mise en œuvre de séquences de test et l'analyse des verdicts obtenus lors du changement simultané de plusieurs entrées logiques. Une campagne d'expérimentation a permis de quantifier, pour différentes configurations de l'implantation, le taux de verdicts erronés dus à ces changements simultanés. - Une définition du critère de SIC-testabilité d'une implantation. Ce critère, déterminé à partir de la spécification Grafcet, définit l'aptitude d'une implantation à être testée sans erreur de verdict. La génération automatique de séquences de test minimisant le risque de verdict erroné est ensuite étudiée.

Ces dernières années ont vu l'émergence d'architectures orientées services (SOA) conçues pour faciliter la création, l'exposition, l'interconnexion et la réutilisation d'applications à base de services. Les services Web sont la réalisation la plus importante de cette architecture SOA. Ce sont des applications auto descriptives et modulaires fournissant un modèle simple de programmation et de déploiement d'applications. La composition de services Web, en particulier l'orchestration, est au coeur de l'ingénierie à base de services (SOC pour Service Oriented Computing) puisque elle supporte la construction de nouveaux services composés à partir de services de base. De son côté, WS-BPEL (ou BPEL) s'est imposé depuis 2005 comme le langage standard d'orchestration de services Web. Cette thèse de Doctorat s'articule autour du test fonctionnel de l'orchestration de services décrite en langage BPEL, qui consiste à établir la conformité de l'implantation d'un service composé par rapport à sa spécification. Nos activités de recherche ont été motivées par les caractéristiques spécifiques de la composition de services surtout celle décrite en BPEL, et par la nécessité d'automatisation des tests. L'objectif de cette thèse est double : d'une part, proposer une modélisation formelle de l'orchestration de services, et d'autre part, proposer une méthode de test complète de l'orchestration de services, allant de la modélisation formelle de l'orchestration à l'exécution des tests, incluant la génération automatique de cas de test. Notre modèle formel (appelé WS-TEFSM) permet de décrire une grande partie de BPEL et prend en considération les propriétés temporelles de la composition de service. La modélisation formelle est la première phase de notre approche de test. Par conséquent, nous utilisons le modèle formel résultant pour la génération de cas de test satisfaisant un ensemble d'objectifs de test. L'automatisation de la génération de cas de test a été mise en oeuvre par l'implémentation d'une stratégie efficace d'exploration partielle de l'espace d'états (i.e. Hit-Or-Jump) dans le simulateur IF. Pour se focaliser seulement sur les erreurs potentielles du service orchestrateur (service composé), nous proposons une approche de test boîte grise consistant à simuler les services partenaires de cet orchestrateur. Nous avons abordé ces problématiques à la fois d'un point de vue théorique et pratique. En plus de la proposition d'une modélisation formelle de l'orchestration de services et d'un algorithme de génération de cas de test temporisés, nous avons implémenté ces deux concepts en développant deux prototypes. BPEL2IF permet de transformer une orchestration de services décrite en BPEL en une spécification formelle à base d'automates temporisés (spécification IF). TestGen-IF permet de dériver automatiquement des cas de test temporisés. Enfin, pour valider notre démarche, nous avons appliqué notre approche de test à des cas d'études de taille réelle.

L'une des façons les plus efficace de s'assurer du bon fonctionnement d'un système informatique est de les représenter par des modèles mathématiques. De nombreux travaux ont été réalisés en utilisant des automates finis comme modèles, nous essayons ici d'étendre ces travaux à des modèles infinis. Dans cette thèse, nous nous intéressons à quelques problèmes dans lesquels un système est observé de façon incomplète. Dans ce cas, il est impossible d'accéder à certaines informations internes. La diagnosticabilité d'une propriété donnée consiste à vérifier qu'à l'exécution du système, un observateur sera en mesure de déterminer avec certitude que la propriété est vérifiée par le système. L'opacité consiste, réciproquement, à déterminer qu'un doute existera toujours. Une autre application concerne la génération de cas de test. Une fois encore, on considère qu'un observateur n'accède qu'à une partie des événements se produisant dans le système (en général les entrées et les sorties). À partir d'une spécification, on produit automatiquement des cas de test, qui ont pour but de détecter des non-conformités (elles même formalisées de façon précise). Ces trois problèmes ont été étudiés pour des modèles finis. Dans cette thèse, nous étendons leur étude aux modèles récursifs, pour cela nous avons introduit notre propre modèle, les RTS, qui sont une généralisation des automates à pile, et d'autres modèles de la récursivité. Nous adaptons ensuite les techniques utilisées sur des modèles finis, qui servent à résoudre les problèmes qui nous intéressent.

L'une des façons les plus efficace de s'assurer du bon fonctionnement d'un système informatique est de les représenter par des modèles mathématiques. De nombreux travaux ont été réalisés en utilisant des automates finis comme modèles, nous essayons ici d'étendre ces travaux à des modèles infinis. Dans cette thèse, nous nous intéressons à quelques problèmes dans lesquels un système est observé de façon incomplète. Dans ce cas, il est impossible d'accéder à certaines informations internes. La diagnosticabilité d'une propriété donnée consiste à vérifier qu'à l'exécution du système, un observateur sera en mesure de déterminer avec certitude que la propriété est vérifiée par le système. L'opacité consiste, réciproquement, à déterminer qu'un doute existera toujours. Une autre application concerne la génération de cas de test. Une fois encore, on considère qu'un observateur n'accède qu'à une partie des événements se produisant dans le système (en général les entrées et les sorties). À partir d'une spécification, on produit automatiquement des cas de test, qui ont pour but de détecter des non-conformités (elles même formalisées de façon précise). Ces trois problèmes ont été étudiés pour des modèles finis. Dans cette thèse, nous étendons leur étude aux modèles récursifs, pour cela nous avons introduit notre propre modèle, les RTS, qui sont une généralisation des automates à pile, et d'autres modèles de la récursivité. Nous adaptons ensuite les techniques utilisées sur des modèles finis, qui servent à résoudre les problèmes qui nous intéressent. / An effective way to ensure the proper functioning of a computer system is to represent it by using mathematical models . Many studies have been conducted using finite automata as models, in this thesis we try to extend these works to infinite models. We focus on three problems in which a system is partially observed. In this case, it is impossible to access certain internal informations. Diagnosability of a given property consist in checking, that, during the execution of the system, an observer will be able to determine with certainty that the property is verified by the system. Conversely, the opacity consists in determining if a doubt will always exist. Another application is the generation of test cases. Once again, we consider that an observer accesses only some events of the system (typically the inputs and outputs): from a specification, we automatically generate test cases, which are designed to detect non-conformance. These three problems have been studied for finite models. In this thesis, we extend their study to recursive models. For this purpose, we have introduced a new model, the RTS, which are a generalization of pushdown automata and other models of recursion. In order to solve problems of interest, we adapt the techniques used in finite models.