Skip to Main content Skip to Navigation
Master Thesis

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].
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download

https://dumas.ccsd.cnrs.fr/dumas-00530773
Contributor : Co-Responsables Du Mri V. Gouranton Et S. Blazy <>
Submitted on : Friday, October 29, 2010 - 6:46:52 PM
Last modification on : Monday, February 15, 2021 - 10:37:19 AM
Long-term archiving on: : Friday, October 26, 2012 - 12:45:36 PM

Identifiers

  • HAL Id : dumas-00530773, version 1

Citation

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

Share

Metrics

Record views

250

Files downloads

361