Abstract
\({\cal T}\! {\cal H} {\cal O} {\cal T}\! {\cal L}\) represents a conservative extension of \({\cal H} {\cal O} {\cal T}\! {\cal L}\) (Hypotheses and Observations Testing Logic) to deal with systems where time plays a fundamental role. We adapt some of the \({\cal H} {\cal O} {\cal T}\! {\cal L}\) rules to cope with the new framework. In addition, we introduce several specific hypotheses and rules to appropriately express time assumptions. We provide a correctness result of \({\cal T}\! {\cal H} {\cal O} {\cal T}\! {\cal L}\) with respect to a general notion of timed conformance.
This research was partially supported by the Spanish MEC project WEST/FAST TIN2006-15578-C02-01 and the Marie Curie project MRTN-CT-2003-505121/TAROT.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Batth, S.S., Rodrigues Vieira, E., Cavalli, A., Uyar, M.Ü.: Specification of timed EFSM fault models in SDL. In: Derrick, J., Vain, J. (eds.) FORTE 2007. LNCS, vol. 4574, pp. 50–65. Springer, Heidelberg (2007)
Bayse, E., Cavalli, A., Núñez, M., Zaïdi, F.: A passive testing approach based on invariants: Application to the WAP. Computer Networks 48(2), 247–266 (2005)
Bosik, B.S., Uyar, M.Ü.: Finite state machine based formal methods in protocol conformance testing. Computer Networks & ISDN Systems 22, 7–33 (1991)
Brandán Briones, L., Brinksma, E.: Testing real-time multi input-output systems. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 264–279. Springer, Heidelberg (2005)
Brinksma, E., Tretmans, J.: Testing transition systems: An annotated bibliography. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 187–195. Springer, Heidelberg (2001)
Cardell-Oliver, R.: Conformance tests for real-time systems with timed automata specifications. Formal Aspects of Computing 12(5), 350–371 (2000)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)
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)
Fecko, M.A., Uyar, M.Ü., Duale, A.Y., Amer, P.D.: A technique to generate feasible tests for communications systems with multiple timers. IEEE/ACM Transactions on Networking 11(5), 796–809 (2003)
Higashino, T., Nakata, A., Taniguchi, K., Cavalli, A.: Generating test cases for a timed I/O automaton model. In: 12th Int. Workshop on Testing of Communicating Systems, IWTCS 1999, pp. 197–214. Kluwer Academic Publishers, Dordrecht (1999)
Huang, G.-D., Wang, F.: Automatic test case generation with region-related coverage annotations for real-time systems. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 144–158. Springer, Heidelberg (2005)
Krichen, M., Tripakis, S.: An expressive and implementable formal framework for testing real-time systems. In: Khendek, F., Dssouli, R. (eds.) TestCom 2005. LNCS, vol. 3502, pp. 209–225. Springer, Heidelberg (2005)
Ladani, B.T., Alcalde, B., Cavalli, A.R.: Passive testing - a constrained invariant checking approach. In: Khendek, F., Dssouli, R. (eds.) TestCom 2005. LNCS, vol. 3502, pp. 9–22. Springer, Heidelberg (2005)
Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines: A survey. Proceedings of the IEEE 84(8), 1090–1123 (1996)
Merayo, M.G., Núñez, M., Rodríguez, I.: A brief introduction to \(\mathcal{THOTL}\). In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 501–510. Springer, Heidelberg (2007)
Merayo, M.G., Núñez, M., Rodríguez, I.: Formal testing from timed finite state machines. Computer Networks 52(2), 432–460 (2008)
Núñez, M., Rodríguez, I.: Towards testing stochastic timed systems. In: König, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol. 2767, pp. 335–350. Springer, Heidelberg (2003)
Petrenko, A.: Fault model-driven test derivation from finite state models: Annotated bibliography. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 196–205. Springer, Heidelberg (2001)
Rodríguez, I., Merayo, M.G., Núñez, M.: A logic for assessing sets of heterogeneous testing hypotheses. In: Uyar, M.Ü., Duale, A.Y., Fecko, M.A. (eds.) TestCom 2006. LNCS, vol. 3964, pp. 39–54. Springer, Heidelberg (2006)
Rodríguez, I., Merayo, M.G., Núñez, M.: \(\mathcal{HOTL}\): Hypotheses and observations testing logic. Journal of Logic and Algebraic Programming 74(2), 57–93 (2008)
Springintveld, J., Vaandrager, F., D’Argenio, P.R.: Testing timed automata. Theoretical Computer Science 254(1-2), 225–257 (2001); Previously appeared as Technical Report CTIT-97-17, University of Twente (1997)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 IFIP International Federation for Information Processing
About this paper
Cite this paper
Merayo, M.G., Núñez, M., Rodríguez, I. (2008). \({\cal T}\! {\cal H} {\cal O} {\cal T}\! {\cal L}\): A Timed Extension of \({\cal H} {\cal O} {\cal T}\! {\cal L}\) . In: Suzuki, K., Higashino, T., Ulrich, A., Hasegawa, T. (eds) Testing of Software and Communicating Systems. FATES TestCom 2008 2008. Lecture Notes in Computer Science, vol 5047. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68524-1_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-68524-1_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68514-2
Online ISBN: 978-3-540-68524-1
eBook Packages: Computer ScienceComputer Science (R0)