Skip to main content

A Test Generation Framework for quiescent Real-Time Systems

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 3395))

Abstract

We present an extension of Tretmans’ theory and algorithm for test generation for input-output transition systems to real-time systems. Our treatment is based on an operational interpretation of the notion of quiescence in the context of real-time behaviour. This gives rise to a family of implementation relations parameterized by observation durations for quiescence. We define a nondeterministic (parameterized) test generation algorithm that generates test cases that are sound with respect to the corresponding implementation relation. Also, the test generation is exhaustive in the sense that for each non-conforming implementation a test case can be generated that detects the non-conformance.

This is a preview of subscription content, log in via an institution.

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Belinfante, A., Feenstra, J., de Vries, R., Tretmans, J., Goga, N., Feijs, L., Mauw, S., Heerink, L.: Formal test automation: A simple experiment. In: Int. Workshop on Testing of Communicating Systems, vol. 12, pp. 179–196. Kluwer, Dordrecht (1999)

    Chapter  Google Scholar 

  2. 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)

    Chapter  Google Scholar 

  3. Clarke, D., Lee, I.: Automatic test generation for the analysis of a real-time system: Case study. In: IEEE Real Time Technology and Applications Symp., pp. 112–124 (1997)

    Google Scholar 

  4. Dill, D.: Timing assumptions and verification of finite-state concurrent systems. In: Proceedings of the int. workshop on Automatic verification methods for finite state systems, pp. 197–212. Springer, New York (1990)

    Chapter  Google Scholar 

  5. Mandrioli, D., Morasca, S., Morzenti, A.: Generating test cases for real-time systems from logic specifications. TOCS 13(4), 365–398 (1995)

    Article  Google Scholar 

  6. Brinksma, E., Heerink, L., Tretmans, J.: Factorized test generation for multi input/output transition systems. In: Int. Workshop on Testing of Communicating Systems, vol. 11, pp. 67–82. Kluwer, Dordrecht (1998)

    Chapter  Google Scholar 

  7. En-Nouaary, A., Dssouli, R., Khendek, F.: Timed test cases generation based on state characterization technique. In: 19th IEEE Real-Time Systems Symp., pp. 220–229 (1998)

    Google Scholar 

  8. ISO8807. Information processing systems, Open Systems Interconnection, LOTOS, A formal description technique based on the temporal ordering of observational behaviour. Int. Organization for Standardization (1989)

    Google Scholar 

  9. 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)

    Chapter  Google Scholar 

  10. Fernandez, J.-C., Jard, C., Jeron, T., Viho, C.: An experiment in automatic generation of test suites for protocols with verification technology. Sience of Computer Programming - Special Issue on COST247, Verification and Validation Methods for Formal Descriptions 29(1-2), 123–146 (1997)

    Google Scholar 

  11. Springintveld, J., Vaandrager, F., D’Argenio, P.: Testing timed automata. Theoretical Computer Science 254(1-2), 225–257 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  12. Tretmans, J.: Test generation with inputs, outputs and repetitive quiescence. In: Software-Concepts and Tools, 17(3) (1996); Also: Technical Report N0. 96-26, Center for Telematics and Information Technology, University of Twente, The Netherlands, pp. 103–120

    Google Scholar 

  13. Tretmans, J., Brinksma, E.: Torx: Automated model-based testing. In: Hartmann, A., Dussa-Ziegler, K. (eds.) First European Conference on Model-Driven Software Engineering, Nuremberg (2003)

    Google Scholar 

  14. Larsen, K., Mikucionis, M., Nielsen, B.: Real-time system testing on-the-fly. In: Sere, K., Walden, M., Karlsson, A. (eds.) The 15th Nordic Workshop on Programming Theory, NWPT (Extended abstract) (2003)

    Google Scholar 

  15. Brandán-Briones, L., Brinksma, E.: A test generation framework for quiescent real-time systems, http://fmt.cs.utwente.nl/research/testing/files/BBB04.ps.gz

  16. 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)

    Chapter  Google Scholar 

  17. Cardell-Oliver, R.: Conformance test experiments for distributed real-time systems. In: Proceedings of the int. symp. on Software testing and analysis, pp. 159–163. ACM Press, New York (2002)

    Google Scholar 

  18. Cleaveland, R., Lee, I., Lewis, P., Smolka, S.: A theory of testing for soft real-time processes (1996)

    Google Scholar 

  19. de Nicola, R., Hennessy, M.: Testing equivalences for processes. In: Díaz, J. (ed.) ICALP 1983, vol. 154 (1983)

    Google Scholar 

  20. van Glabbeek, R.J.: The linear time-branching time spectrum ii (the semantics of sequential systems with silent moves). In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993)

    Google Scholar 

  21. Langerak, R.: A testing theory for lotos using deadlock detection. In: Proceedings of the IFIP WG 6.1 Ninth int. Symp. on Protocol Spec., Testing, and Verification, IFIP, pp. 87–98 (1990)

    Google Scholar 

  22. Higashino, T., Nakata, A., Taniguchi, K., Cavalli, R.: Generating test cases for a timed i/o automaton model. In: IWTCS 1999, pp. 197–214 (1999)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2005 IFIP International Federation for Information Processing

About this paper

Cite this paper

Briones, L.B., Brinksma, E. (2005). A Test Generation Framework for quiescent Real-Time Systems. 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_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-31848-4_5

  • 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)

Publish with us

Policies and ethics