From Application Models to Filmstrip Models: An Approach to Automatic Validation of Model Dynamics
Martin Gogolla, Lars Hamann, Frank Hilken, Mirco Kuhlmann · 2014
Abstract: Efficient model validation and verification techniques are strong in the anal-ysis of systems describing static structures, for example, UML class diagrams and OCL invariants. However, general UML and OCL models can involve dynamic as-pects in form of OCL pre- and postconditions for operations. This paper describes the automatic transformation of a UML and OCL model with invariants and pre- and post-conditions into an equivalent model with only invariants. We call the first model (with pre- and 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. Pre- and postconditions from the application model be-come invariants in the filmstrip model. Providing a proper context, the text of the pre-and 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. 1