The Object Constraint Language (OCL) is the established language for the specification of properties of objects and object structures in UML models. One reason that it is not widely adopted in industry is the lack of proper and integrated tool support for OCL. Therefore, we investigate a prototype tool, which analyzes the syntax and semantics of OCL constraints together with some of the UML models and translate them into the language of the theorem prover PVS. In particular, we handle the problematic fact that OCL is based on a three-valued logic, whereas PVS is only based on a two valued logic.
International Workshop on Semantic Foundations of Engineering Design Languages