Abstract
We propose a new framework for black-box conformance testing of real-time systems, based on the model of timed automata. The framework is expressive: it can fully handle partially-observable, non-deterministic timed automata. It also allows the user to define, through appropriate modeling, assumptions on the environment of the system under test (SUT) as well as on the interface between the tester and the SUT. The framework is implementable: tests can be implemented as finite-state machines accessing a finite-precision digital clock. We propose, for this framework, a set of test-generation algorithms with respect to different coverage criteria. We have implemented these algorithms in a prototype tool called TTG. Experimental results obtained by applying TTG on the Bounded Retransmission Protocol show that only a few tests suffice to cover thousands of reachable symbolic states in the specification.
Work partially supported by CNRS STIC project “CORTOS” and by IST Network of Excellence “ARTIST2”.
Chapter PDF
Similar content being viewed by others
References
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Berthomieu, B., Menasche, M.: An enumerative approach for analyzing time Petri nets. IFIP Congress Series 9, 41–46 (1983)
Bozga, M., Fernandez, J.C., Ghirvu, L., Graf, S., Krimm, J.P., Mounier, L.: IF: a validation environment for timed asynchronous systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)
Bozga, M., Graf, S., Kerbrat, A., Mounier, L., Ober, I., Vincent, D.: SDL for Real-Time: What is Missing? In: Proceedings of SAM 2000: 2nd Workshop on SDL and MSC. IMAG, Grenoble, France, June 2000, pp. 108–122 (2000)
Cardell-Oliver, R.: Conformance tests for real-time systems with timed automata specifications. Formal Aspects of Computing 12(5), 350–371 (2000)
Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)
En-Nouaary, A., Dssouli, R., Khendek, F., Elqortobi, A.: Timed test cases generation based on state characterization technique. In: RTSS 1998. IEEE, Los Alamitos (1998)
Fernandez, J.C., Jard, C., Jéron, T., Viho, G.: Using on-the-fly verification techniques for the generation of test suites. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102. Springer, Heidelberg (1996)
Hessel, A., Larsen, K., Nielsen, B., Pettersson, P., Skou, A.: Time-optimal real-time test case generation using UPPAAL. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 114–130. Springer, Heidelberg (2004)
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–146. Springer, Heidelberg (2004)
Kohavi, Z.: Switching and finite automata theory, 2nd edn. McGraw-Hill, New York (1978)
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)
Kuliamin, V., Petrenko, A., Pakoulin, N., Kossatchev, A., Bourdonov, I.: Integration of functional and timed testing of real-time and concurrent systems. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol. 2890, pp. 450–461. Springer, Heidelberg (2004)
Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines - A survey. Proceedings of the IEEE 84, 1090–1126 (1996)
Nielsen, B., Skou, A.: Automated test generation from timed automata. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 343. Springer, Heidelberg (2001)
Petrenko, A., Boroday, S., Groz, R.: Confirming configurations in EFSM testing. IEEE Trans. Software Eng. 30(1) (2004)
Springintveld, J., Vaandrager, F., D’Argenio, P.: Testing timed automata. Theoretical Computer Science 254 (2001)
Tretmans, J.: Testing concurrent systems: A formal approach. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 46–65. Springer, Heidelberg (1999)
Tripakis, S.: Fault diagnosis for timed automata. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, p. 205. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 IFIP International Federation for Information Processing
About this paper
Cite this paper
Krichen, M., Tripakis, S. (2005). An Expressive and Implementable Formal Framework for Testing Real-Time Systems. In: Khendek, F., Dssouli, R. (eds) Testing of Communicating Systems. TestCom 2005. Lecture Notes in Computer Science, vol 3502. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11430230_15
Download citation
DOI: https://doi.org/10.1007/11430230_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26054-7
Online ISBN: 978-3-540-32076-0
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science
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.
