OCL meets CTL: Towards CTL-Extended OCL Model Checking? Robert Bill1 , Sebastian Gabmeyer1 , Petra Kaufmann1 , Martina Seidl1,2 1 Business Informatics Group Vienna University of Technology, Vienna, Austria {bill, gabmeyer, kaufmann, seidl}@big.tuwien.ac.at 2 Institute for Formal Models and Verification, Johannes Kepler University, Linz, Austria 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. How- ever, 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 tem- poral operators to express properties over the lifetime of an instance model. We explain syntax and semantics of our OCL extension and pro- vide a prototypical implementation of our MocOCL model checker. 1 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. 13 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 environ- ment 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 CTL- extended 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 implemen- tation of our verification framework. Finally, after showcasing a first case study (Section 4), we close the paper with an overview of related approaches (Sec- tion 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 uni- versally (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. 14 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 → Val t 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 seman- tics 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. 15 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 philoso- pher 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 pick up both the left and the right fork of their phils Philosopher plate Table plate. When they are done eating, they release * their forks and put them back on the table. plates forks left right * We model the dynamic behavior of the dining * left 1 0..1 0..1 philosophers system with graph transforma- Plate Fork tions [7], but any other model transformation right 1 1 formalism would work equally well. Figure 2 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 philoso- pher 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 apply- ing 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 forbid#1 forbid#1 preserve :Fork right :Philosopher :Fork preserve create preserve delete left left left left preserve plate preserve preserve plate preserve :Philosopher preserve :Plate :Philosopher preserve :Plate forbid#2 delete preserve left right right forbid#2 preserve :Fork :Fork (a) Pick up left fork rule. (b) Release forks rule. Fig. 2. Graph transformation rules for the dining philosophers example. 16 The concrete syntax enhances the readability of cOCL expressions. It al- lows 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 be- come always and sometimes. The type definitions Sequence(t), Set(t), and Bag(t) and the function defini- tions 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 en- vironment, 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 corre- sponds to an instance of the system and thus represents a system’s state at a dis- crete 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 corre- sponding 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 repre- sented by σs . We write σs ⇒ σt to denote that σs is rewritten to σt by rule r r ∈ R. The state space generation function is then defined as stategenR (σs ) = r∈R {(σt , m)|σs ⇒ σt ∧ ∃m ∈ M : ∀c ∈ σs |class : m(c) ∈ σt |class ∨ m(c) = S r ⊥}. 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)) if β(v) ∈ Dom(m), i.e., β(v) ∈ σclass otherwise.  β(v)  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) X ∈ Sequence(t)   mapcol(X, m) = mkSett (mapvar(x, m)|e ∈ X) X ∈ Set(t) mkBagt (mapvar(x, m)|e ∈ X)  X ∈ Bag(t)  4 P (X) is the set of all finite subsets of X. 17 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. Cur- rently, 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- ω := ω \ {τ } tain all states where ϕ and ψ hold, if IJψK(τ ) or IJφK(τ ) then and a third set η that contains all if IJψK(τ ) then states reachable from a ϕ-state but Ψ := Ψ ∪ {τ } 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 cycle (cycle ⇔ ∆ 6= Φ) nor dead- lock; IJE φ U ψK(τ ) holds if Ψ is not Fig. 3. Algorithm pseudo code empty; IJA φ W ψK(τ ) holds if η is empty; and IJE φ W ψK(τ ) holds if Ψ is not empty or Φ contains a cycle. Expressions (A|E) Xφ are implemented as 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 return- ing 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 ϕ. 18 4 A First Showcase In this section, we illustrate how cOCL expressions can be used to express prop- erties 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 transfor- mations 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 transfor- mation 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: 19 (!((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 Tur- owski [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 20 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 ex- pressiveness, 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 automat- ically 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 seman- tics 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 tem- poral 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 exten- sion 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 spec- ifications. 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 tech- niques 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 21 References 1. T. Arendt, E. Biermann, S. Jurack, C. Krause, and G. Taentzer. Henshin: Ad- vanced 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 Object- Based 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. Müller. Formal semantics of static and temporal state-oriented ocl constraints. Software and System Modeling, 2(3):164–186, 2003. 9. M. Gogolla, F. Büttner, and M. Richters. USE: A UML-based specification en- vironment 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 Check- ing Dynamic and Hierarchical UML State Machines. In Proc. MoDeV2 a: 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. 22