Proving and Visualizing OCL Invariant Independence by Automatically Generated Test Cases

摘要

Within model-driven development, class invariants play a central role. An essential property of a collection of invariants is the independence of each single invariant, i.e., the invariant at hand cannot be deduced from the other invariants. The paper explains with three example models the details of an approach for automatically proving and representing invariant independence on the basis of a script constructing large test cases for the underlying model. Analysis of invariant independence is visualized by means of several diagrams like a 'test configuration and result' diagram, an 'invariant dependence detail' diagram, and an 'invariant dependence overview' diagram. The paper also discusses how to build the test case construction script in a systematic way. The test case construction script is written by the model developer, but a general construction frame for the script is outlined.