Abstract
We present T-Uppaal — a new tool for online black-box testing of real-time embedded systems from non-deterministic timed automata specifications. We describe a sound and complete randomized online testing algorithm and how to implement it using symbolic state representation and manipulation techniques. We propose the notion of relativized timed input/output conformance as the formal implementation relation. A novelty of this relation and our testing algorithm is that they explicitly take environment assumptions into account, generate, execute and verify the result online using the Uppaal on-the-fly model-checking tool engine. A medium size case study shows promising results in terms of error detection capability and computation performance.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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
Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Information and Computation 111(2), 193–244 (1994)
Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126(2), 183–235 (1994)
Behrmann, G., Bengtsson, J., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Uppaal implementation secrets. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 3–22. Springer, Heidelberg (2002)
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: 12th Int. Workshop on Testing of Communicating Systems, pp. 179–196 (1999)
Blom, J., Hessel, A., Jonsson, B., Pettersson, P.: Specifying and generating test cases using observer automata. In: Formal Approaches to Testing of Software, Linz, Austria, September 21. LNCS. Springer, Heidelberg (2004)
Braberman, V., Felder, M., Marré, M.: Testing Timing Behaviors of Real Time Software. In: Quality Week 1997, San Francisco, USA, April-May 1997, pp. 143–155 (1997)
Brinksma, E., Larsen, K.G., Nielsen, B., Tretmans, J.: Systematic Testing of Realtime Embedded Software Systems (STRESS), Research proposal submitted and accepted by the Dutch Research Council (March 2002)
Briones, L.B., Brinksma, E.: A test generation framework for quiescent real-time systems. In: Formal Approaches to Testing of Software, Linz, Austria, September 21. LNCS. Springer, Heidelberg (2004)
Cardell-Oliver, R.: Conformance Testing of Real-Time Systems with Timed Automata. Formal Aspects of Computing 12(5), 350–371 (2000)
Cleaveland, R., Hennessy, M.: Testing Equivalence as a Bisimulation Equivalence. Formal Aspects of Computing 5, 1–20 (1993)
En-Nouaary, A., Dssouli, R., Khendek, F., Elqortobi, A.: Timed Test Cases Generation Based on State Characterization Technique. In: 19th IEEE Real-Time Systems Symposium (RTSS 1998), December 2-4, pp. 220–229 (1998)
Frantzen, L., Tretmans, J., Willemse, T.: Test generation based on symbolic specifications. In: Formal Approaches to Testing of Software, Linz, Austria, September 21. LNCS. Springer, Heidelberg (2004)
Hessel, A., Larsen, K.G., Nielsen, B., Pettersson, P., Skou, A.: Time-Optimal Test Cases for Real-Time Systems. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 114–130. Springer, Heidelberg (2004)
Higashino, T., Nakata, A., Taniguchi, K., Cavalli, A.R.: Generating test cases for a timed i/o automaton model. In: IFIP Int’l Work. Test. Communicat. Syst., pp. 197–214 (1999)
Hong, H.S., Lee, I., Sokolsky, O., Ural, H.: A temporal logic based theory of test coverage and generation. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 327–341. Springer, Heidelberg (2002)
Ouaknine, J., Worrell, J.: Revisiting digitization, robustness, and decidability for timed automata. In: 18th IEEE Symposium on Logic in Computer Science (LICS 2003), Ottawa, Canada, June 2003, pp. 198–207. IEEE Computer Society, Los Alamitos (2003)
Jéron, T., Morel, P.: Test generation derived from model-checking. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 108–121. Springer, Heidelberg (1999)
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)
Larsen, K.G.: A Context Dependent Equivalence Between Processes. Theoretical Computer Science 49, 185–215 (1987)
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)
Mandrioli, D., Morasca, S., Morzenti, A.: Generating Test Cases for Real-Time Systems from Logic Specifications. ACM Transactions on Computer Systems 13(4), 365–398 (1995)
Mikucionis, M., Larsen, K.G., Nielsen, B.: Online on-the-fly testing of real-time systems. Technical Report RS-03-49, Basic Researc. In: Computer Science (BRICS) (December 2003)
Mikucionis, M., Nielsen, B., Larsen, K.G.: Real-time system testing on-the-fly. In: The 15th Nordic Workshop on Programming Theory, Turku, Finland, October 29-31, 2003, vol. 34(B), pp. 36–38 (2003); Åbo Akademi, Department of Computer Science, Finland (Abstracts)
Mikucionis, M., Sasnauskaite, E.: On-the-fly testing using UppAal. Master’s thesis, Department of Computer Science, Aalborg University, Denmark (June 2003)
Nielsen, B., Skou, A.: Automated Test Generation from Timed Automata. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 343–357. Springer, Heidelberg (2001)
Peleska, J., Amthor, P., Dick, S., Meyer, O., Siegel, M., Zahlten, C.: Testing Reactive Real-Time Systems. In: Material for the School – 5th International School and Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 1998), Lyngby, Denmark (1998)
Tripakis, S.: Fault Diagnosis for Timed Automata. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, p. 205. Springer, Heidelberg (2002)
Springintveld, J., Vaandrager, F., D’Argenio, P.R.: Testing Timed Automata. Theoretical Computer Science 254(1-2), 225–257 (2001)
Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 545–558. Springer, Heidelberg (1992)
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)
Tretmans, J., Belinfante, A.: Automatic testing with formal methods. In: EuroSTAR 1999: 7th European Int. Conference on Software Testing, Analysis & Review. EuroStar Conferences, Barcelona, Spain, Galway, Ireland, November 8-12 (1999)
Diekert, V., Gastin, P., Petit, A.: Removing epsilon-Transitions in Timed Automata. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, pp. 583–594. Springer, Heidelberg (1997)
de Vries, R., Tretmans, J., Belinfante, A., Feenstra, J., Feijs, L., Mauw, S., Goga, N., Heerink, L., de Heer, A.: Côte de resyste in Progress. In: STW Technology Foundation (ed.) Progress 2000 – Workshop on Embedded Systems, Utrecht, The Netherlands, October 2000, pp. 141–148 (2000)
de Vries, R.G., Tretmans, J.: On-the-fly conformance testing using Spin. Software Tools for Technology Transfer 2(4), 382–393 (2000)
Yi, W., Pettersson, P., Daniels, M.: Automatic Verification of Real-Time Communicating Systems By Constraint-Solving. In: Hogrefe, D., Leue, S. (eds.) Proc. of the 7th Int. Conf. on Formal Description Techniques, pp. 223–238. North Holland, Amsterdam (1994)
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
Larsen, K.G., Mikucionis, M., Nielsen, B. (2005). Online Testing of Real-time Systems Using Uppaal . In: Grabowski, J., Nielsen, B. (eds) Formal Approaches to Software Testing. FATES 2004. Lecture Notes in Computer Science, vol 3395. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31848-4_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-31848-4_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25109-5
Online ISBN: 978-3-540-31848-4
eBook Packages: Computer ScienceComputer Science (R0)