Proposition de stage de Master2 Recherche


Implémentation d'un générateur de tests pour Automates Temporisés de type VDTA

Mots-clés: test formel, automates temporisés, génération de test, test à base de modèle, Variable Driven Timed Automata

Contexte

Le test logiciel est une phase très importante et très coûteuse du développement logiciel. L'utilisation de méthodes de test et d'outils de test performants est souvent un gage d'économie de temps et de fiabilité du logiciel.

Travail demandé

Dans la cadre du projet ANR Testec, les membres du LaBRI et de l'Inria Rennes ont travaillé sur une variante des automates temporisés pour modéliser des systèmes à temps continu et à flot de données, le Variable Driven Timed Automaton (VDTA) ([3], [4], [9]). Ils ont ensuite travaillé à la mise au point d'algorithmes de génération de tests à partir de ce modèle. Le premier objectif de ce stage est de développer un outil de génération de tests à partir de VDTA, sur la base des algorithmes déjà écrits mais non implémentés. Dans un deuxième temps, le stagiaire sera amené à réfléchir sur les possibilités de générer des tests à partir d'objectifs de tests et à développer ces approches.

Encadrants / contacts

Antoine Rollet
LaBRI - University of Bordeaux
(+33)5 40 00 35 34
email: rollet__AT__labri.fr

Références


[1] S. Bornot, J. Sifakis, and S. Tripakis, "Modeling urgency in timed systems," in Proc. of COMPOS'97, ser. LNCS. Springer, 1998, pp. 103-129.

[2] R. Barbuti and L. Tesei, "Timed automata with urgent tran- sitions," Acta Inf., vol. 40, no. 5, pp. 317-347, 2004.

[3] O. Nguena-Timo and A. Rollet, "Conformance testing of variable driven automata," in Proc. of WFCS'10. IEEE, 2010, pp. 241-248.

[4] O. Nguena-Timo and A. Rollet. A zone-based reachability analysis of variable driven timed automata. In 3rd International Conference on Advances in System Testing and Validation Lifecycle VALID 2011, Barcelona, Spain, page 7p, 10 2011

[5] R. Cardell-Oliver, "Conformance testing of real-time systems with timed automata specifications," Formal Aspects of Com- puting Journal, vol. 12, no. 5, pp. 350-371, 2000.

[6] J. Springintveld, F. Vaandrager, and P. R. D'Argenio, "Timed Testing Automata," Theor. Comput. Sci., no. 254, pp. 225- 257, 2001.

[7] M. Krichen and S. Tripakis, "Black-box conformance testing for real-time systems," in Proc. of SPIN, ser. LNCS, vol. 2989. Springer, 2004, pp. 109-126.

[8] M. Mikucionis, K. G. Larsen, and B. Nielsen, "T-uppaal: Online model-based testing of real-time systems," in Proc. of ASE'04. IEEE, 2004, pp. 396-397.

[9] O. Nguena-Timo, H. Marchand, and A. Rollet, "Automatic test generation for data-flow reactive systems with time con- straints," in Proc. of ICTSS (Short paper) 2010. CRIM- Canada, 2010, pp. 25-30.

[10] H. B. Mokadem, B. B ' rard, P. Bouyer, and F. Laroussinie, "A new modality for almost everywhere properties in timed automata," in Proc. of CONCUR'05, ser. LNCS, vol. 3653, 2005, pp. 110-124.

[11] R. Alur and D. Dill, "A theory of timed automata," Theor. Comput. Sci., vol. 126, pp. 183-235, 1994.

[12] J. Bengtsson and W. Yi, "Timed automata: Semantics, algo- rithm and tools," in Lectures on Concurrency and Petri Nets, ser. LNCS, vol. 3098. Springer, 2004, pp. 87-124.