Test d'automates temporisés - DUMAS - Dépôt Universitaire de Mémoires Après Soutenance Accéder directement au contenu
Mémoires Année : 2010

Test d'automates temporisés

Résumé

Les automates temporisés sont un modèle introduit par Alur et Dill en 1994 [AD94], obtenu en munissant les automates finis d'horloges continues. Ce modèle est couramment utilisé en vérification. La décidabilité de l'accessibilité dans un automate temporisé est une propriété primordiale dans l'utilisation de ce modèle pour la vérification et pour le test. Tout comme les automates finis, les automates temporisés ne sont pas nécessairement déterministes, mais ils ne sont pas non plus déterminisables en général [AD94]. Quelques classes d'automates déterminisables sont présentées dans [BBBB09]. Pour la problématique de la vérification, il est essentiel pour l'expressivité d'autoriser la modélisation des spécifications par des automates non-déterministes. Malheureusement, pour la génération des cas de tests, le déterminisme est primordial pour l'efficacité des calculs. Dans de nombreux travaux, on se restreint à des classes d'automates temporisés déterminisables, quand ce n'est pas à des automates déterministes. Krichen et Tripakis proposent une solution à ce problème [KT09]. Ils présentent une méthode de sur-approximation déterministe des automates temporisés sur laquelle on pourrait générer les cas de tests au risque de perdre en précision. La méthode nécessite une hypothèse contraignante sur la spécification pour préserver la relation de conformité, mais cela permet d'élargir le champ d'application des outils de modélisation à des automates non-déterministes, ce qui est considérable. D'un autre côté, l'article [BBBB09] présente une heuristique de déterminisation. Lorsqu'elle termine, elle produit un déterminisé de l'automate en argument et elle termine sur plusieurs classes d'automates temporisés déterminisables. Le principal résultat de ce stage a été de développer une approche par le jeu qui recouvre les deux méthodes actuelles de déterminisation. Cette approche est inspirée d'un travail sur les automates temporisés pour un tout autre problème : la diagnosticabilité à ressources fixées [BCD05]. Notre méthode produit un déterminisé si possible, une sur-approximation déterministe sinon, et elle est à la fois plus générale que la procédure [BBBB09] et plus précise que la sur-approximation [KT09].
Fichier principal
Vignette du fichier
Stainer_Amelie.pdf (481.23 Ko) Télécharger le fichier
Loading...

Dates et versions

dumas-00530773 , version 1 (29-10-2010)

Identifiants

  • HAL Id : dumas-00530773 , version 1

Citer

Amélie Staïner. Test d'automates temporisés. Théorie et langage formel [cs.FL]. 2010. ⟨dumas-00530773⟩
206 Consultations
200 Téléchargements

Partager

Gmail Facebook X LinkedIn More