Abstract
This paper proposes novel off-line test generation techniques for non-deterministic timed automata with inputs and outputs (TAIOs) in the formal framework of the tioco, conformance theory. In this context, a first problem is the determinization of TAIOs, which is necessary to foresee next enabled actions, but is in general impossible. This problem is solved here thanks to an approximate determinization using a game approach, which preserves tioco, and guarantees the soundness of generated test cases. A second problem is test selection for which a precise description of timed behaviors to be tested is carried out by expressive test purposes modeled by a generalization of TAIOs. Finally, using a symbolic co-reachability analysis guided by the test purpose, test cases are generated in the form of TAIOs equipped with verdicts.
This work was partly funded by the french ANR project Testec. An extended version of the paper with full proofs is available as a technical report[4].
Chapter PDF
Similar content being viewed by others
Keywords
References
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163–178. Springer, Heidelberg (1998)
Bérard, B., Gastin, P., Petit, A.: On the power of non-observable actions in timed automata. In: Puech, C., Reischuk, R. (eds.) STACS 1996. LNCS, vol. 1046, pp. 255–268. Springer, Heidelberg (1996)
Bertrand, N., Jéron, T., Stainer, A., Krichen, M.: Off-line test selection with test purposes for non-deterministic timed automata. Technical Report 7501, INRIA (January 2011), http://hal.inria.fr/inria-00550923
Bertrand, N., Stainer, A., Jéron, T., Krichen, M.: A game approach to determinize timed automata. In: FOSSACS 2011 (to appear, 2011); Extended version as INRIA report 7381, http://hal.inria.fr/inria-00524830
Briones, L.B., Brinksma, E.: A test generation framework for quiescent real-time systems. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 64–78. Springer, Heidelberg (2005)
David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed I/O automata: a complete specification theory for real-time systems. In: HSCC 2010, pp. 91–100. ACM Press, New York (2010)
David, A., Larsen, K.G., Li, S., Nielsen, B.: Timed testing under partial observability. In: ICST 2009, pp. 61–70. IEEE Computer Society, Los Alamitos (2009)
En-Nouaary, A., Dssouli, R.: A guided method for testing timed input output automata. In: Hogrefe, D., Wiles, A. (eds.) TestCom 2003. LNCS, vol. 2644, pp. 211–225. Springer, Heidelberg (2003)
Finkel, O.: Undecidable problems about timed automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 187–199. Springer, Heidelberg (2006)
Jard, C., Jéron, T.: TGV: theory, principles and algorithms. Software Tools for Technology Transfer 7(4), 297–315 (2005)
Khoumsi, A., Jéron, T., Marchand, H.: Test cases generation for nondeterministic real-time systems. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 131–145. Springer, Heidelberg (2004)
Koné, O., Castanet, R., Laurencot, P.: On the fly test generation for real time protocols. In: ICCCN 1998, pp. 378–387. IEEE, Los Alamitos (1998)
Krichen, M., Tripakis, S.: Conformance testing for real-time systems. Formal Methods in System Design 34(3), 238–304 (2009)
Nielsen, B., Skou, A.: Automated test generation from timed automata. Software Tools for Technology Transfer 5(1), 59–77 (2003)
Schmaltz, J., Tretmans, J.: On conformance testing for timed systems. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 250–264. Springer, Heidelberg (2008)
Tretmans, J.: Test generation with inputs, outputs and repetitive quiescence. Software - Concepts and Tools 3, 103–120 (1996)
Tripakis, S.: Folk theorems on the determinization and minimization of timed automata. Information Processing Letters 99(6), 222–226 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bertrand, N., Jéron, T., Stainer, A., Krichen, M. (2011). Off-Line Test Selection with Test Purposes for Non-deterministic Timed Automata. In: Abdulla, P.A., Leino, K.R.M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2011. Lecture Notes in Computer Science, vol 6605. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19835-9_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-19835-9_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19834-2
Online ISBN: 978-3-642-19835-9
eBook Packages: Computer ScienceComputer Science (R0)