Towards a developer-oriented process for verifying behavioral properties in UML and OCL models

Abstract

Validation and verification of models in the software development design phase have a great potential for general quality improvement within software engineering. A system modeled with UML and OCL can be checked thoroughly before performing further development steps. Verifying not only static but also dynamic aspects of the model will reduce the cost of software development. In this paper, we introduce an approach for automatic behavioral property verification. An initial UML and OCL model will be enriched by frame conditions and then transformed into a (so-called) filmstrip model in which behavioral characteristics can be checked. The final step is to verify a property, which can be added to the filmstrip model in form of an OCL invariant. In order to make the process developer-friendly, UML diagrams can be employed for various purposes, in particular for formulating the verification task and the verification result.