Advertisement

Testing Protocol Robustness

  • Antoine Rollet
  • Hacène Fouchal
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2877)

Abstract

Some new protocols as multimedia or wireless protocols are constrained and sometimes critical. We need to ensure their correct functioning before their development. They handle time constraints to model important aspects (delays, timeouts). This issue should be considered in specification language used to model such protocols. This paper presents a methodology for the development of reliable timed systems in general. It might be used to develop complex protocols.

We use the RT-LOTOS language as a high level model and we use the timed automata model as a low level model. This later is the basis of our validation technique. We collect all possible errors on such systems and show how to integrate them in some automated derived test sequences in order to observe the system reactions when it executes faulty behavior. Our aim is to observe the robustness of the whole system in presence of simulated errors.

Keywords

Robustness Testing Validation Protocol Testing Timed Automata Automata Theory 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [ACH94]
    Alur, R., Courcoubetis, C., Henzinger, T.A.: The observational power of clocks. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 162–177. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  2. [AD94]
    Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  3. [BB89]
    Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. In: van Eijk, P.H.L., Vissers, C.A., Diaz, M. (eds.) The formal description technique LOTOS, pp. 23–73. Elsevier Science Publishers, Amsterdam (1989)Google Scholar
  4. [BDS95]
    Bryans, J., Davies, J., Schneider, S.: Real-time CSP and ET-LOTOS. Technical report, Dept. of Computer Science, University of Reading (1995)Google Scholar
  5. [BL92]
    Bolognesi, T., Lucidi, F.: Timed process algebras with urgent interactions and a unique powerful binary operator. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 124–148. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  6. [BLL+98]
    Bengtsson, J., Larsen, K.G., Larsen, F., Petterson, P., Yi, W., Weise, C.: New Generation of UPPAAL. In: Proceedings of the International Workshop on SOftware Tools and Technology Transfer (Aalborg, Denmark, July 12-13) (July 1998)Google Scholar
  7. [CL97]
    Clarke, D., Lee, I.: Automatic generation of tests for timing constraints from requirements. In: Proceedings of the Third International Workshop on Object-Oriented Real-Time Dependable Systems, Newport Beach, California (February 1997)Google Scholar
  8. [CO95]
    Courtiat, J.-P., De Oliveira, R.C.: On rt-lotos and its application to the formal design of multimedia protocols. Annals of Telecommunications 50(11-12), 888–906 (1995)Google Scholar
  9. [COG98]
    Cardel-Oliver, R., Glover, T.: A practical and complete algorithm for testing real-time systems. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 251–261. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  10. [DNH84]
    De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theoretical Computer Science 34, 83–133 (1984)zbMATHCrossRefMathSciNetGoogle Scholar
  11. [DOTY95]
    Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool Kronos. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, Springer, Heidelberg (1996)CrossRefGoogle Scholar
  12. [DOY94]
    Daws, C., Olivero, A., Yovine, S.: Verifying ET-LOTOS programs with kronos. In: Hogrefe, D., Leue, S. (eds.) Proceedings of the 7th International Conference on Formal Description Techniques, FORTE 1994, pp. 207–222. North-Holland, Amsterdam (1994)Google Scholar
  13. [DY95]
    Daws, C., Yovine, S.: Two examples of verification of multirate timed automata with kronos. In: Proceedings of the 1995 IEEE Real-Time Systems Symposium, RTSS 1995, Pisa, Italy, IEEE Computer Society Press, Los Alamitos (1995)Google Scholar
  14. [ENDKE98]
    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), Madrid, Spain (1998)Google Scholar
  15. [FBK+91]
    Fujiwara, S., Bochmann, G., Khendek, F., Amalou, M., Ghedamsi, A.: Test selection based on finite-state models. IEEE Transactions on Software Engineering 17(6), 591–603 (1991)CrossRefGoogle Scholar
  16. [HNTC01]
    Hogashino, T., Nakata, A., Taniguchi, K., Cavalli, A.R.: Generating Test Cases for a Timed I/O Automaton Model (October 2001)Google Scholar
  17. [ISO87]
    ISO. Information processing systems – open systems interconnection – LOTOS – a formal description technique based on the temporal ordering of observational behaviour ISO/TC97/SC21/N DIS8807 (1987) Google Scholar
  18. [ISO97]
    ISO. Working draft on enhancements to lotos. Technical Report ISO/IEC JTC1/SC21, International Organization for Standardization —WG7, Genève (January 1997) Google Scholar
  19. [Kar92]
    Karjoth, G.: Generating Transition Graphs from LOTOS Specifications. In: Diaz, M., Groz, R. (eds.) Proceedings of the 5th International Conference on Formal Description Techniques FORTE 1992 (Perros-Guirec, France), November 1992, North-Holland, Amsterdam (1992)Google Scholar
  20. [Kon95]
    Koné, O.: Designing test for time dependant systems. In: Proceedings of the 13th IFIP International Conference on Computer Communication Séoul, South Korea (1995)Google Scholar
  21. [LC97]
    Laurencot, P., Castanet, R.: Integration of Time in Canonical Testers for Real-Time Systems. In: International Workshop on Object- Oriented Real-Time Dependable Systems, California, IEEE Computer Society Press, Los Alamitos (1997)Google Scholar
  22. [Led92]
    Leduc, G.: An upward compatible timed extension to LOTOS. In: Parker, K., Rose, G. (eds.) Proceedings of the 4th International Conference on Formal Description Techniques, FORTE 1991, North-Holland, Amsterdam (1992)Google Scholar
  23. [LL93]
    Leduc, G., Léonard, L.: A timed LOTOS supporting a dense time domain and including new timed operators. In: Proceedings of the 5th International Conference on Formal Description Techniques, FORTE 1992, North-Holland, Amsterdam (1993)Google Scholar
  24. [NS01]
    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)CrossRefGoogle Scholar
  25. [PF99]
    Petitjean, E., Fouchal, H.: From Timed Automata to Testable Untimeed Automata. In: 24th IFAC/IFIP International Workshop on Real- Time Programming, Schloss Dagstuhl, Germany (1999)Google Scholar
  26. [RNHW98]
    Raymond, P., Nicollin, X., Halbwatchs, N., Waber, D.: Automatic testing of reactive systems, madrid, spain. In: Proceedings of the 1998 IEEE Real-Time Systems Symposium, RTSS 1998, December 1998, pp. 200–209. IEEE Computer Society Press, Los Alamitos (1998)Google Scholar
  27. [SVD01]
    Springintveld, J., Vaandrager, F.W., D’Argenio, P.R.: Timed Testing Automata. Theoretical Computer Science 254(254), 225–257 (2001)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Antoine Rollet
    • 1
  • Hacène Fouchal
    • 1
  1. 1.Département de Mathématiques et InformatiqueUniversité de Reims Champagne-ArdenneReims CedexFrance

Personalised recommendations