OCL meets CTL: Towards CTL-Extended OCL Model Checking?

Abstract

In software modeling, the Object Constraint Language (OCL) is an important tool to specify properties that a model has to satisfy. The design of OCL reflects the structure of MOF-based modeling languages like UML and the tight integration results in an intuitive usability. However, OCL allows to express properties in the context of the current state of an instance model only but not with respect to its evolution. In this paper, we show how OCL can be extended with CTL-based temporal operators to express properties over the lifetime of an instance model. We explain syntax and semantics of our OCL extension and provide a prototypical implementation of our MocOCL model checker.

Introduction

In software and hardware verification, model checking [ 3 ] is currently one of the most widely used verification techniques to show that a system satisfies its specification.3 Model checking requires a formal representation of the system and a specification that is often expressed in terms of a temporal logic formula. Common choices are the computation tree logic (CTL) and the linear temporal logic (LTL) that are used to express constraints over the lifetime of the system.

In the context of model-based engineering (MBE), software models are the core artifacts to specify and develop a system. Obviously, the correctness of the models is a prerequisite for the correctness of the system that is presented to the end user [ 19 ]. Consequently, formal verification techniques find their way into the MBE processes to help detect and avoid errors in the models. Due to its fully automatic verification capabilities, model checking has been shown to be of particular importance. Recent works and tools, for example, Hugo [ 14 ], Groove [ 13 ], and Proco [ 11 ] to name but a few, show that various kinds of software models can be suitably verified with model checking. ? This work was partially funded by the Vienna Science and Technology Fund (WWTF) under grant ICT10-018. 3 Usually, a specification consists of a set of properties that should hold in a system.

We will, however, often use these terms interchangeably.

Many approaches, however, require the modeler to express the properties of a specification in the language of the target model checker. In our opinion this is a drawback as (1) the modeler needs to leave her usual working environment and (2) the properties are not expressed on the modeling layer. Typically, a modeling environment provides some language to express constraints that a model has to satisfy. For example, the Object Constraint Language (OCL) [ 10 ] is a widely adopted language to express invariants, and pre- and postconditions over a model. But OCL only considers a single snapshot of the model, not its evolution during the execution of the system.

In this paper we thus present a CTL-based temporal extension to OCL and, in addition, provide a working implementation of a model checker to verify CTLextended OCL constraints. Hence, our contribution is twofold. First, we extend syntax and semantics of OCL with CTL operators. Second, we integrate the syntactical extension into the Eclipse OCL Workbench and implement a model checker to evaluate CTL-extended OCL constraints in Eclipse. In the following, we assume that the static structure of the system is represented by an Ecore model and the system’s behavior is described by a set of model transformations. The specification is expressed as a CTL-extended OCL constraint.

The structure of this paper is as follows. In Section 2 we present the syntax and semantics of our CTL-based OCL extension. Then, in Section 3, we discuss the overall idea by means of a motivating example and describe the implementation of our verification framework. Finally, after showcasing a first case study (Section 4), we close the paper with an overview of related approaches (Section 5), and conclude in Section 6 with a critical discussion and an outlook on future work. Due to space limitations we assume familiarity with model checking and CTL and kindly refer to standard literature [ 3 ] for an introduction. 2

A Temporal Extension of OCL

In the following, we formally introduce the syntax and semantics of OCL enriched with standard CTL operators. We integrate our extension, named cOCL, into the formal semantics of OCL [ 10,18 ] without modifying the existing definitions. Due to space limitations we do not reproduce the existing definitions here and kindly refer to the work of Richters et al. [ 18 ] for the details on the syntax and semantics of OCL.

Definition 1 (Syntax). The expressions of cOCL are defined as follows: 1. Each OCL expression of Definition 1 in [ 18 ] is in cOCL; 2. if φ, ψ ∈ Expr Bool then AXφ, EXφ, AφWψ, EφWψ, AφUψ, EφUψ ∈ Expr Bool in cOCL, where Expr Bool are expressions of type Boolean.

Our extension introduces three temporal operators, next (X), weak until (W), and (strong) until (U), which are quantified either existentially (E) or universally (A). We define the eventually and globally operators as equivalences: EFϕ ≡ E true U ϕ and AFϕ ≡ A true U ϕ, and EGϕ ≡ E ϕ W f alse and AGϕ ≡ A ϕ W f alse. Definition 2 (State space). The state space KM = (S, ι, T , B, E ) of a model M consists of a set of states S, a single initial state ι ∈ S, a transition relation T ⊆ E × E , a set of variable assignments B, and the environment relation E ⊆ S × B. An environment τ ∈ E is a pair (σ, β), where σ ∈ S is a state and β ∈ B a variable assignment.

For each state σ ∈ S the set of objects, associations, and attributes of M are accessible via σ|class, σ|assoc, and σ|attrs [ 18 ]. A variable assignment is a function β : Var t → Valt that, given a variable name, returns the current value of the associated variable, where t is the type of the associated variable. The concept of an environment τ = (σ, β) has been introduced by Richters and Gogolla [ 18 ]. Definition 3 (Path). Let KM = (S, ι, T , B, E ) be the state space of a model M . A path π is a finite or infinite sequence of environments (τ1, τ2, . . .) with τi ∈ E such that (τi, τi+1) ∈ T . For a path π = (τ1, τ2, . . .), we define the projection function π(i) = τi . The length of a path |π| = n for finite paths π = (τ1, . . . , τn), and |π| = ∞ for infinite paths π = (τ1, τ2, . . .).

We are now able to describe the semantics of cOCL as follows.

Definition 4 (Semantics). Let KM be a state space of model M . The semantics of a cOCL expression is defined by the rules i.–vi. of Definition 2 from [ 18 ] plus the following rules for the temporal extension. vii. IJA φ U ψK(τ ) = true ⇔ ∀ paths π with π(0) = τ : ∃n ∈ N, n ≤ |π| :

IJψK(π(n)) = true ∧ ∀ 0 ≤ i < n : IJφK(τi) = true viii. IJE φ U ψK(τ ) = true ⇔ ∃ path π with π(0) = τ : ∃n ∈ N, n ≤ |π| :

IJψK(π(n)) = true ∧ ∀ 0 ≤ i < n : IJφK(τi) = true ix. IJA φ W ψK(τ ) = true ⇔ ∀ paths π with π(0) = τ : ∀n ∈ N, n ≤ |π| :

IJφK(π(n)) = false → ∃i ∈ N, i ≤ n : IJψK(π(i)) = true x. IJE φ W ψK(τ ) = true ⇔ ∃ path π with π(0) = τ : ∀n ∈ N, n ≤ |π| :

IJφK(π(n)) = false → ∃i ∈ N, i ≤ n : IJψK(π(i)) = true xi. IJE X φK(τ ) = true ⇔ ∃ path π with π(0) = τ, |π| ≥ 1 : IJφK(π(1)) = true xii. IJA X φK(τ ) = true ⇔ ∀ paths π with π(0) = τ, |π| ≥ 1 : IJφK(π(1)) = true The semantics of the eventually and globally operators follow directly from the above definitions. We define a cOCL expression satisfiable as follows. Definition 5 (Satisfiability). A cOCL expression φ is satisfiable w.r.t. a state space KM iff IJφK(ι) is true w.r.t. KM . 3

A framework to integrate CTL and OCL

In the following we describe our verification framework that accepts MOF-based software models and cOCL specifications as input. This allows us to embed model checking support seamlessly into the MBE workflow. We introduce the general idea based on the (in)famous dining philosophers problem.

3.1 Basic Idea

Consider the model depicted in Fig. 1. The root node of type Table contains an arbitrary number of instances of type Philosopher, Plate, and Fork. Each philosopher is associated with exactly one plate. Each fork is assigned to two adjacent plates such that philosophers need to share their forks.

In order to eat, the philosophers need to pplicakteu. pWbhoetnh tthheeyleafrteadnodnteheeartiignhgt, ftohrekyorfeltehaesier Table phils* Philosopher plate tWheeirmfoodreklsthaneddypnuatmtihcebmehbaavcikoroonf tthhee dtianbinleg. *plates left f1or*ks l0e.f.1t r0i.g.1ht philosophers system with graph transforma- Plate Fork tions [ 7 ], but any other model transformation right 1 formalism would work equally well. Figure 2 1 shows the rules in storyboard notation. Rule (a) of Figure 2 creates an association to as- Fig. 1. Dining philosophers model sign the left fork to a philosopher whenever the philosopher has not picked up the left fork yet (forbid#1) and the philosopher to his right has not picked up the fork either (forbid#2). The rule to pick up the right fork works analogously. Rule (b) in Fig. 2 releases simultaneously the forks that a philosopher has picked up and deletes each of the associations between the philosopher and the left and right forks.

To check a cOCL property, we first need to create the state space of the dining philosophers system. The state space is obtained by recursively applying all matching graph transformation rules starting on a given initial model. For example, consider an initial model with one table, three philosophers, three plates, and three forks, where none of the philosophers has neither picked up a left fork nor a right fork. The initial state has six successor states, as both rules for picking up a left fork and a right fork can be applied to each philosopher. Overall, the resulting state space consists of 27 states. 3.2

Implementation

Our verification framework consists of two parts, a concrete syntax extension for our CTL-based OCL extension that we presented in Section 2, and the MocOCL model checker that verifies cOCL specifications.

preserve :Fork create left preserve :Philosopher forbid#2 left forbid#2 :Fork forbid#1 right

forbid#1 :Philosopher preserve

left plate preserve preserve :Plate preserve :Fork delete left preserve :Philosopher delete right preserve :Fork preserve

left plate preserve right preserve :Plate preserve (a) Pick up left fork rule. (b) Release forks rule.

Fig. 2. Graph transformation rules for the dining philosophers example.

The concrete syntax enhances the readability of cOCL expressions. It allows to write the temporal operators in their familiar long forms, i.e., Xϕ, Fϕ, Gϕ, ϕWψ, and ϕUψ become next ϕ, eventually ϕ, globally ϕ, ϕ unless ψ, and ϕ until ψ. The universal and existential quantifiers for temporal operators become always and sometimes.

The type definitions Sequence(t), Set(t), and Bag(t) and the function definitions mkSequencet, mkSett, and mkBagt that we use in the following definitions are those introduced by Richters and Gogolla [ 18 ]. For example, I(Sequence(t)) defines the set of all possible sequences of type t. We define I(Collection(t)) = (I(Sequence(t)) ∪ I(Set(t)) ∪ I(Bag(t))). The prototypical implementation of the MocOCL model checker performs the following steps. Given an initial environment, a set of model transformations, and a cOCL specification, MocOCL first generates the state space, then evaluates the cOCL properties, and finally reports to the modeler useful information on the reason of a specific evaluation result.

In MocOCL, the state space consists of a set of graphs. Each graph corresponds to an instance of the system and thus represents a system’s state at a discrete point in time. Given a graph transformation system G = (R, ι) with graph rewrite rules R and an initial state ι, the function stategenR: S → P (S × M)4 handles the generation of the state space. It expects as input a state σs and returns a set of pairs (σt, m) where σt denotes the successor state of σs and m : σClass → σClass ∪ {⊥} is a morphism that maps objects in σs to corresponding objects in σt, or to ⊥ if no such object exists. The successor state σt is obtained from σs by applying a rewrite rule r ∈ R to the graph reprer sented by σs. We write σs ⇒ σt to denote that σs is rewritten to σt by rule r ∈ R. The state space generation function is then defined as stategenR(σs) = Sr∈R{(σt, m)|σs ⇒r σt ∧ ∃m ∈ M : ∀c ∈ σs|class : m(c) ∈ σt|class ∨ m(c) = ⊥}. The helper function succ: E → P (E ) returns all environments reachable by a transition from the source environment τs = (σs, βs) and is defined by succ((σs, βs)) := {(σt, βt)|(σt, m) ∈ stategenR(σs), βt = mapvar(βs, m)}. The mapvar : B × M → B function takes a variable assignment βs of state σs and a mapping m ∈ M and updates βs with respect to m resulting in a variable assignment βt for the successor state σt. It is defined by mapcol(β(v), m) if ∃t : β(v) ∈ I(Collection(t))  mapvar(β(v), m) : v 7→ m(β(v)) β(v) if β(v) ∈ Dom(m), i.e., β(v) ∈ σclass otherwise.

A collection is mapped by the mapcol : Collection(t) × M → Collection(t) function, which applies mapvar recursively to all elements of the collection: mkSequencet(mapvar(x, m)|x ∈ X)  mapcol(X, m) = mkSett(mapvar(x, m)|e ∈ X) mkBagt(mapvar(x, m)|e ∈ X)

X ∈ Sequence(t) X ∈ Set(t) X ∈ Bag(t) 4 P (X) is the set of all finite subsets of X. This implementation gives us a state space KM = (S, ι, T , B, E ) with initial state ι ∈ G and (τs, τt) ∈ T ⇔ τt ∈ succ(τs), E being the transitive closure of applying the succ function to the initial environment (ι, βι), and S and B being all states and variable assignments occurring in an environment. Currently, we use Henshin’s graph rewrite engine [ 1 ] to generate the state space.

The evaluation of cOCL expres- ω = {τι}; Φ = Ψ = η = Δ = Δl = ∅ sions of the form (A|E) φ (U |W ) ψ is while ω 6= ∅ shown in Fig. 3. The algorithm con- pick τ = (σ, β) ∈ ω structs the sets Φ and Ψ that con- ω := ω \ {τ } tsaatnaidntesaallrtehsaticrahdtaesbselwethfηreortmehaϕta acϕno-dnsttaψatinehsoblaudltl, if iIfJψΨIKJ(:ψτ=)K(Ψτo)r∪t{IhτJeφ}nK(τ ) then where neither ϕ nor ψ hold. The else worklist ω contains all nodes that Φ := Φ ∪ {τ } need to be processed. The algorithm ω := ω ∪ succ(τ ) \ (Φ ∪ Ψ ∪ η) sets the worklist to the initial envi- end if ronment τι and uses the succ func- else tion to iteratively expand the set of η := η ∪ {τ } reachable environments. It evaluates end if ϕ and ψ in each environment τ and end while assigns τ to the corresponding sets repeat Φ and Ψ , or to η if neither ϕ or Δl := Δ ψ hold. Then, IJA φ U ψK(τ ) holds if Δ := {τ ∈ Φ | succ(τ )∩(Φ\Δl) = ∅} η is empty, and Φ contains neither until Δ = Δl lecnoymocctkple;teymI(;JcpEyItcJyφAleUoφr⇔ψWΦK(ψΔτc)Ko(nτh6=t)oalidΦhnso)slidfnasoΨcriyficdslηeena. doisEt-xepmrpestsyi;oFnasingd.(A3I.|EJAE)lgXφorWφithψamrKe(pτsi)meuhpdoloelmdcosedniefteΨd aiss IJ(A|E) XφK((σ, β)) = (∀|∃)n ∈ succ(σ, β) : IJφK(n) = true where we check if all (at least one) successor of the current state satisfies expression ϕ.

The evaluation of a cOCL expression yields a report that, besides returning the result of the evaluation, contains a cause or explanation for the result. A cause is is associated with a cOCL expression. It stores the result of the evaluation of the associated expression and, for each relevant sub-expression, a sub-cause. A sub-expression is relevant if it influences the result of its super-expression. For example, if the sub-expression ϕ in ϕ or ψ evaluates to true then no sub-cause is generated for ψ as the evaluation of ϕ uniquely determines the result of ϕ or ψ. If, however, both ϕ and ψ evaluate to false, then a sub-cause for each of the two sub-expressions is generated and stored in the cause of ϕ or ψ. Note that cause generation need not be deterministic, as is the case, for example, if both ϕ and ψ evaluate to true. In case of cOCL expressions the report generation becomes expensive fast. For example, the number of generated sub-causes for a counter-example trace of a EFϕ formula, where ϕ is a propositional formula without set operations, has as upper bound O(|KM | × |ϕ|) the size of the state space times the size of the formula ϕ.

A First Showcase

In this section, we illustrate how cOCL expressions can be used to express properties of a system. For the purpose of comparison, we also specify the properties as CTL formulas as used in Groove [ 17 ], which generates the state space similar to our model checker, but uses graph transformations to express properties of the system. Such a graph transformation-based expression evaluates to true if the graph transformation can be applied in the current state. Graph transformations are the only link between the temporal formula to be verified and the model of the system. Thus, it is neither possible to store and compare variables nor to iterate over multiple state space elements.

In the following, we formulate two properties based on the dining philosophers example introduced in the previous section. The statement ”every philosopher should always be able to eat at some point in the future” is specified as follows: self.philosophers->forAll(p | always globally always eventually (p.left <> null and p.right <> null))

Note that OCL allows us to quantify over all philosopher objects and with our extension we are able to say that in all reachable branches of the state space eventually a philosopher has to have a right and a left fork.

In Groove, every philosopher needs an ID to be traced. Additionally, there are no parametrized properties and thus a new graph transformation has to be specified for each philosopher. Then the graph transformation rules are specified as in Fig. 4 and the formula is specified in Groove as (A G A F phil1full) & (A G A F phil2full) & (A G A F phil3full)

The rule philXfull (see Fig. 5) is applicable when, and thus specifies the property that, the philosopher with ID X has forks in both hands.

The second example shows that in some cases, there can be an even more extreme blowup in necessary rule count. We want to check the property that a single fork is owned by exactly two adjacent philosophers. This is expressed in MocOCL as Fig. 4. Rule phil1full self.forks->forAll(f | self.philosophers-> select(p | (sometimes eventually p.left = f or p.right = f))->size() = 2)

In Groove, the statement p.left = f or p.right = f has to be specified for every fork and every philosopher. Thus, in the case of three philosophers nine graph transformation rules philXforkY have to be defined; in general, n2 graph transformation rules for n philosophers are necessary. Additionally, to specify that for every fork, exactly two philosophers may use Fig. 5. Rule the fork, the specification of ((phil1forkX & phil1forkY) & phil1fork1 !(phil1forkZ)) is required for every combination of X, Y, and Z. Consequently, the property in Groove grows rather large, even if we consider only three philosophers: (!((E F phil1fork1) & (E F phil1fork2) & (E F phil1fork3)) & (((E F phil1fork1) & ((E F phil1fork2) | (E F phil1fork3))) | ((E F phil1fork2) & (E F phil1fork3)))) & (!((E F phil2fork1) & (E F phil2fork2) & (E F phil2fork3)) & (((E F phil2fork1) & ((E F phil2fork2) | (E F phil2fork3))) | ((E F phil2fork2) & (E F phil2fork3)))) & (!((E F phil3fork1) & (E F phil3fork2) & (E F phil3fork3)) & (((E F phil3fork1) & ((E F phil3fork2) | (E F phil3fork3))) | ((E F phil3fork2) & (E F phil3fork3))))

These small examples already illustrate the benefits of combining OCL with temporal logics. Since our implementation is currently a prototypical proof of concept, we do not achieve the same performance as Groove. Here, we identified the following problems and possible solutions to overcome these issues. First, the state space generation is slow and can be improved with more sophisticated isomorphism checks and retrieval of mapping information. Second, there is room for improvement in the evaluation of consecutive temporal operators, where we plan to apply more advanced evaluation algorithms. And third, the OCL engine imposes a bottleneck, and we are in the process of investigating if alternative implementations of OCL are better suited for our demands. Overall, we are convinced that it is possible to find solutions to these issues. 5

Related Work

One of the first to suggest a temporal extension to OCL were Conrad and Turowski [ 4 ]. For describing the interactions of software components in a design by contract manner they introduce an OCL extension that adds past and future temporal operators. Their work targets only the specification of the component’s correct interaction, not the verification. Distefano et al. [ 5 ] propose a CTL-based logic, called BOTL, to specify static and dynamic properties of object-oriented systems without inheritance and sub-typing. Instead of extending OCL, they map OCL onto BOTL, thus providing a formal semantics for a large part of OCL based on BOTL. Ziemann et al. [ 21 ] aim to extend the semantics of the OCL standard with their proposed LTL-based extension, similar to our CTL solution. They need to extend the environment τ by an additional index i that points to the current state. Further, they analyze only finite sequences of states. We are not aware of any implentation of this approach. Soden and Eichler [ 20 ] also present an LTL based extension for OCL. They extend the semantics of the OCL standard and, like Ziemann et al., they introduce an additional index into the evaluation environment that captures the current time instant. They suggest to define the operational semantics of MOF-conforming models with the M3Action framework. This allows them to define a finite execution trace by a sequence of changes from which the actual states are derived by applying the changes in succession to the initial model up to the current state. Flake and Mueller [ 8 ] aim at a tight integration of UML class diagrams, state charts, and OCL, where the state charts describe the behavior of the associated class diagrams. They use time-based traces to capture the evolution of the system and propose a UML Profile to specify state-oriented, real-time invariants whose semantics are defined by a mapping to clocked CTL formulas. In regard to expressiveness, Bradfield et al. [ 2 ] propose the richest extension by embedding OCL into the observational μ-calculus. As noted by the authors this expressiveness comes at the price of complexity inherent to specifications using the μ-calculus. They thus suggest the use of predefined templates with concise semantics, but which hide the complexity of the underlying μ-calculus formula that is automatically generated from the template. We are not aware of any implementations realizing the above approaches.

Mullins and Oarga [ 16 ] present an extension to OCL, called EOCL, that augments OCL with CTL operators. They define EOCL’s operational semantics over object-oriented transition systems. The SOCLe tool translates class, state chart, and object diagrams into an abstract state machine and it checks on-the-fly if the system satisfies the specification given as an EOCL expression. Kyas et al. [ 15 ] present a prototype that verifies OCL properties over simplified UML class diagrams whose behavior is described by state machines. In contrast to all other approaches presented thus far they do not extend OCL with temporal operators but rather translate class diagrams, state machines, and OCL specifications into the input format of the PVS theorem prover. With PVS they are able to prove OCL properties of infinite state systems. Similar to Bradfield et al.’s proposed templates, Kanso and Taha [ 12 ] introduce a temporal extension based on Dwyer et al.’s patterns for the specification of properties for finite state systems [ 6 ]. Although these patterns are not as expressive as their CTL, LTL, or μ-calculus counterparts, they greatly simplify the property specification process. Kanso and Taha define a scenario-based semantics for their extension, where each scenario is a finite sequence of events.

It is thus the combination of our two contributions, a CTL-based extension of OCL, whose formal syntax and semantics extend the OCL standard without modifying existing definitions, and the implementation of the MocOCL model checker, that distinguishes our approach from previous works. 6

Conclusion and Future Work

In this paper, we present syntax and semantics of cOCL, our OCL extension with CTL-based temporal operators. Further, we describe the implementation and technical feasibility of our MocOCL model checker5 that verifies cOCL specifications. With first showcases we illustrate that the combination of OCL and CTL expressions allows for compact formulations of specifications.

In future work, we plan to improve our implementation in terms of efficiency and usability. Work on a detailed performance analysis is currently in progress. For dealing with the state explosion problem, symbolic model checking techniques will be considered. Finally, we would like to apply our approach in the context of larger V&V environments as for example in USE [ 9 ]. 5 MocOCL is available at www.modelevolution.org/prototypes/cocl

References

1. T. Arendt , E. Biermann , S. Jurack , C. Krause , and G. Taentzer . Henshin: Advanced Concepts and Tools for In-Place EMF Model Transformations . In MoDELS, volume 6394 of LNCS , pages 121 - 135 . Springer, 2010 .

2. J. C. Bradfield , J. K. Filipe , and P. Stevens. Enriching OCL Using Observational Mu-Calculus. In FASE , volume 2306 of LNCS , pages 203 - 217 . Springer, 2002 .

3. E. M. Clarke , O. Grumberg , and D. Peled . Model checking . MIT press, 1999 .

4. S. Conrad and K. Turowski . Temporal OCL Meeting Specification Demands for Business Components . In UML'01 , volume 2185 of LNCS , pages 151 - 165 . Springer, 2001 .

5. D. Distefano , J.-P. Katoen , and A. Rensink . On a Temporal Logic for ObjectBased Systems . In FMOODS, volume 177 of IFIP Conf. Proc. , pages 285 - 304 . Springer, 2000 .

6. M. B. Dwyer , G. S. Avrunin , and J. C. Corbett . Patterns in Property Specifications for Finite-State Verification . In ICSE , pages 411 - 420 . ACM, 1999 .

7. H. Ehrig , K. Ehrig , U. Prange , and G. Taentzer . Fundamentals of Algebraic Graph Transformation . Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2006 .

8. S. Flake and W. Mu ¨ller. Formal semantics of static and temporal state-oriented ocl constraints . Software and System Modeling , 2 ( 3 ): 164 - 186 , 2003 .

9. M. Gogolla , F. Bu¨ttner, and M. Richters . USE: A UML-based specification environment for validating UML and OCL . Sci. Comput . Program., 69 ( 1-3 ): 27 - 34 , 2007 .

10. O. M. Group . Object Constraint Language (OCL) V2.2 . http://www.omg.org/ spec/OCL/2.2/, February 2010 .

11. T. Jussila , J. Dubrovin , T. Junttila , T. L. Latvala , and I. Porres. Model Checking Dynamic and Hierarchical UML State Machines . In Proc. MoDeV2a: Model Development, Validation and Verification , pages 94 - 110 , 2006 .

12. B. Kanso and S. Taha . Temporal Constraint Support for OCL . In SLE , volume 7745 of LNCS , pages 83 - 103 . Springer, 2012 .

13. H. Kastenberg and A. Rensink . Model Checking Dynamic States in GROOVE . In SPIN, volume 3925 of LNCS , pages 299 - 305 . Springer, 2006 .

14. A. Knapp and J. Wuttke . Model Checking of UML 2.0 Interactions . In MoDELS Workshops, volume 4364 of LNCS , pages 42 - 51 . Springer, 2006 .

15. M. Kyas , H. Fecher , F. S. de Boer, J. Jacob , J. Hooman , M. van der Zwaag, T. Arons, and H. Kugler . Formalizing UML Models and OCL Constraints in PVS . Electr. Notes Theor. Comput. Sci. , 115 : 39 - 47 , 2005 .

16. J. Mullins and R. Oarga . Model Checking of Extended OCL Constraints on UML Models in SOCLe . In FMOODS, volume 4468 of LNCS , pages 59 - 75 . Springer, 2007 .

17. A. Rensink . The GROOVE Simulator: A Tool for State Space Generation . In AGTIVE , volume 3062 of LNCS , pages 479 - 485 . Springer, 2003 .

18. M. Richters and M. Gogolla . Ocl: Syntax, semantics, and tools . In Object Modeling with the OCL , volume 2263 of LNCS , pages 42 - 68 . Springer, 2002 .

19. B. Selic . What will it take? a view on adoption of model-based methods in practice . Software & Systems Modeling , 11 ( 4 ): 513 - 526 , 2012 .

20. M. Soden and H. Eichler . Temporal Extensions of OCL Revisited . In ECMDA-FA , volume 5562 of LNCS , pages 190 - 205 . Springer, 2009 .

21. P. Ziemann and M. Gogolla . OCL Extended with Temporal Logic . In Ershov Memorial Conference , volume 2890 of LNCS , pages 351 - 357 . Springer, 2003 .