From Application Models to Filmstrip Models: An Approach to Automatic Validation of Model Dynamics

Abstract

Efficient model validation and verification techniques are strong in the analysis of systems describing static structures, for example, UML class diagrams and OCL invariants. However, general UML and OCL models can involve dynamic aspects in form of OCL preand postconditions for operations. This paper describes the automatic transformation of a UML and OCL model with invariants and preand postconditions into an equivalent model with only invariants. We call the first model (with preand postconditions) the application model and the second model (with invariants only) the filmstrip model, because a sequence of system states in the application model becomes a single system state in the filmstrip model. This single system state can be thought of as being a filmstrip presenting snapshots from the application model with different logical time stamps. Preand postconditions from the application model become invariants in the filmstrip model. Providing a proper context, the text of the preand postconditions can be used in the filmstrip model nearly unchanged. The filmstrip model can be employed for automatically constructing dynamic test scenarios and for checking temporal properties.