An ASM Definition of the Dynamic OCL 2.0 Semantics

The recently adopted OCL 2.0 specification comes with a formal semantics that is based on set theory with a notion of an object model and system states. System states keep the runtime information relevant for the evaluation of OCL expressions. However, not all new language concepts of OCL 2.0 are already addressed in that formal semantics. We show how to overcome this by introducing new components to the object model and system states defining a dynamic semantics of OCL. In order to give precise rules that determine when the current system state has to be updated according to a change in the referred UML model, we make use of adequate mathematical means, namely Abstract State Machines (ASMs). Though our ASM specification also gives a clear definition for the evaluation of OCL constraints, it leaves sufficient flexibility for application specific implementations that have to determine when constraints are to be checked.