Couverture de tests d'automates temporisés
Mots clés : Test, méthodes formelles, automates temporisés, déterminisation.
Encadreurs: Nathalie Bertrand (Nathalie.Bertrand@irisa.fr), Thierry Jéron (Thierry.Jeron@irisa.fr),
Description :
Le modèle des automates temporisés d'Alur et Dill [AD94] est un modèle standard pour représenter des systèmes réactifs soumis à des contraintes temps-réelles, et sur lequel beaucoup de recherches se sont focalisées sur la vérification formelle, le contrôle, le diagnostic et le test. Dans ce stage, on s'intéresse plus particulièrement à la génération automatique de tests de conformité à partir de tels modèles. Cette problématique a déjà été étudiée, avec l'émergence de théories du test de conformité et des algorithmes de géneration fondés sur la vérification symbolique [NS03,KT04,BB05,ST08].
Un des problèmes de la génération de tests est celui de la couverture des tests dont le but est de produire un ensemble de tests qui couvrent au mieux les comportements des modèles, et sont éventuellement à même de détecter plus d'erreurs dans les implémentations. Les critères existants sont essentiellement syntaxiques (e.g. couverture des localités, des transitions, des branches) voire légèrement sémantiques (couverture des conditions booléennes) [ZHM97]. Mais peu s'intéressent à la couverture réelle de la sémantique définie en termes des comportements.
Après une étude bibliographique basée sur les références citées ci dessus, le but du stage sera d'étudier les problématiques de couverture de test pour les automates temporisés, en s'attachant à exhiber des critères sémantiques plus significatifs que les critères de couverture syntaxiques usuels [ZHM97] (en s'inspirant par exemple des travaux de [ND07]), et à exhiber les algorithmes de génération de tests correspondants.
Prérequis : a réalisation de ce stage nécessite de suivre le module VTS.
Bibliographie : [AD94] R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994.
[BB05] E. Brinksma and L. B. Briones. A test generation framework for quiescent real-time systems. In Formal Approaches to Software Testing, 4th International Workshop, FATES 2004, Linz, Austria, LNCS No 3395. Springer, 2005.
[KT04] M. Krichen and S. Tripakis. Black-box conformance testing for real-time systems. In 11th International SPIN Workshop, Barcelona, Spain, LNCS No 2989. Springer, 2004.
[ND07] T. Nahhal and T. Dang. Test Coverage for Continuous and Hybrid Systems. In CAV 2007 - Computer Aided Verification, Berlin, Germany, July 2007.
[NS03] B. Nielsen and A. Skou. Automated test generation from timed automata. International Journal on Software Tools for Technology Transfer (STTT), vol 5, 2003.
[ST08] J. Schmaltz and J. Tretmans. On conformance testing for timed systems. In 6th International Conference, FORMATS 2008, Saint Malo, France, number 5215 in LNCS, p 15-17. Springer, 2008.
[ZHM97] Zhu, H., Hall, P. A., and May, J. H. 1997. Software unit test coverage and adequacy. ACM Computing Survey, 29, 4 (Dec. 1997), 366-427.