MocOCL
Last Updated on Monday, 21 July 2014 12:45 Written by Petra Kaufmann
MocOCL: An OCL-Based CTL Model Checker
In software modeling, the Object Constraint Language (OCL) is an important language to specify properties that a model has to satisfy. The design of OCL reflects the structure of MOF-based modeling languages like the Unified Modeling Language (UML) and its tight integration results in an intuitive usability. But OCL allows to express properties only in the context of a single instance model and not with respect to a sequence of instance models that capture the execution of the system as is possible with temporal logics.
Thus, we show how OCL can be extended with Computation Tree Logic (CTL)-based temporal operators to express properties over the lifetime of an instance model. Our CTL-based OCL extension is twofold. (1) We formally introduce syntax and semantics of our CTL-based OCL language cOCL. (2) The properties specified with cOCL can be verified with our explicit state space model checking framework, called MocOCL.
cOCL
In order to bridge the gap between software models as used in model based development and their representation used for verification, cOCL enriches OCL with standard CTL operators. We formally introduce the syntax and semantics of our cOCL language based on and without modifying the existing definitions of OCL as given by Richters and Gogolla.
Details on the definitions may be found in our paper OCL meets CTL: Towards CTL-Extended OCL Model Checking. For short, we provide a seamless integration of the standard-logic based semantics with OCL semantics and introduce a textual concrete syntax for the following CTL operators, where X, U, G, and F are temporal operators and A and E are path quantifiers:
| CTL operator | Concrete syntax in cOCL |
|---|---|
| X φ | Next φ |
| φ U ψ | φ Until ψ |
| G φ | Globally φ |
| F φ | Eventually φ |
| A τ | Always τ |
| E τ | Exists τ or Sometimes τ |
MocOCL
MocOCL is an explicit state model checker to verify cOCL specifications. It takes an initial model, a set of Transformations, and an cOCL specification as input. In the current realization, we use Ecore to describe the initial model and Henshin graph transformations to implement the system's behavior. We employ Henshin's state space generation facilities to incrementally explore the state space by recursivly applying all matching graph transformation rules. The resulting state space is then analyzed by our extension of the Eclipse OCL plugin. Finally, the resulting example or counterexample trace is visualized in MocOCL's web UI.
Try it online
A demo version of the MocOCL model checker is available online. The demo setting is fixed to a simplified version of a Pacman game based on the following artifacts:
Pacman Game Model
Initial Pacman Game Instance
Move Pacman Transformation
Move Ghost Transformation
Please note that the transformation "Move Ghost" is erroneous on purpose to better illustrate the MocOCL tool.
State Space
After recursively applying the transformations for moving Pacman and the ghost, the following state space is generated and yields the basis for evaluating cOCL expressions. The state highlighted green in the bottom left corner acts as initial state. The red states with dashed border are end states of the system.
Example Specifications
Try out the following example expressions, or specify some on your own.
| cOCL Expression | Natural language description |
|---|---|
| self.fields-> exists(field | field.treasure) | Initially, there is a field containing a treasure. |
| Always Next false / Exists Next true | The game is over / not over. |
| Always Eventually (Always Next false) | The game will surely be over somtimes. |
| Always Globally self.pacman.on.neighbor-> exists(field | field.treasure) implies (Exists Next self.pacman.on.treasure) | As long as not all fields next to Pacman are occupied by ghosts, there is a possibility that the game is not over after the next turn. |
| Always Globally self.pacman.on.neighbor-> exists(field | self.ghosts-> forAll(g | field <> g.on) implies (Exists Next (Exists Next true))) | As long as the game is not over, every ghost may move to at least two different positions. |
| Always Globally (self.pacman.on.treasure) implies (Always Next false) | The game is over after Pacman has found the treasure. |
Download
If you would like to use MocOCL in different verification scenarios, you may install the MocOCL web application on your own machine. Download and deploy the web archive on a machine running Java 7 and Apache Tomcat 7.
The Pacman demo application is shipped with MocOCL by default. However, you may upload and verify your own system description at http://localhost:8080/mococl/testcm.xhtml (depending on your deployment configuration).
For larger verification tasks you may need to configure the timeout after which MocOCL stops evaluating cOCL specifications. The timeout is given as context parameter named "maxevaltime" in the WEB-INF/web.xml file.