Test de systèmes temps-réel à base de modèle
Institution:
Université Joseph Fourier (Grenoble)Disciplines:
Directors:
Abstract EN:
We are interested in model-based testing for real-time systems. Specifically, we study two classes of problems, namely: (I) state identification problems and (II) black-box conformance testing. For state identification problems, we are given the model of a machine with an initial unknown state and we look for an experiment to apply on the machine to identify the initial unknown state or the final state to which the machine has moved after the experiment. For black-box conformance testing, we are given a model of the machine and we want to check whether the machine conforms to its model or not. Our framework is mainly based on the model of partially-observable, nondeterministic timed automata. We argue that partial observability and non-determinism are essential features for ease of modeling, expressiveness and implementability. The framework allows the user to define, through appropriate modeling, assumptions on the environment of the system under test (SUT) as well as on the interface between the tester and the SUT. Before solving state identification problems for timed automata, we study these problems for the case of finite state transducers (FST). FST is an extension of the Mealy machine model. We show that these problems are undecidable for FST in general. We consider a subclass of FST, so-called, wait-synchronize transducers (WSFST) for which these problems are decidable. The first step to solve state identification problems for timed automata, consists in computing the time-abstracting bisimulation (TAB) quotient graph of the considered timed automaton. The second step is to transform this graph into a Mealy machine on which state-identification problems can be solved using existing techniques. For conformance testing, we consider two types of tests: analog-clock tests and digital-clock tests. Our algorithm to generate analog-clock tests is based on an on-the-fly determinization of the specification automaton during the execution of the test, which in turn relies on reachability computations. The latter can sometimes be costly, thus problematic, since the tester must quickly react to the actions of the system under test. Therefore, we provide techniques which allow analog-clock testers to be represented as deterministic timed automata, thus minimizing the reaction time to a simple state jump. We provide algorithms for static or on-the-fly generation of digital-clock tests. These tests measure time only with finite-precision, digital clocks, an essential condition for implementability. We propose a technique for location, edge and state coverage of the specification, by reducing the problem to covering a symbolic reachability graph. This avoids having to generate too many tests. We also propose digital-clock test generation techniques based on action refinement in order to reduce the size of generated tests. We report on a prototype tool TTG and four case studies: a lighting device, the Bounded Retransmission Protocol, the K9 Mars Rover (NASA) and the Dala Robot (LAAS).
Abstract FR:
Nous sommes interesses par le test de systemes temps-reels a base de modele. Plus precisement, nous etudions deux classes de problemes, a savoir: (1) les problemes d'identification d'etat (II) le test de conformite en boite noire. Pour les problemes d'identification d'etat, nous disposons du modele de la machine dont nous ignorons l'etat initial et nous cherchons une experience a appliquer sur cette machine afin d'identifier l'etat initial inconnu ou l'etat final vers lequel la machine a evolue suite a cette experience. Pour le test de conformite, nous disposons du modele de la machine et nous voulons tester si la machine est conforme a son modele ou pas. Notre approche est basee principalement sur le modele d'automate temporise non-deterministe et partiellement observable. L'observabilite partielle et le non-determinisme sont des elements essentiels pour simplifier la modelisation ainsi que pour augmenter l'expressivite et l'implementabilite des systemes. Ce cadre permet'a l'utilisateur de definir, par une modelisation appropriee, des hypotheses sur l'environnement du systeme sous test (SST) ainsi que sur l'interface entre le testeur et le SST. Avant de resoudre les problemes d'identification d'etat pour le cas des automates temporises, nous etudions ces problemes pour le cas des transducteurs a etats finis(TEF). TEF est une extension du modele de la machine de Mealy. Nous montrons que ces problemes sont indecidables pour les TEF en general. Nous considerons une sous-classe de TEF, nommee, transducteurs avec attente de synchronisation (TEF-AS) pour laquelle ces problemes sont decidables. La premiere etape pour resoudre les problemes d'identification pour le cas des automates temporises consiste a calculer le "time-abstracting bisimulation (TAB) quotient graph" de l'automate temporise en question. La deuxieme etape consiste a transformer ce graphe en une machine de Mealy pour laquelle les problemes d'identification peuvent se resoudre en utilisant des techniques deja existantes. Pour le test de conformite en boite-noire, nous considerons deux types de tests: tests a horloge analogique et tests a horloge numerique. Notre algorithme pour la generation de tests a horloge analogique est base sur la determinisation a-la-volee de l'automate specification, durant l'execution du test, qui repose a son tour sur des calculs d'atteignabilite. Ces derniers peuvent etre parfois couteux, et par consequent problematiques, puisque le testeur doit reagir rapidement aux actions du systeme sous test. Pour cela, nous proposons des techniques permettant de representer les testeurs a horloge analogique sous forme d'automates temporises deterministes, reduisant ainsi le temps de reaction a un simple saut d'etat. Nous proposons des algorithmes de generation statique ou a-la-volee de tests a horloge numerique. Ces tests mesurent le temps avec des horloges numeriques a precision finie, qui est une condition essentielle d'implementabilite. Nous proposons une technique pour la couverture des noeuds, des arcs ou des etats, en reduisant le probleme a une couverture d'un graphe d'atteignabilite symbolique. Ceci permet d'eviter de generer un grand nombre de tests. Nous proposons egalement des techniques de generation de test a horloge numerique basees sur les techniques de raffinement pour reduire la taille des Tests generes. Nous decrivons notre outil prototype TTG ainsi que quatre etudes de cas: un systeme d'eclairage, le Bounded Retransmission Protocol, le K9 Mars Rover (NASA) et le Robot Dala (LAAS).