Proving Properties of Operation Contracts with Test Scenarios.

This contribution studies structural and behavioral models by applying (a) UML classes, associations, attributes, generalization and OCL invariants for structural model features and (b) UML operations and OCL contracts, i.e., pre- and postconditions, for behavioral features. For detecting and assuring model properties that are not explicitly present, but valid in the considered model suitable test cases are constructed. Inspected model properties are: (a) the consistency between the invariants and the contracts, including the consistency between operation calls by checking whether the postcondition of one operation is compatible with the precondition of a following operation, and (b) the reachability of particular model states defined by invariant-like OCL formulas gained through an operation call chain. Thus, by constructing test cases we prove model consistency and property reachability for behavioral models.