Mapping OCL Constraints into CTL-like Logic and SML for UML Validation.

The UML (Unified Modeling Language) graphical models miss providing some pertinent elements of specification as constraints over objects and operations. To fill this lack, OCL (Object Constraint Language) has been developed by IBM and integrated to UML as a modern and formal modeling language, which is easy to learn and efficient to use. On the other hand, many works emerged providing a formal semantics to UML dynamic diagrams by using CP-nets (High-level Petri Nets). The latter are verified based on system properties written in temporal logic. The purpose of this paper is to assist the UML modeler, not necessarily familiar with temporal logics, by letting him expressing the properties in OCL language and proposing an automatic mapping of OCL invariants and pre/post-conditions into CTL-like logic (Computational Tree Logic) coupled with the functional programming language Standard ML. The obtained temporal logic formulas are verified over the state space of the CP-net models derived from UML diagrams by model-checking. UML; OCL; CP-nets; CPN-ML; ASKCTL; CPNtools; Mapping; model-checking. 1.