Test de systèmes temps réel à l’aide du forçage en ligne

Real-time systems must conform to requirements of correctness and safety, which requires testing them. In this thesis, we propose a method that allows to force an execution of a real-time system so as to reach a chosen state. This technique can be used to test real-time systems in situations where the chosen state could be hard to reach when dealing with the input sequence of the system alone. One example of an application could be that of a state that triggers a redundancy mechanism when reached, the execution of which would be infrequent, but that still requires testing. In this use case, it is effectively fault injection in the system. This solution is based on an offline analysis of a set of behavioral models of the system, using the formalism of durational Kripke structures. The models of the system are obtained through a Model Driven Engineering approach, and present the behaviors of the tasks from the point of view of the real-time operating system. Using a parametrization, transformation and composition of the models, we perform a parametric analysis of the resulting Time Petri net. Thanks to the result of this analysis, we establish a set of delays to be added to the execution of the system so as to reach the chosen state. With the help of an embedded model of the different tasks of the system, and through the means of a controller embedded in the real-time operating system, we perform the runtime enforcement of the system so as to make it reach the chosen state, and possibly allow for testing the execution starting from this state. This thesis details the formalisms used to model the application, the way in which the models are modified and analyzed to obtain the execution delays, as well as the implementation in a real-time operating system: TrampolineRTOS.Les systèmes temps réel doivent répondre à des contraintes d’exactitude et de sureté de fonctionnement, ce qui nécessite de pouvoir les tester. Dans ces travaux de thèse, nous proposons une méthode permettant de forcer une exécution d’un système temps réel de manière à atteindre un état choisi. Cette technique peut permettre le test de systèmes temps réel dans des situations où l’état choisi pourrait être compliqué à atteindre en ne manipulant que les données d’entrée du système. Un exemple d’application pourrait être celui d’un état déclenchant un redondant, et dont l’exécution serait peu fréquente, mais que l’on souhaite néanmoins tester. Dans ce cas d’utilisation, il s’agit effectivement de l’injection de fautes dans le système. Cette solution est basée sur une analyse hors-ligne d’un ensemble de modèles comportementaux du système, utilisant le formalisme des structures de Kripke à durée. Les modèles du système sont issu d’une démarche IDM, et présentent le comportement des tâches du point de vue du système d’exploitation temps réel. À l’aide d’une paramétrisation, transformation et composition des modèles, nous effectuons une analyse paramétrée du réseau de Petri temporel résultant. Grâce au résultat de cette analyse, nous déterminons un ensemble de délais à ajouter à l’exécution du système afin de forcer le système à atteindre l’état choisi. En utilisant un modèle embarqué des différentes tâches, et par le biais d’un contrôleur intégré au système d’exploitation temps réel, nous effectuons le forçage en ligne du système afin de permettre l’atteinte de l’état choisi, et éventuellement le test de l’exécution découlant de cet état. Ce travail de thèse détaille les formalismes utilisés pour modéliser l’application, la manière dont ils sont modifiés et analysés pour obtenir les délais d’exécution, ainsi que l’implémentation dans un système d’exploitation temps réel : TrampolineRTOS