More than true or false: Native Support of Irregular Values in the Automatic Validation & Verification of UML/OCL Models

Nils Przigoda, Philipp Niemann, Judith Peters, Frank Hilken, Robert Wille, Rolf Drechsler

In: 15th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE). ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE-15) September 29-October 2 Wien Austria 2017.


UML/OCL models are used to describe system models in early stages of the design process. In order to detect design flaws in these models as soon as possible (ideally before the implementation phase starts), various methods for the validation and verification of UML/OCL models have been proposed. In particular, automatic solutions (so-called model finders) are of interest here. They pro- vide designers with quick feedback, e. g., on the consistency of their models in a push-button fashion. But thus far, all proposed approaches support a (small) subset of UML/OCL only or employ substantial restrictions. In fact, there are only few solutions that support the extended type system including the irregular values null and invalid – although these values play an important role for covering exceptional cases. Moreover, these solutions either heavily rely on manual interaction or significantly restrict the sup- ported UML/OCL description means. In this work, we propose a generic formal representation of UML/OCL which can be used for the validation and verification of corresponding models and, at the same time, addresses these shortcomings. The resulting representation can be used by various reasoning engines and, hence, eventually allows for the validation and verifi- cation of UML/OCL models with irregular values.


German Research Center for Artificial Intelligence
Deutsches Forschungszentrum für Künstliche Intelligenz