Gesellschaft für Informatik e.V.

Lecture Notes in Informatics

Modellierung 2014 P-225, 273-288 (2014).

Gesellschaft für Informatik, Bonn

Copyright © Gesellschaft für Informatik, Bonn


From application models to filmstrip models: an approach to automatic validation of model dynamics

Martin Gogolla , Lars Hamann , Frank Hilken , Mirco Kuhlmann and Robert France


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.

Full Text: PDF

Gesellschaft für Informatik, Bonn
ISBN 978-388579-619-0

Last changed 14.04.2014 18:06:17