Soutenance mémoire
Introduction
Les syst`emes temps-r´eel sont r´epandus et souvent critiques, c’est-`a-dire qu’une erreur au cours de leur fonctionnement peut avoir des cons´equences graves. Pour rendre leur utilisation plus sˆure, il existe plusieurs m´ethodes telles que la v´erification ou le test que l’on dispose ou non du mod`ele du syst`eme, ou encore le contrˆole pour empˆecher les comportements fautifs. Dans ce rapport, nous nous consacrons `a la mod´elisation par automates temporis´es qui est tout `a fait adapt´ee aux syst`emes temps-r´eel. Plus pr´ecis´ement nous approfondirons la question de la d´eterminisation des automates temporis´es pour la g´en´eration de test.
Nous nous int´eressons particuli`erement au cas du test de conformit´e. On souhaite v´erifier qu’un syst`eme « boˆıte-noire », une impl´ementation dont on ne peut observer que les entr´ees et sorties, est conforme `a une sp´ecification donn´ee. Pour essayer de r´epondre `a cette question, on interagit avec l’impl´ementation. On g´en`ere des entr´ees et on observe les sorties, on d´etecte alors d’´eventuelles erreurs de conformit´e par rapport `a la sp´ecification. Il y a deux grandes approches pour faire du test, on-line et off-line. Le test on-line consiste en la g´en´eration du test durant son ex´ecution. Il implique la d´eterminisation `a la vol´ee car on a besoin de savoir en permanence, quelles actions sont possibles dans la sp´ecification. `A chaque ´etape, on calcule donc l’ensemble des ´etats accessibles par la s´equence d’actions en cours. Le test on-line de syst`emes temps-r´eel est difficilement r´ealisable pour les sp´ecifications non-d´eterministes pour des raisons ´evidentes de temps de calcul. D’autre part, le test off-line consiste en la generation pr´ealable de cas de test, dans notre cas sous forme d’automates temporises, puis leur execution.
Contrairement au test on-line, cette approche permet d’appliquer la meme serie de cas de test a plusieurs impl´ementations. On peut alors fournir une certification, par exemple, on peut generer un ensemble de cas de test que l’implementation devra passer pour etre validee. Pour la g´en´eralit´e des cas de test g´en´er´es, il est necessaire de se baser sur une specification eterministe. Sinon, on ne g´en`ererait que des cas de test arborescents de hauteur finie. C’est pour cela que nous nous int´eressons `a la determinisation des automates temporis´es et `a l’approximation d´eterministe pr´eservant la conformit´e, c’est-`a-dire telle que toute implementation conforme `a la sp´ecification non-d´eterministe soit conforme `a l’approximation.
Les automates temporis´es sont un modele introduit par Alur et Dill en 1994 [AD94], obtenu en munissant les automates finis d’horloges continues. Ce mod`ele est couramment utilise en v´erification. La d´ecidabilit´e de l’accessibilite dans un automate temporis´e est une propriete primordiale dans l’utilisation de ce mod`ele pour la v´erification et pour le test. Tout comme les automates finis, les automates temporis´es ne sont pas necessairement deterministes, mais ils ne sont pas non plus determinisables en g´en´eral [AD94]. Quelques classes d’automates ´eterminisables sont pr´esent´ees dans [BBBB09]. Pour la probl´ematique de la v´erification, il est essentiel pour l’expressivit´e d’autoriser la mod´elisation des sp´ecifications par des automates non-d´eterministes. Malheureusement, pour la g´en´eration des cas de tests, le d´eterminisme est primordial pour l’efficacit´e des calculs. Dans de nombreux travaux, on se restreint a des classes d’automates temporis´es determinisables, quand ce n’est pas `a des automates deterministes. Krichen et Tripakis proposent une solution `a ce probl`eme [KT09]. Ils presentent une methode de sur-approximation deterministe des automates temporis´es sur laquelle on pourrait generer les cas de tests au risque de perdre en pr´ecision. La m´ethode n´ecessite une hypothese contraignante sur la sp´ecification pour pr´eserver la relation de conformit´e, mais cela permet d’´elargir le champ d’application des outils de mod´elisation a des automates non-deterministes, ce qui est consid´erable. D’un autre cote, l’article [BBBB09] presente une heuristique de d´eterminisation. Lorsqu’elle termine, elle produit un d´eterminis´e de l’automate en argument et elle termine sur plusieurs classes d’automates temporis´es d´eterminisables.
Le principal r´esultat de ce stage a ´et´e de d´evelopper une approche par le jeu qui recouvre les deux m´ethodes actuelles de d´eterminisation. Cette approche est inspir´ee d’un travail sur les automates temporis´es pour un tout autre probl`eme : la diagnosticabilite a ressources fix´ees [BCD05]. Notre m´ethode produit un d´eterminis´e si possible, une sur-approximation d´eterministe sinon, et elle est `a la fois plus g´en´erale que la proc´edure [BBBB09] et plus pr´ecise que la sur-approximation [KT09].
Au d´ebut de ce stage, nous avions ´elargi le domaine d’application de [BBBB09] grˆace `a une m´ethode d’analyse statique d´ej`a existante pr´esent´ee dans [DY96]. Cette proc´edure diminue le nombre d’horloges d’un automate temporis´e en consid´erant l’ensemble des horloges actives dans chaque localit´e. Cette analyse permet de lisser le comportement des horloges et de supprimer des comportements inutiles qui empˆechaient la terminaison de la m´ethode [BBBB09].
L’algorithme introduit des transferts d’horloges sur les transitions, mais la procedure de ´eterminisation [BBBB09] s’adapte naturellement aux automates avec transferts. De plus, il existe une construction pour supprimer les transferts sans ajouter d’horloges [Bou09]. Nous avons illustr´e ce travail par des exemples ´etendant strictement le domaine de [BBBB09]. Ce travail, bien qu’int´eressant, n’est pas pr´esent´e dans ce rapport car le domaine d’application de cette procedure am´elior´ee reste inclus dans l’ensemble des automates temporis´es que notre approche par le jeu d´eterminise exactement. Par ailleurs, cette analyse ne permet pas d’´etendre le domaine d’application de notre approche de d´eterminisation qui est robuste aux comportements parasites.
Enfin, nous avons appliqu´e notre m´ethode de d´eterminisation `a la probl´ematique du test de conformit´e avec sp´ecification sous forme d’automate temporis´e. Nous avons tout d’abord propos ´e une formalisation pour la g´en´eration de cas de test `a partir de sp´ecifications d´eterministes. Une adaptation de notre approche pour sous-approximer sur les entr´ees et sur-approximer sur les sorties nous permet de fournir une approximation pr´eservant la conformit´e. Grˆace `a cela, nous pouvons g´en´erer des cas de test corrects (ne produisant pas de faux n´egatifs) `a partir d’une sp´ecification non-d´eterministe. Nous avons ensuite pr´esent´e un mod`ele d’automates temporis´es ouverts, c’est-`a-dire d’automates temporis´es capables d’observer des horloges d’un environnement et en particulier d’un autre automate temporis´e. Nous avons alors utilise ce mod`ele pour formaliser la notion d’objectif de test. Tout cela nous a permis de formaliser la g´en´eration de cas de test correct avec sp´ecification et objectif a priori non-d´eterministes.
La suite de ce document se d´ecompose en trois parties. La premi`ere partie est consacr´ee `a la pr´esentation des automates temporis´es et des principaux r´esultats utiles pour les autres parties de ce rapport, en particulier relatifs au probl`eme de la d´eterminisation des automates temporises.
Dans la seconde partie, on pr´esentera notre approche par le jeu pour la d´eterminisation ainsi que ses propri´et´es. La derni`ere partie pr´esentera la probl´ematique du test et notre travail de formalisation pour la g´en´eration de test `a partir d’une specification a priori non-deterministe avec, ´eventuellement, un objectif pas n´ecessairement d´eterministe.
Sur-approximation [KT09]
Krichen et Tripakis ont propose un algorithme [KT09] qui, etant donne un TA A et un nombre d’horloges k, fournit un DTA `a k horloges reconnaissant un langage contenant le langage du TA initial. Dans [KT09], la procedure est presentee avec une seule horloge, mais les auteurs expliquent que la construction s’adapte `a plusieurs horloges. Il est en fait possible de choisir un comportement plus fin pour les horloges d’observation. Ce comportement doit etre donne sous la forme d’un automate fini nomme squelette dont l’alphabet est le produit cartesien de l’alphabet de A par l’ensemble des horloges d’observation. Une transition fait correspondre `a une action, un ensemble d’horloges `a reinitialiser.
Expliquons le principe de la construction quand on ne s’autorise qu’une seule horloge y quel’on ´einitialise `a chaque transition. Les localit´es de l’automate construit sont ´etiquetees par un ensemble de couples compos´es d’une localite dans le TA initial et d’une zone des valuations des horloges initiales possibles. Cette zone sur les horloges initiales est exprimee en fonction de y. L’approximation est faite sur les gardes des transitions qui sont exprimees avec la seule horloge de la sur-approximation. La construction se fait `a partir de la localite (l0, x = y) o`u l0 est la localite initiale du TA en argument, x une horloge de A et y l’horloge de l’approximation.
Elle s’effectue ensuite par calculs successifs des meilleures sur-approximations des gardes des transitions tirables. La Figure 11 illustre cette construction sur un exemple.
Conclusion de la Section 2
A present que nous avons introduit les éléments de théorie des automates temporises nécessaires a la comprehension de notre travail, nous allons pr´esenter en Section 3, le coeur du stage : notre approche par le jeu pour la determinisation des TAs. Dans cette partie, nous avons vu deux approches diff´erentes : une qui a privil´egi´e l’exactitude `a la terminaison et l’autre qui a decide de faire une sur-approximation pour pouvoir terminer dans tous les cas. L’approche que nous presentons dans la Section 3 assure la terminaison dans tous les cas et l’exactitude dans plus de cas que ceux trait´es par la proc´edure de [BBBB09]. Comme Krichen et Tripakis, lorsqu’on ne peut etre exact, on produit une sur-approximation d´eterministe. Notre methode est `a la fois plus generale que la proc´edure [BBBB09] et plus precise que la sur-approximation [KT09]. 3 Une approche par le jeu pour determiniser les automates temporises.
Introduction
Certains automates temporis´es, bien que determinisables, ne verifient pas les hypotheses necessaires pour la proc´edure de d´eterminisation [BBBB09]. Pour ´etendre la classe des automates que l’on sait d´eterminiser, on veut prendre en compte les dependances entre horloges de la forme x = y + c avec c ∈ N et utiliser ces relations pour obtenir une sur-approximation dans le cas o`u les horloges donn´ees ne sont pas suffisantes. Notre methode est bas´ee sur les mˆemes calculs que dans [KT09] mais elle consiste `a chercher les meilleures r´einitialisations possibles `a chaque transition. Pour cela, on construit un jeu fini turn-based de sˆuret´e GA,(1,My) [GTW]. Le joueur qui veut rester dans des etats surs est “Determinisator”, il choisit les reinitialisations. L’autre joueur est “Spoiler” et il choisit la transition. On obtient l’implication suivante.
Un jeu pour la d´eterminisation d’un TA A avec la pr´ecision (1,My)
Description informelle
On se donne un TA quelconque A. On souhaite construire un determinise de A si possible, une sur-approximation deterministe sinon. Pour cela, on se donne une horloge y, ce sera la seule horloge de l’automate que l’on va construire. Avec cette horloge, on va estimer les valeurs des horloges de A pour construire les transitions. Notre approche se base sur la construction d’un jeu turn-based fini de suret´e dont les joueurs sont Spoiler et Determinisator. Determinisator choisit quand r´einitialiser y et les choix de Spoiler sont des couples (a, r) o`u a est une action et r une r´egion sur y. Une strat´egie positionnelle de Determinisator correspond alors `a un TA d´eterministe dont une transition est compos´ee d’une tour de jeu de Spoiler puis de determinisator.
Dans l´etude des strat´egies gagnantes d’un jeu fini de sˆuret%B
