Test Plan Generation for Concurrent Real-Time Systems Based on Zone Coverage Analysis

Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5047)


The state space explosion due to concurrency and timing constraints of concurrent real-time systems (CRTS) presents significant challenges to the verification engineers. In this paper, we investigate how to use coverage techniques to generate efficient test plans for such systems. We first discuss how to use communicating timed automata to model CRTS. We present a new coverage technique, AZC (active zone coverage), based on the zone equivalence relation between states of CRTS. We discuss techniques to estimate AZC values of active zones represented in BDD-like diagrams. We explain how to construct zone trees and map their root-to-leaf paths to test cases. We then present an algorithm to generate test plans by prioritizing the test cases. The test plans that we generate can efficiently achieve full coverage in AZC. We have implemented our ideas with our TCTL model-checker RED. Experiment report with the Bluetooth L2CAP showed improvement of the coverage growth rate in the test plan execution.


Test Plan Global Transition System Under Test Test Case Generation State Space Explosion 
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.


  1. 1.
    Alur, R., Courcoubetis, C., Dill, D.L.: Model Checking for Real-Time Systems. In: IEEE LICS (1990)Google Scholar
  2. 2.
    Bening, L., Foster, H.: Principles of Verifiable RTL Design: a Functional Coding Style Supporting Verification Processes in Verilog, 2nd edn. Kluwer Academic Publishers, Dordrecht (2001)zbMATHGoogle Scholar
  3. 3.
    Behrmann, G., Fehnker, A., Hune, T.S., Larsen, K.G., Pettersson, P., Romijn, J.: Efficient Guiding Towards Cost-Optimality in UPPAAL. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, Springer, Heidelberg (2001)CrossRefGoogle Scholar
  4. 4.
    Bochmann, G.V., Petrenko, A.: Protocol Testing: Review of Methods and Relevance for Software Testing. In: Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis (1994)Google Scholar
  5. 5.
    Clarke, E., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons using Branching-Time Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, Springer, Heidelberg (1982)CrossRefGoogle Scholar
  6. 6.
    Cheng, K.-T., Krishnakumar, A.S.: Automatic Functional Test Generation Using the Extended Finite State Machine Model. In: Proceedings of the 30th Design Automation Conference, June 1993, pp. 86–91 (1993)Google Scholar
  7. 7.
    En-Nouaary, A., Dssouli, R., Khendek, F.: Timed Wp: Testing Real-time Systems. In: IEEE Transactions on Software Engineering, vol. 29(11), IEEE Computer Society, Los Alamitos (2002)Google Scholar
  8. 8.
    Elbaum, S., Malishevsky, A.G., Rothermel, G.: Test Case Prioritization: A Family of Empirical Studies. IEEE Transactions on Software Engineering archive 28(2) (2002)Google Scholar
  9. 9.
    ETSI: Methods for Testing and Specification (MTS) The Testing and Test Control Notation version 3. ETSI ES 201873, parts 1 to 7, v3.1.1, (2005-06)Google Scholar
  10. 10.
    Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman, New York (1983)zbMATHGoogle Scholar
  11. 11.
    Haartsen, J.: Bluetooth Specification, version 1.0.
  12. 12.
    Hessel, A., Larsen, K.G., 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, Springer, Heidelberg (2004)CrossRefGoogle Scholar
  13. 13.
    Ho, P.-H., Wong-Toi, H.: Automated Analysis of an Audio Control Protocol. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, Springer, Heidelberg (1995)CrossRefGoogle Scholar
  14. 14.
    Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic Model Checking for Real-Time Systems. In: IEEE LICS 1992 (1992)Google Scholar
  15. 15.
    Hoskote, Y., Moundanos, D., Abraham, J.A.: Automatic Extraction of the Control Flow Machine and Application to Evaluating Coverage of Verification Vectors. In: Proceedings of the Int’l Conference on Computer Design, October 1995, pp. 532–537 (1995)Google Scholar
  16. 16.
    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, Springer, Heidelberg (2005)CrossRefGoogle Scholar
  17. 17.
    Krichen, M., Tripakis, S.: Black-box Conformance Testing for Real-Time Systems. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, Springer, Heidelberg (2004)CrossRefGoogle Scholar
  18. 18.
    Larsen, K.G., Pettersson, P., Yi, W.: Diagnostic Model-Checking for Real-Time Systems. In: Proceedings of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, New Brunswick, New Jersey, October 22-24 (1995)Google Scholar
  19. 19.
    Lee, D., Yannakakis, M.: Principles and Methods of Testing Finite State Machines - A Survey. Proceedings of The IEEE 84(8), 1090–1123 (1996)CrossRefGoogle Scholar
  20. 20.
    Nielsen, B., Skou, A.: Automated Test Generation from Timed Automata. International Journal on Software Tools for Technology Transfer (STTT) 4 (2002)Google Scholar
  21. 21.
    Pettersson, P., Larsen, K.G.: UPPAAL2k. Bulletin of the European Association for Theoretical Computer Science 70, 40–44 (2000)Google Scholar
  22. 22.
    Rashinkar, P., Paterson, P., Singh, L.: System-on-a-chip Verificatoin, Methodology and Techniques. Kluwer Academic Publishers, Dordrecht (2001)zbMATHGoogle Scholar
  23. 23.
    Shaw, A.: Communicating Real-time State Machines. IEEE Transactions on Software Engineering 18(9) (September 1992)Google Scholar
  24. 24.
    Srivastava, A., Thiagarajan, J.: Effectively prioritizing tests in development environment. In: Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis (2002)Google Scholar
  25. 25.
    Springintveld, J., Vaandrager, F., D’Argenio, P.R.: Testing Timed Automata. Theoretical Computer Science 254(1-2) (2001)Google Scholar
  26. 26.
    Wang, F.: Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram. In: Proceedings of FORTE, Cheju Island, Korea (August 2001)Google Scholar
  27. 27.
    Wang, F.: Efficient Verification of Timed Automata with BDD-like Data-Structures. STTT (Software Tools for Technology Transfer) 6(1) (June 2004); special issue for the 4th VMCAI, LNCS. vol. 2575. Springer, Heildelberg (January 2003) Google Scholar
  28. 28.
    Wang, F.: Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-like Data-Structures. In: IEEE Transactions on Software Engineering, vol. 31(1), pp. 38–51. IEEE Computer Society, Los Alamitos (2005); A preliminary version is in proceedings of 16th CAV, LNCS vol. 3114. Springer, Heildelberg (2004) Google Scholar
  29. 29.
    Weyuker, E.J.: In Defense of Coverage Criteria. In: Proceedings of the 11th ACM/IEEE International Conf. on Software Engineering (ICSE), Pittsburgh, Pa (May 1989)Google Scholar
  30. 30.
    Weyuker, E.J.: How to Judge Testing Progress. Journal of Information and Software Technology 45(5), 323–328 (2004)CrossRefGoogle Scholar
  31. 31.
    Wang, F., Huang, G.-D., Yu, F.: Symbolic Simulation of Real-Time Concurrent Systems. In: Chen, J., Hong, S. (eds.) RTCSA 2003. LNCS, vol. 2968, Springer, Heidelberg (2004)Google Scholar
  32. 32.
    Wang, F., Huang, G.-D., Yu, F.: Numerical Coverage Estimation for Dense-Time Systems. In: König, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol. 2767, Springer, Heidelberg (2003)CrossRefGoogle Scholar
  33. 33.
    Wong-Toi, H.: Symbolic Approximations for Verifying Real-Time Systems. Ph.D. dissertation, Stanford Univ., Stanford, CA (1995)Google Scholar
  34. 34.
    Yovine, S.: Kronos: A Verification Tool for Real-Time Systems. International Journal of Software Tools for Technology Transfer 1(1/2) (October 1997)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2008

Authors and Affiliations

  1. 1.Dept. of Electrical EngineeringNational Taiwan UniversityTaiwan, ROC
  2. 2.Grad. Inst. of Electronic EngineeringNational Taiwan UniversityTaiwan, ROC

Personalised recommendations