1 Introduction

Automated test data generation is an important method for the verification and validation of UML/OCL specifications. Instead of verifying concrete code via a Hoare-Calculus for a specific programming language against OCL method contracts — a technique developed in detail for OCL in

Brucker, A.D., Wolff, B.: An extensible encoding of object-oriented data models in HOL. Journal of Automated Reasoning 41, 219–249 (2008).

Brucker, A.D., Wolff, B.: Semantics, calculi, and analysis for object-oriented specifications. Acta Informatica 46(4), 255–284 (2009).

test generation can be a more light-weighted (but logically less safe) formal method to reveal errors both in specification and implementations

In this paper, we will adapt existing specification-based testing techniques to UML/OCL, i. e., an object-oriented specification formalism centered around the concept of an object-graph as state, state-transitions described by class-models and state-charts (which we will ignore here), and a type system based on subtyping and inheritance.

In this paper, we will adapt existing specification-based testing techniques to UML/OCL, and a type system based on subtyping and inheritance.

The work presented here is based on the previous work on a formal UML/OCL semantics [7, 11]

Brucker, A.D., Krieger, M.P., Wolff, B.: Extending OCL with null-references. In: Gosh, S. (ed.) Models in Software Engineering, no. 6002 in LNCS, pp. 261–275. Springer (2009).

Brucker, A.D., Wolff, B.: Semantics, calculi, and analysis for object-oriented specifications. Acta Informatica 46(4), 255–284 (2009).

and attempts to develop, in contrast to prior works such as,

Benattou, M., Bruel, J., & Hameurlain, N. (2002). Generating test data from OCL specification. URL http://www.imamu.edu.sa/DContent/IT_Topics/Generating\%20Test\%20Data\%20from\%20OCL\%20Specication.pdf

a comprehensive test-generation method for the complete language and for realistic test-scenarios.

Contribution:

1. the extension of specification-based test generation methods to the world of object-oriented specifications,
2. a deductive, theorem-prover based test data generation from OCL specifications including language features such as recursive query-operations, and
3. a particular representation of object-graph classes by our novel concept of an alias closure; rather than representing the explicit object graphs we represent the object identity by an equivalence relation.

2 A Gentle Introduction to a Formal OCL 2.2 Semantics

Pragmatically, HOL can be viewed as a typed functional programming language like Haskell extended by logical quantifiers.

3 Running Example: Linked Lists

4 Test Generation

5 Integrating the Technique in HOL-TestGen

6 Related and Future Work