
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
T. Higashino, G.v. Bochmann, "Automatic Analysis and Test Case Derivation for a Restricted Class of LOTOS Expressions with Data Parameters," IEEE Transactions on Software Engineering, vol. 20, no. 1, pp. 2942, January, 1994.  
BibTex  x  
@article{ 10.1109/32.263753, author = {T. Higashino and G.v. Bochmann}, title = {Automatic Analysis and Test Case Derivation for a Restricted Class of LOTOS Expressions with Data Parameters}, journal ={IEEE Transactions on Software Engineering}, volume = {20}, number = {1}, issn = {00985589}, year = {1994}, pages = {2942}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.263753}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Automatic Analysis and Test Case Derivation for a Restricted Class of LOTOS Expressions with Data Parameters IS  1 SN  00985589 SP29 EP42 EPD  2942 A1  T. Higashino, A1  G.v. Bochmann, PY  1994 KW  specification languages; formal specification; linear programming; integer programming; concurrency control; test case derivation; LOTOS expressions; data parameters; automatic analysis method; data values; PLOTOS expressions; data types; Presburger arithmetic; integer; Boolean types; addition; subtraction; comparison; decision procedure; integer linear programming problems; deadlock detection problem; nonexecutable branch detection; nondeterministic behavior detection; test selection; simplified Session protocol; specification language VL  20 JA  IEEE Transactions on Software Engineering ER   
We propose an automatic analysis and test case derivation method for LOTOS expressions with data values. We introduce the class of PLOTOS expressions where the data types are restricted to Presburger arithmetic. That is, only the integer and Boolean types are used, and the operators of the integers are restricted to addition, subtraction, and comparison. For this class, we give an algorithm for deriving a set of test cases (a test suite). The algorithm is carried out by using a decision procedure for integer linear programming problems. We also give solutions for the deadlock detection problem, the detection of nonexecutable branches, and the detection of nondeterministic behaviors. We have implemented a tool for the analysis and test selection based on our techniques. The derivation of a test suite for a simplified Session protocol is described as an example.
[1] G. v. Bochmann, "Protocol specification for OSI,"Computer Networks ISDN Syst., vol. 18, pp. 167184, 1989/1990.
[2] T. Bolognesi and E. Brinksma, "Introduction to the ISO Specification language LOTOS,"Computer Networks ISDN Syst., vol. 14, pp. 25 59, 1987.
[3] E. Brinksma, "A theory for the derivation of tests,"Proc. 8th Int. Conf. Protocol Specification, Testing and Verification, NorthHolland, 1988, pp. 6374.
[4] E. Brinksma, R. Alderden, R. Langerak, J. v. d. Lagemaat, and J. Tretmans, "Formal approach to conformance testing,"Proc. Int. Workshop on Protocol Test Systems (IWPTS'89), NorthHolland, 1989, pp. 311325.
[5] CCITT, "SDL: Specification and description language," Recommendation Z.100, Nov. 1988.
[6] H. Eertink and D. Wolz, "Symbolic execution of LOTOS specifications,"Proc. 5th Int. Conf. on Formal Description Techniques (FORTE'92), NorthHolland, 1992, pp. 295310.
[7] P. H. J. v. Eijk, C. A. Vissers, and M. Diaz, Eds.,The Formal Description Technique LOTOS. NorthHolland, 1989, p. 451.
[8] A. Fantechi, S. Gnesi, and G. Mazzarini, "How much expressive are LOTOS behavior expressions?,"Proc. 3rd Int. Conf. on Formal Description Techniques (FORTE'90), NorthHolland, 1990, pp. 1732.
[9] S. Fujiwara, G. v. Bochmann, F. Khendek, M. Amalou, and A. Ghedamsi, "Test selection based on finite state models,"IEEE Trans. Soft. Eng., vol. 17, pp. 591603, June 1991.
[10] S. Fujiwara and G. von Bochmann, "Testing nondeterministic state machincs with fault coverage,"Proc. 4th Int. Workshop on Protocol Test Systems (IWPTS'92), NorthHolland, 1991, pp. 267280.
[11] R. Guillemot and L. Logrippo, "Derivation of useful execution trees from LOTOS specification by using an interpreter," inProc. FORTE'88, Stirling, U.K., Sept. 1988.
[12] D. Gueraichi, and L. Logrippo, "Derivation of test cases for LAPB from LOTOS specification," inProc. FORTE'89, Vancouver, B.C., Canada, Dec. 1989.
[13] T. Higashino, G. v. Bochmann, X. Li, K. Yasumoto, and K. Taniguchi, "Test system for a restricted class of LOTOS Expressions with data parameters,"Proc. 5th Int. Workshop on Protocol Test Systems (IWPTS'92). NorthHolland, 1992, pp. 205216.
[14] T. Higashino, K. Ninomiya, T. Kimoto, K. Taniguchi, and M. Mori, "Automated verification of equivalence of protocol machines,"Proc. 9th Int. Conf. Protocol Specification, Testing and Verification (PSTVIX)NorthHolland, 1989, pp. 235246.
[15] J.E. Hopcroft and J.D. Ullman,Introduction to Automata Theory, Languages, and Computation, AddisonWesley, Reading, Mass., 1979.
[16] ISO, "Information processing systemOpen systems interconnectionBasic connection oriented Session protocol specification," IS 8327, Aug. 1987.
[17] ISO, "Information processing system, open systems interconnection, LOTOSA formal description technique based on the temporal ordering of observational behavior," IS 8807, Jan. 1989.
[18] ISO, "Estelle: A formal description technique based on an extended state transition model," ISO 9074, July 1989.
[19] J. W. Klop, "Term rewriting systems: A tutorial,"Bull EATCS, vol. 32, pp. 143183, 1987.
[20] R. Langerak, "A testing theory for LOTOS using deadlock detection,"Proc. 9th Int. Conf. Protocol Specification, Testing and Verification (PSTVIX), pp. 8798, NorthHolland, June 1989.
[21] T. Matsuura, T. Nakamura, T. Higashino, K. Taniguchi, and S. Masuda, "VTM: A graph editor for large trees,"Proc. 12th IFIP World Computer Congress'92, vol. I. NorthHolland, 1992, pp. 210216.
[22] D. C. Oppen, "A 222pnupper bound on the complexity of Presburger arithmetic,"J. Comput. Syst. Sci., vol. 16, pp. 322332, 1978.
[23] M. Presburger, "Uber die vollstandigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchen die addition als einzige operation hervortritt," inComptesRendus du ler Congres des Mathematiciens des Pays Slavs, 1929.
[24] B. Sarikayaet al., "A test design methodology for protocol testing,"IEEE Trans. Software Eng., vol. SE13, no. 5, pp. 518531, May 1987.
[25] P. Tripath and B. Sarikaya, "Test generation from protocol specification," inProc. 2nd Int. Conf. Formal Description Techniques for Distributed Syst. Commun. Protocols, Vancouver, B.C., Canada, Dec. 1989, pp. 455468.
[26] J. Tretmans, "Test case derivation from LOTOS specification," inProc. FORTE'89, Vancouver, B.C., Canada, Dec. 1989.
[27] C. D. Wezeman, "The COOP method for compositional derivation of conformance testers," inProc. 9th IFIP Symp. Protocols, Twente, June 1989.