Automatic Analysis and Test Case Derivation for a Restricted Class of LOTOS Expressions with Data Parameters
Issue No. 01 - January (1994 vol. 20)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.263753
<p>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.</p>
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
G. Bochmann and T. Higashino, "Automatic Analysis and Test Case Derivation for a Restricted Class of LOTOS Expressions with Data Parameters," in IEEE Transactions on Software Engineering, vol. 20, no. , pp. 29-42, 1994.