Abstract
TorX is a specification-based, on-the-fly testing tool that tests for ioco conformance of implementations w.r.t. a formal specification. This paper describes an extension of TorX to not only allow testing for functional correctness, but also for correctness w.r.t. timing properties expressed in the specification. An implementation then passes a timed test if it passes according to ioco, and if occurrence times of outputs or of quiescence signals are legal according to the specification. The specifications are described by means of non-deterministic safety timed automata. This paper describes the basic algorithms for ioco, the necessary modifications to standard safety timed automata to make them usable as an input formalism, a test-derivation algorithm from timed automata, and the concrete algorithms implemented in TorX for timed testing. Finally, practical concerns with respect to timed testing are discussed.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comp. Science 126(2), 183–235 (1994)
Belinfante, A.: Timed testing with TorX: The Oosterschelde storm surge barrier. In: Gijsen, M. (ed.) Handout 8e Nederlandse Testdag, Rotterdam. CMG (2002)
Belinfante, A., Feenstra, J., Heerink, L., de Vries, R.G.: Specification based formal testing: The easylink case study. In: 2nd Workshop Emb. Systems (PROGRESS 2001), pp. 73–82 (2001)
Belinfante, A., Feenstra, J., de Vries, R.G., Tretmans, J., Goga, N., Feijs, L., Mauw, S., Heerink, L.: Formal test automation: A simple experiment. In: Csopaki, G., Dibuz, S., Tarnay, K. (eds.) 12th Int. Workshop on Testing of Communicating Systems, pp. 179–196. Kluwer, Dordrecht (1999)
Bengtsson, J., Yi, W.: In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)
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)
de Alfaro, L., Faella, M., Stoelinga, M.: Linear and branching metrics for quantitative transition systems. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 97–109. Springer, Heidelberg (2004)
Fernandez, J.-C., Jard, C., Jeron, T., Viho, C.: Using on-the-fly verification techniques for the generation of test suites. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 348–359. Springer, Heidelberg (1996)
Fernandez, J.-C., Jard, C., Jeron, T., Viho, C.: An experiment in automatic generation of test suites for protocols with verification technology. Science of Computer Programming 29(1–2), 123–146 (1997); Special Issue on COST 247, Verification and Validation Methods for Formal Descriptions
Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Journal Inf. and Comp. 111(2), 193–244 (1994)
Krichen, M., Tripakis, S.: Black-box conformance testing for real-time systems. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 109–126. Springer, Heidelberg (2004)
Mikucionis, M., Nielsen, B., Larsen, K.G.: Real-time system testing on-the-fly. In: Sere, K., Waldén, M. (eds.) 15th Nordic Workshop on Programming Theory, Abo Akademi, vol. 34, pp. 36–38. Department of Computer Science, Finland (2003)
Springintveld, J.G., Vaandrager, F.W., D’Argenio, P.R.: Testing timed automata. Theoretical Computer Science 254(1–2), 225–257 (2001)
Tretmans, J.: Test Generation with Inputs, Outputs and Repetitive Quiescence. Software—Concepts and Tools 17(3), 103–120 (1996)
Tretmans, J., Brinksma, H.: Torx: Automated model based testing. In: Hartman, A., Dussa-Ziegler, K. (eds.) 1st European Conf. on Model-Driven Software Engineering, Nürnberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bohnenkamp, H., Belinfante, A. (2005). Timed Testing with TorX. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds) FM 2005: Formal Methods. FM 2005. Lecture Notes in Computer Science, vol 3582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11526841_13
Download citation
DOI: https://doi.org/10.1007/11526841_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27882-5
Online ISBN: 978-3-540-31714-2
eBook Packages: Computer ScienceComputer Science (R0)