Les systèmes réactifs sont modélisés avec différents types d'automates, tels que les systèmes de transitions symboliques à entrée sortie (IOSTS). L'exécution symbolique d'un IOSTS permet la génération de cas de test qui peuvent être exécutés sur une implantation concrète, afin de déterminer si elle est conforme à son modèle. Dans ce document, nous étendons les IOSTS avec des appels de fonctions utilisateur et analysons leur impact sur le système entier et viceversa. Cette thèse comble l'écart entre une approche basée sur le modèle où les fonctions utilisateur sont abstraites et une approche basée sur le code où les petits morceaux de code sont considérés séparément, indépendamment de la façon dont ils sont combinés. Selon le niveau de connaissance que nous avons sur ces fonctions, elles sont modélisées soit par une spécification complète, soit par une spécification partielle, soit juste comme des boîtes noires fournies sans aucune connaissance. Premièrement, lorsque les fonctions sont partiellement connues, nous utilisons des bouchons définis par des tables contenant des tuples représentatifs des données d'entrée/sortie. L'approche proposée emprunte au test "concolic", l'idée de mélanger l'exécution symbolique avec l'information obtenue à partir d'exécutions concrètes des fonctions (tables). Deuxièmement, si l'utilisateur est prêt à fournir d'autres spécifications, il serait intéressant d'utiliser des représentations plus complètes pour les fonctions. Par conséquent, nous proposons d'abstraire des comportements des fonctions par des contrats pré/post. Ensuite, nous étendons l'exécution symbolique en analysant les fonctions via leurs contrats. Enfin, lorsque les fonctions appelées sont complètement inconnues, nous présentons une approche pour extraire de nouveaux contrats pour eux en explorant les contraintes issues de l'exécution symbolique de l'IOSTS. De tels contrats reflètent les contraintes des fonctions qui rendent possible un certain comportement (exigence). / Reactive systems are modeled with various kinds of automata, such as Input Output Symbolic Transition Systems (IOSTS). Symbolic execution over an IOSTS allows test cases generation that can be executed on a concrete implementation, in order to determine whether it is conforming to its model. In this dissertation, we aim at extending the IOSTS framework with explicit user-defined function calls and analyze their impact on a whole system and vice-versa. The thesis bridges the gap between a model-based approach in which user-defined functions are abstracted away and a code-based approach in which small pieces of code are considered separately regardless of the way they are combined. According to the level of knowledge we have about these functions, they are modeled either by a complete specification, a partial specification, or even just as black-boxes provided without any knowledge. First, when functions are partially known, we use function stubs defined by tables containing representative input/output data tuples. The proposed approach borrows from concolic testing, the idea of mixing symbolic execution with information obtained from instrumented concrete executions (function tables). Second, if the user is willing to provide further specifications, it would be interesting to use more complete representations for called functions. Hence, we propose to abstract function behaviors by means of pre/post contracts. Then we extend symbolic execution by analyzing the functions through their contracts. Finally, when called functions are completely unknown, we present an approach to extract new contracts for them by exploring constraints coming from the IOSTS symbolic execution. Such contracts reflect constraints on the functions that make some behavior (requirement) feasible.

En raison de la complexité croissante des systèmes réactifs, le test est devenu un des éléments essentiels dans le processus de leur développement. Les tests de conformité avec des méthodes formelles concernent la correction du contrôle fonctionnel, par le biais des tests d'un système en boîte noire avec une spécification formelle du système. Les techniques passives de test sont utilisées lorsque l’exécution des systèmes testés ne peut pas être perturbée ou l'interface du système n'est pas fournie. Les techniques passives de test sont fondées sur l'observation et la vérification des propriétés du comportement d'un système sans interférer avec son fonctionnement normal. Les tests contribuent également à établir les comportements anormaux pendant l’exécution sur la base de l'observation de toute déviation d'un comportement prédéterminé. L'objectif principal de cette thèse est de présenter une nouvelle approche pour la mise en place des tests passifs fondés sur l'analyse des parties contrôle et données du système sous test. Au cours des dernières décennies, de nombreuses théories et outils ont été développés pour effectuer les tests de conformité. De fait, les spécifications ou les propriétés des systèmes réactifs sont souvent modélisés par différentes variantes de Labeled Transition Systems (LTS). Toutefois, ces méthodes ne prennent pas explicitement en compte les parties données du système, étant donné que le modèle sous-jacent de LTS n’est pas en mesure de le faire. Par conséquent, avec ces approches il est nécessaire d'énumérer les valeurs des données avant la modélisation du système. Cela conduit souvent au problème de l'explosion combinatoire de l'état-espace. Pour palier à cette limitation, nous avons étudié un modèle appelé Input-Output Symbolic Transition Systems (IOSTS) qui inclut explicitement toutes les données d'un système réactif. De nombreuses techniques de tests passives prennent uniquement en considération la partie du contrôle du système en négligeant les données, ou elles sont confrontées à une quantité énorme de données du processus. Dans notre approche, nous prenons en compte la partie contrôle et données en intégrant les concepts d'exécution symbolique et nous améliorons l'analyse de traces en introduisant des techniques de slicing des traces d’exécution. Les propriétés sont décrites à l'aide d'IOSTS et nous illustrons dans notre approche comment elles peuvent être testées sur l'exécution réelle des traces en optimisant l'analyse. Ces propriétés peuvent être conçues pour tester la conformité fonctionnelle d'un protocole ainsi que des propriétés de sécurité. Au-delà de l'approche théorique, nous avons développé un outil logiciel qui implémente les algorithmes présentés dans nos travaux. Enfin, comme preuve de concept de notre approche et de l'outil logiciel, nous avons appliqué les techniques à deux études de cas réels : le protocole SIP et le protocole Bluetooth / Due to the increasing complexity of reactive systems, testing has become an important part in the process of the development of such systems. Conformance testing with formal methods refers to checking functional correctness, by means of testing, of a black-box system under test with respect to a formal system specification, i.e., a specification given in a language with a formal semantics. In this aspect, passive testing techniques are used when the implementation under test cannot be disturbed or the system interface is not provided. Passive testing techniques are based on the observation and verification of properties on the behavior of a system without interfering with its normal operation, it also helps to observe abnormal behavior in the implementation under test on the basis of observing any deviation from the predefined behavior. The main objective of this thesis is to present a new approach to perform passive testing based on the analysis of the control and data part of the system under test. During the last decades, many theories and tools have been developed to perform conformance testing. However, in these theories, the specifications or properties of reactive systems are often modeled by different variants of Labeled Transition Systems (LTS). However, these methodologies do not explicitly take into account the system's data, since the underlying model of LTS are not able to do that. Hence, it is mandatory to enumerate the values of the data before modeling the system. This often results in the state-space explosion problem. To overcome this limitation, we have studied a model called Input-Output Symbolic Transition Systems (IOSTS) which explicitly includes all the data of a reactive system. Many passive testing techniques consider only the control part of the system and neglect data, or are confronted with an overwhelming amount of data values to process. In our approach, we consider control and data parts by integrating the concepts of symbolic execution and we improve trace analysis by introducing trace slicing techniques. Properties are described using Input Output Symbolic Transition Systems (IOSTSs) and we illustrate in our approach how they can be tested on real execution traces optimizing the trace analysis. These properties can be designed to test the functional conformance of a protocol as well as security properties. In addition to the theoretical approach, we have developed a software tool that implements the algorithms presented in this paper. Finally, as a proof of concept of our approach and tool we have applied the techniques to two real-life case studies: the SIP and Bluetooth protocol

Due to the increasing complexity of reactive systems, testing has become an important part in the process of the development of such systems. Conformance testing with formal methods refers to checking functional correctness, by means of testing, of a black-box system under test with respect to a formal system specification, i.e., a specification given in a language with a formal semantics. In this aspect, passive testing techniques are used when the implementation under test cannot be disturbed or the system interface is not provided. Passive testing techniques are based on the observation and verification of properties on the behavior of a system without interfering with its normal operation, it also helps to observe abnormal behavior in the implementation under test on the basis of observing any deviation from the predefined behavior. The main objective of this thesis is to present a new approach to perform passive testing based on the analysis of the control and data part of the system under test. During the last decades, many theories and tools have been developed to perform conformance testing. However, in these theories, the specifications or properties of reactive systems are often modeled by different variants of Labeled Transition Systems (LTS). However, these methodologies do not explicitly take into account the system's data, since the underlying model of LTS are not able to do that. Hence, it is mandatory to enumerate the values of the data before modeling the system. This often results in the state-space explosion problem. To overcome this limitation, we have studied a model called Input-Output Symbolic Transition Systems (IOSTS) which explicitly includes all the data of a reactive system. Many passive testing techniques consider only the control part of the system and neglect data, or are confronted with an overwhelming amount of data values to process. In our approach, we consider control and data parts by integrating the concepts of symbolic execution and we improve trace analysis by introducing trace slicing techniques. Properties are described using Input Output Symbolic Transition Systems (IOSTSs) and we illustrate in our approach how they can be tested on real execution traces optimizing the trace analysis. These properties can be designed to test the functional conformance of a protocol as well as security properties. In addition to the theoretical approach, we have developed a software tool that implements the algorithms presented in this paper. Finally, as a proof of concept of our approach and tool we have applied the techniques to two real-life case studies: the SIP and Bluetooth protocol