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

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 provide 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 supported 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 verification of UML/OCL models with irregular values.