Automatic analysis and test case derivation for a restricted class of LOTOS expressions with data parameters

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