OCL2MSFOL is a tool that implements a mapping from OCL (Object Constraint Language) to Many-Sorted First-Order Logic. This mapping allows us to reason on UML models with OCL expressions and check satisfaction of them. It translation considers the four-value characteristics of OCL and is significantly more comprehensive than previous work, called OCL2FOL+.
The tool is available online, here
- eHRM: an eHealth Case Study:
We report on our experience applying this methodology on a non-trivial case study: namely, an application for managing medical records. You can download the data model with the invariants here.
- SocialNetwork: Example.
You can download the data model here
- CivilStatus: Example.
This example appears in Initiating a Benchmark for UML and OCL Analysis Tools. TAP 2013. Gogolla et al.
You can download the files to check it, using CVC4.
The examples that appears in Gogolla et al., are described in this paper.
It was accepted at International Symposium Intelligent Systems and Applications (ISA 2016).
- Definitions. The complete mapping are described here