We present the model checker MocOCL, a tool for model checking software models. The design rationale behind MocOCL is to close the gap between formal verification based on model checking and model-based engineering. Our approach avoids conversions that translate the software models into a format that a model checker can process. To this end, we implemented an explicit state model checker that directly processes the software model and verifies them against a specification formulated in a temporal extension of the constraint language OCL. MocOCL offers a web interface that interacts with the Eclipse Modeling Framework.
We present the model checker MocOCL [
The specifications are expressed in cOCL [
The input for our MocOCL tool are hence an Ecore model that represents the static structure of the modeled system, graph transformations that specify its behavior, an instance model conforming to the Ecore model that captures ? This work was partially funded by the Vienna Science and Technology Fund (WWTF) under grant ICT10-018. (Always|Exists) (Next | Globally | Eventually | Until | the system’s initial state, and a specification formulated with cOCL. For the evaluation of such an expression, MocOCL implements an enumerative model checking approach that represents states explicitly. The results of the evaluation are then visualized in an informative user interface. 2
For the tool demonstration, we use a variation of the well–known Pacman game. The game is played with a single Pacman and zero or more ghosts on a game board consisting of several fields, some of which host a treasure. At each turn, either Pacman or a ghost move to an adjacent field. The order of moves is not restricted, i.e., Pacman might move multiple times before a ghost moves. Pacman loses if he gets killed by a ghost, i.e., if both of them share the same field. Pacman wins if he finds a treasure without being killed by a ghost. Figure 1 depicts an initial state of the Pacman game.
Any implementation of this game should fulfill cer- 1 2 tain properties. The rules of the game require, for example, that the game is over if Pacman reaches a treasure. Other properties enforce that Pacman must not get trapped or that Pacman is able to reach a treasure (ini- 3 4 tially). In the following, we will show how these properties are expressed using cOCL and how MocOCL evaluates these cOCL expressions on a certain initial state given as input model to find erroneous behavior. Fig. 1: Initial state 3
In this section we discuss our temporal, CTL-based extension of OCL, called cOCL, and the verification workflow of MocOCL using the running example presented in the previous section.
The cOCL extension. We extend the OCL standard with operators from the branching-time logic CTL. As shown in Fig. 2, '; are either Boolean OCL expressions or cOCL expressions, each of which evaluates to a Boolean value as well. In general CTL formulas are evaluated over sequences of states. In our case, the states correspond to Ecore model instances.
The semantics of these CTL operations are as follows. The path quantifier Always (Exists) requires the following temporal operator to evaluate to true in all (at least one) path(s) starting from the current state. The temporal operators Next, Globally, Eventually, Until, and Unless specify conditions on the path: Next requires to hold in the next state, Globally requires to hold in all states, Eventually requires to hold in at least one state and Until requires to hold eventually and holding before that,
Unless requires to hold forever or before holds. For a more detailed
overview on the cOCL language and property evaluation we kindly refer to [
To verify the system, we need to formulate the system specification in cOCL. For example, to express that the game is over if Pacman is on a treasure we have to specify that in every state of the game if Pacman is on a treasure, there is no next state. This may be expressed in cOCL with Always Globally self.pacman.on.treasure implies (Always Next false) where the context of the expression is, by default, set to the root object of the initial model, that is, the Game class in this case.
The requirement that Pacman does not get trapped is equivalent to Pacman might always change its position provided that the game is not over. Thus, it may be expressed as cOCL property Always (let x = pacman.on in Exists Next x <> pacman.on) Unless (Always Next false).
The requirement that it is possible that Pacman reaches all treasure fields at some point in time is expressed as fields->select(treasure)->forAll(f | Exists Eventually f = pacman.on).
Usage. Once the input is prepared, MocOCL5 loads the Ecore model, the initial model and the set of graph transformations as shown in Fig. 4. The prepared input files are selected via the respective input fields (1), (2), and (3). If necessary, only a subset of the rules defined in the Henshin file can be selected in (6a) and 3 http://www.eclipse.org/modeling/emf/?project=emf 4 https://www.eclipse.org/henshin/ 5 Available for download at http://modelevolution.org/prototypes/ mococl/ with a simplified version for the Pacman example for Google Chrome being usable online at http://modelevolution.org/mococl/ nreoibghhgbioernitdre:a:sFuiereld:1false neniegihgbhobror State 4 to state 7 by movePacman 15 12 2 movePacman on
itdre:a:sFuiereld:3false 11 movePacman 4mnoaveP mcaacm Pevaonm2 4 movePacm1an3 7 ε 14 7 moveGhost
12 itdre:a:sFuiereld:2false 16 on 17
:Pacman :Ghost nreoigbhhbgioern itdre:a:Fsuiereld:4true (6b). Moreover, the user may choose to hide the Ecore model’s root container (4). The tool’s verbose output is useful for understanding verification result (see below), yet, its generation might consume a lot of memory. Thus, the user may opt to restrict the tool’s output to a simple message that reports whether the property is fulfilled or not by deselecting checkbox (5). After the user has entered the cOCL expression into input field (8) and clicked on the Evaluate button (9), all files and the expression are sent to the MocOCL server which evaluates the expression and sends back the result to the Web GUI.
The verification result (9) is displayed next to the Evaluate button together with some performance information. The tree view (10) to the left of the output (9) shows the verification result together with its cause. The cause explains why the expression evaluated to either true or false. The cause of a CTL expression consists of the states leading to the result. If a counter example trace is generated, the cause consists of the last state of the trace. The cause of a state consists of the expressions evaluated in the state and predecessor and successor states. Note that due to the iterative state space exploration strategy, some states not relevant for the result are omitted. The state space is represented in two different views displayed in the right part of Fig. 4. The first view, the partial state space view (11), shows all states occurring in the evaluation tree together with all known transitions among these states. In the second view, the trace view (12), the states of the evaluation tree are visualized as a trace leading from the initial to the final states.
Initial states, i.e., states without incoming transitions, are highlighted in green. Final states, i.e., states without outgoing transitions, are highlighted in orange. Transitions between two states that result from evaluating a sub– expression are displayed semi-transparent and are connected to its immediate parent–level expression using –transitions to differentiate between relevant parts of the parent- and its sub–expressions. If the size of the displayed state space together with all sub–expression transitions grows too large, these transitions can be hidden by changing the setting (7) from Connected to none.
Upon selecting a state or transition in the state space or trace view, the state or transition is highlighted (13) and its model instance is displayed in the state– visualization area (15). There, those parts of the model instance that occur in sub–expressions are highlighted in purple (16). Associations in red (green) indicate that these associations are deleted (added) (17) when transitioning from the source to the target state.
The result of the verification can be interpreted as follows. Recall that we wanted to ensure that the game is over if Pacman has found the treasure. The highlighted transition indicates that Pacman has really found the treasure, but the ghost is still able to move. In fact, our moveGhost transition only forbids the ghost from moving if he has killed Pacman, but not if Pacman has won the game. 4
Several model checkers for graph-based languages have been proposed in the
literature. CheckVML verifies systems defined by UML-like class diagrams
whose behavior is captured by a set of graph transformations against safety
properties provided as property graphs [
The SOCLe tool verifies systems that are specified by a class diagram and
a set of state machines, which describe the behavior of each class, against an
EOCL specification [
Similar to Groove, where the system’s model and its specification are described with attributed graphs, MocOCL allows its users to express the verification problem at the level of the models that capture structure and behavior of a system. This and the fact that cOCL extends OCL, which is presumably well-known to modelers, lead to our conjecture that MocOCL bridges the gap between model checking and model-based engineering. The validation of this conjecture is subject to a future user study. In contrast to more mature tools the performance of MocOCL requires improvements. For example, MocOCL asserts that Pacman can win the game on a board with 32 fields and 2 ghosts after 33,65 seconds while Groove requires only 21,65 seconds on a i5-2410M machine with 2.3 GHz and 8 GB ram.
In future work we plan to switch to an incremental evaluation algorithm for cOCL specifications and remove expensive isomorphism checks currently necessary during the exploration of the state space. Further, the integration of MocOCL into Eclipse and an improved user interface are work in progress.