This Article 
 Bibliographic References 
 Add to: 
Automatic Analysis and Test Case Derivation for a Restricted Class of LOTOS Expressions with Data Parameters
January 1994 (vol. 20 no. 1)
pp. 29-42

We propose an automatic analysis and test case derivation method for LOTOS expressions with data values. We introduce the class of P-LOTOS 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. 167-184, 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, North-Holland, 1988, pp. 63-74.
[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), North-Holland, 1989, pp. 311-325.
[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), North-Holland, 1992, pp. 295-310.
[7] P. H. J. v. Eijk, C. A. Vissers, and M. Diaz, Eds.,The Formal Description Technique LOTOS. North-Holland, 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), North-Holland, 1990, pp. 17-32.
[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. 591-603, June 1991.
[10] S. Fujiwara and G. von Bochmann, "Testing non-deterministic state machincs with fault coverage,"Proc. 4th Int. Workshop on Protocol Test Systems (IWPTS'92), North-Holland, 1991, pp. 267-280.
[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 LAP-B 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). North-Holland, 1992, pp. 205-216.
[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 (PSTV-IX)North-Holland, 1989, pp. 235-246.
[15] J.E. Hopcroft and J.D. Ullman,Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, Reading, Mass., 1979.
[16] ISO, "Information processing system--Open systems interconnection--Basic connection oriented Session protocol specification," IS 8327, Aug. 1987.
[17] ISO, "Information processing system, open systems interconnection, LOTOS--A 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. 143-183, 1987.
[20] R. Langerak, "A testing theory for LOTOS using deadlock detection,"Proc. 9th Int. Conf. Protocol Specification, Testing and Verification (PSTV-IX), pp. 87-98, North-Holland, 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. North-Holland, 1992, pp. 210-216.
[22] D. C. Oppen, "A 222pnupper bound on the complexity of Presburger arithmetic,"J. Comput. Syst. Sci., vol. 16, pp. 322-332, 1978.
[23] M. Presburger, "Uber die vollstandigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchen die addition als einzige operation hervortritt," inComptes-Rendus 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. SE-13, no. 5, pp. 518-531, 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. 455-468.
[26] J. Tretmans, "Test case derivation from LOTOS specification," inProc. FORTE'89, Vancouver, B.C., Canada, Dec. 1989.
[27] C. D. Wezeman, "The CO-OP method for compositional derivation of conformance testers," inProc. 9th IFIP Symp. Protocols, Twente, June 1989.

Index Terms:
specification languages; formal specification; linear programming; integer programming; concurrency control; test case derivation; LOTOS expressions; data parameters; automatic analysis method; data values; P-LOTOS 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
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. 29-42, Jan. 1994, doi:10.1109/32.263753
Usage of this product signifies your acceptance of the Terms of Use.