102 Mapping OCL constraints into CTL-like logic and SML for UML validation Miloud BENNAMA and Thouraya BOUABANA-TEBIBEL Laboratoire de Communication dans les Systèmes Informatiques (LCSI) Ecole Nationale Supérieure d’Informatique (ESI) Alger, Ageria m_bennama@esi.dz, t_tebibel@esi.dz The UML (Unified Modeling Language) graphical models miss providing some pertinent elements of specification as constraints over objects and operations. To fill this lack, OCL (Object Constraint Language) has been developed by IBM and integrated to UML as a modern and formal modeling language, which is easy to learn and efficient to use. On the other hand, many works emerged providing a formal semantics to UML dynamic diagrams by using CP-nets (High-level Petri Nets). The latter are verified based on system properties written in temporal logic. The purpose of this paper is to assist the UML modeler, not necessarily familiar with temporal logics, by letting him expressing the properties in OCL language and proposing an automatic mapping of OCL invariants and pre/post-conditions into CTL-like logic (Computational Tree Logic) coupled with the functional programming language Standard ML. The obtained temporal logic formulas are verified over the state space of the CP-net models derived from UML diagrams by model-checking. UML; OCL; CP-nets; CPN-ML; ASKCTL; CPNtools; Mapping; model-checking. 1. INTRODUCTION A formal tool, called CPNtools, has emerged for analyzing CP-nets. It uses the functional UML [17] is the de facto standard for specifying programming language Standard ML [14,21] and both of the structural and behavioral aspects of CTL-like temporal logic, called ASKCTL [5], for systems. OCL (Object Constraint Language [16]), model description, data manipulation and an integral part of UML, allows for specifying properties specification. additional constraints on UML models in a more precise and concise manner. OCL has a We proposed in [3] an approach to translate the mathematical definition based on set theory with a Interaction Overview Diagram (IOD) to CP-nets for notion of object model and system states. UML simulation and state space analysis using and OCL are easy and familiar to users, but they CPNtools. To specify and check system properties, do not support validation tasks and their semantics the modeler is not familiar with temporal logic and is defined in a semi-formal way. ML language that require many skills. To provide a rigorous semantics for UML models, To assist the modeler in this phase of specification, CPN-nets [10] have been used by many studies we propose to allow him to express system [1,3,9,20] as an expressive semantics domain. properties in his usual language of specification, Also, OMG (Object Management Group) has namely OCL, and to automate the translation of inspired many UML concepts from Petri Nets, OCL properties to ASKCTL and ML. The resulting particularly, in activity diagrams. CP-nets are formulas are evaluated over the state space of the widely-used for specifying and analysing behaviour CP-net model derived from the IOD diagram. of concurrent systems. They consist in a transition Various works [2,4,7,12,15,23] have been system that supports model-checking validation undertaken to transform OCL into other formal method. languages. Our approach differs from works that Model-checking technique shows that a system use temporal logics to formalize OCL constraints in satisfies its specification. It requires a formal that it achieves a detailed mapping of basic and representation (as CP-nets) of the system and a complex expressions of OCL into Standard ML. specification that is often expressed in terms of a This extends our previous works on the IOD temporal logic formula [2]. diagrams mapping into CP-net models. Unlike other works, our approach translates the class 103 diagram, IOD diagram, and OCL specifications into feature. The contextual instance self then is an the input languages of CPNtools model-checker. instance of the type that owns the operation or method as a feature. The context declaration in The remainder of this paper is organized as OCL uses the context keyword, followed by the follows. Section 2 presents OCL language and its type and operation declaration. The stereotype of constraints whereas section 3 presents the constraint is shown by putting the labels ‘pre:’ and CPNtools and its input formal languages. Section 4 ‘post:’ before the actual Preconditions and describes our approach of mapping of OCL Postconditions [16]. expressions into ML functions and OCL constraints into ASKCTL formulas. Section 5 illustrates the context application of our approach over an ATM system. ::(: Section 6 recalls the related works. Finally, Section , ... ): 7 concludes and presents future works. pre : post : 2. OBJECT CONSTRAINT LANGAGE The UML has been widely accepted as a standard Optionally, the name of the precondition or for object-oriented modeling language and is postcondition may be written after the pre or post supported by a great number of CASE tools. The keyword, allowing the constraint to be referenced Object Constraint Language (OCL) is an integral by name. part of UML, and was introduced to express subtleties and nuances of meaning that diagrams cannot convey by themselves. 3. CP-NETS AND TEMPORAL LOGIC OCL has been introduced by IBM for business modeling and adopted by UML as a mean to 3.1 CPN-ML language specify invariants of classes and types in a class The CPN-ML [11] programming language is a model, to specify type invariant of stereotypes, to variation of functional programming language describe pre- and post-conditions on operations Standard ML (SML) used in CP-nets. CPN-ML and methods, to describe guards, and also as a embeds the Standard ML and extends it with navigation language. OCL is a language of typed constructs for defining colour sets and functions, expressions, where an expression can be declaring variables, and writing inscriptions in CP- universally and existentially quantified [13]. net models. SML provides the user with the expressiveness required to model data and data 2.1 Invariants manipulation of complexity found in industrial The OCL expression can be part of an Invariant systems. SML is also used to implement simulation, which is a Constraint stereotyped as an state space analysis, and performance analysis of «invariant». When the invariant is associated with a CP-net models. Classifier, the latter is referred to as a “type” in this clause. An OCL expression is an invariant of the (i) Colour sets: The CPN ML language type and must be true for all instances of that type provides a predefined set of basic types at any time [16] inherited from Standard ML that can be used as simple colour sets. context inv : (ii) Expressions and Types: In CP-nets, relatively simple expressions have been used as arc expressions, guards, and initial Optionally, the name of the constraint may be markings. It is possible to use the complete written after the inv keyword, allowing the set of Standard ML expressions. constraint to be referenced by name. (iii) Functions: Functions are similar to the procedures and methods known from Integrity constraints in OCL are represented as conventional programming languages. invariants defined in the context of a specific type, (iv) Recursion and Lists: Such loop statements named the context type of the constraint. Its body, are not available in a functional the Boolean condition to be checked, must be programming language, which instead satisfied by all instances of the context type. relies on recursive functions to express 2.1 Pre/post conditions iteration. The OCL expression can be part of a Precondition or Postcondition, corresponding to «precondition» and «postcondition» stereotypes of Constraint associated with an Operation or other behavioral 104 3.2 ASKCTL logic 4.1.1 Numbers and arithmetical operations The ASKCTL [5] is a CTL-like logic which is There are three types to express numbers in OCL: interpreted over the state spaces of CP-nets. The Real, Integer and UnlimitedNatural, where logic has been designed to express properties of UnlimitedNatural is a subtype of Integer and both state and transition information over the CP- Integer is a subtype of Real. The basic arithmetical net state space. The logic is powerful enough to (+, -, *, =, abs(), min(), max()) and comparison express many of the standard CP-net properties. operations (>, <, >=, <=) are defined for numbers. Using ASKCTL logic implies that we get a well Two types of conversion from Real to Integer are understood and easy to use framework for provided (floor(), round()) and additionally, a expressing a much wider range of properties. The conversion to string was introduced (toString()). models over which we interpret ASKCTL are state There are two operations defined for the Integer spaces of CP-nets. These graphs carry information and UnlimitedNatural types only: division quotient on both nodes and edges. (div()) and remainder (mod()). Table 1 shows the mapping of OCL numeral operations into ML. ASKCTL is a branching-time modal logic and an extension of Computational Tree Logic (CTL [8]). The OCL UnlimitedNatural type represents the set An ASKCTL statement is defined to be a state or a of non-negative integers. Its OCL declaration a : transition formula. For more details about ASKCTL UnlimitedNatural is expressed in ML by var a:INT syntax see [6] and [22]. with 0..maxINT;. All integer operations are applied in the UnlimitedNatural subtype except the 3.3 CP-nets negation operation. CP-nets [10] are high-level Petri nets widely-used The OCL Real type represents numerals with a formal method for system specification, design, decimal point. All integer operations are applied in simulation and verification. They provide a the Real supertype except the div and mod graphical oriented modeling language capable of operations. Additionally, the floor and around expressing concurrency, synchronization, operations are supported in Real type. resources sharing and non-determinism at different levels of abstraction. They combine the mathematic primitives of Petri Nets [18] and the expressive 4.1.2 Boolean type mapping power of SML. They support a variety of verification Basically OCL users work with the Boolean values techniques such as state space analysis and model true and false that are the instances of the Boolean simulation. type. OCL provides the basic logical operations and, or, not as well as the derived operations xor, 3.4 CPNtools implies. The OCL declaration syntax of a Boolean CPNtools [19] is a tool for editing, simulating, and a: Boolean is expressed in ML syntax by var a: analyzing CP-nets. The tool features incremental BOOL; syntax checking and code generation, which take In ML, the OCL Boolean conjunction ‘a and b’ place while a net is being constructed. A fast becomes ‘a andalso b’, disjunction ‘a or b’ becomes simulator efficiently handles untimed and timed ‘a orelse b’, implication ‘a implies b’ becomes ‘not a nets. Full and partial state spaces can be orelse b’ and negation ‘not a’ is the same. The generated and analyzed, and a standard state table 2 shows the mapping of OCL Boolean space report contains information, such as operations into ML. boundedness properties and liveness properties. CPNtools supports state space analysis and model-checking of ASKCTL logic. OCL ML Description A:Integer var a: INT; integer type declaration 4. MAPPING OF OCL A: var a:INT with natural type declaration UnlimitedNatural 0..maxINT ; 4.1. Mapping of OCL expressions to ML A:Real A:Real; real type declaration In OCL language, a number of basic types are A = B , A <> B A = B, A <> B equal, not equal predefined to the UML modeler. These predefined types, such as Boolean, UnlimitedNatural, Integer, A > B , A >= B , A > B , A >= B greater, greater or equal, less, A< B, A <= B , A< B, A <= B less or equal Real, Enumeration and String, are independent of any object model. In ML language, the same basic A + B , A – B , A + B , A – B , addition, subtraction, types are available with some difference in the A*B A*B multiplication syntax. Negation (only for real and -A ~A integer) 105 A. div(B) , A div B , A division quotient, remainder extract a substring of A.mod(B) mod B substring length len starting at (only for integer and natural) A.subString(i,i+len) (A,i,len) position i in A, first position A.min(B), INT.min(A,B), minimum, maximum is 0 A.max(B) INT.max(A,B) convert string A to list of A.characters() explode A absolute value chars A.abs abs A returns the i(th) char of A, the largest integer not larger A.at(i) sub (A, i) counting from zero. A.floor() floor A than A convert all chars to (only for real) A.toUpper() map toUpper A uppercase the integer nearest to A convert all chars to A. round() round A A.toLower() map toLower A (only for real) uppercase Table 1. Mapping of Numeral operations Table 3. Mapping of string operations 4.1.3 Strings and text operations 4.1.4 Enumeration type Strings are specified by sequences of printable OCL enumeration types are user-defined types. An ASCII characters surrounded with double quotes. enumeration type is defined by specifying a name The OCL declaration syntax of a string a: String is and a set of literals. An enumeration value is one of expressed in ML syntax by var a: String;. In both the literals used for its type definition. In ML, OCL and ML, the length of a string (size) can be enumerated values are explicitly named as determined, a string can be projected to a identifiers in the declaration. These values must be substring, and two strings can be concatenated (^). alphanumeric identifiers. Table 4 shows the Also, it is possible to access single or all characters mapping of OCL enumeration operations into ML. of a given string and to applied case conversion. Table 3 shows the mapping of OCL string OCL ML Description operations into ML. A: Var Enum = with enumeration type Enum{v0,v1,..,vn} v0| v1|...|vn; declaration equality and OCL ML Description A = #vi , A <> #vi A = #vi , A <> #vi inequality with an enumeration value A: Boolean var a: BOOL; Boolean type declaration A = B , A <> B A = B , A <> B equality , inequality Table 4. Mapping of enumeration operations. A and B A andalso B conjunction 4.1.5 TupleType A or B A orelse B disjunction Informally known as record type. It combines A xor B A <> B exclusive disjunction different types into a single aggregate type. The parts of a TupleType are described by its attributes, Implication A implies B not A orelse B each having a name and a type. (if A then B else true) The OCL TupleType declaration A: Tuple(id1:type1, not A not A negation id2:type2,…, idn:typen) is expressed in ML by : If the expression A is true colset tuple = record id1:type1 * … * idn:typen; if A then B else If A then B else then B must be true else C var A:tuple; C endif C must be true Values of this color set have the form: {id1=v1,..., idn=vn} where vi are values of type typei for Table 2. Mapping of Boolean operations 1<=i<=n. To extract the ith element of a product the following operation is used: #idi tuple OCL ML Description In ML, each component in the record color set may be a different type and each is identified by a A: String var A: STRING; String type declaration unique label so that each field is position- A = B , A <> B A = B , A <> B equality and inequality independent. A .size() String.size A String length A.concat(B) A^^B Concatenate two strings 106 4.1.5 CollectionType C1- contains_all C1 All elements of C2 are in >includesAll(C2) C2 C1 It describes a list of elements of a particular given C->isEmpty: C=nil Same as (c->size = 0) type. It is a concrete metaclass whose instances Boolean C->notEmpty: are the subclasses SetType, OrderedSetType, C<>nil Same as (not c->isEmpty) Boolean SequenceType, and BagType. Table 5. Mapping of standard operations (v) BagType is a collection type that describes a multiset of elements where each element may occur multiple times in the bag. The elements are unordered. OCL ML Description (vi) SequenceType is a collection type that The collection of those describes a list of elements where each C->select(x|p(x)) filter p C elements in c for which p element may occur multiple times in the is true. The collection of those sequence. The elements are ordered by C->reject(x|p(x)) filter (not p) C elements in c for which p their position in the sequence. is false. (vii) SetType is a collection type that describes Returns any element for a set of elements where each distinct which p is true C->any(x|p(x)) random (filter p C) where C->notEmpty() is element occurs only once in the set. The true elements are not ordered. returns true if p is true for C->exist(x|p(x)) List.exists p C (viii) OrderedSetType is a collection type that some element in C describes a set of elements where each C->forAll(x|p(x) ) (filter p C) = C returns true if p is true for distinct element occurs only once in the set. all element in C isUnique f C The elements are ordered by their position fun isUnique _ [] = in the sequence. false | isUnique _ [x]=true | isUnique C- Does f has unique value The OCL CollectionType declaration A: >isUnique(x|f(x)) f [x,y] = f(x)=f(y) | for all elements of C isUnique f (x::xs) = Collection(Type) is expressed in ML by: (f(x)=f(hd(xs))) colset collection= list Type; andalso (isUnique f var A : collection; xs); Returns a collection C- In ML, the values of a list color set are a sequence sort f C containing all elements >sortedBy(x|f(x)) ordered by f whose color set must be the same type. Values of Returns a collection this color set have form [v1, v2, ..., vn] where vi has containing the result of C->collect(x|f(x)) map f C type Type for i=1..n. applying f on all elements of C returns f(e1, f(e2, …,f(en, The four kind of collection in OCL have the same C->iterate(x, r=v| foldr f v C v) …)) where C = [e1, declaration in ML as a list color set but the f(x,r)) e2,…, en] difference is shown in the treatment of their operations. Table 5 shows the mapping of standard Table 6. Mapping of iteration operations operations while table 6 presents the mapping of iteration operations and table 7 describes the mapping of the collection operations. OCL ML Description A set corresponding C->asSet: to the collection remdupl C OCL ML Description Set (duplicates are Colset Collect = dropped). Collection type Collection (T) List T A sequence declaration Var C : Collect corresponding to the Number of elements in C->asSequence: collection. C->size() length C sort T.lt C the collection; Sequence More useful: c- Sum of elements in the >sortedBy C->sum():Integer foldr (fn (x,y) => collection. Elements must (Comparator(T)). x+y) 0 C be numbers or have a + C->asBag: A bag corresponding C operation defined Bag to the collection. foldr (fn (x,y) => if An OrdredSet x=e then y+1 else The number of times that C->asOrdredSet: corresponding to the C->count(e) sort T.lt (remdupl C) y) 0 C e is in c. OrdredSet collection (duplicates cf e C are dropped, ordred). Equality between two C->excludes(e): C1 = C2 OrdredSets or two not (mem C e) C exclude the element e Boolean C1=C2: Sequence s C->includes(e): Boolean contains_all C1 C2 mem C e C include the element e Equality between two Boollean andalso C1- ((intersect C1 C2) Sets or two Bags no element of C2 is in C1 contains_all C2 C1 >excludesAll(C2) = nil) 107 Inequality between var class_name : class_type; C1 <> C2 two OrdredSets or The attribute value class_name.atti is expressed in C1=C2: two Sequence s ML by #atti class_name;. Boolean not (contains_all C1 Inequality between C2 andalso two Sets or two Bags contains_all C2 C1) 4.2 Mapping of OCL Constraints to ASKCTL Subtraction of two collections C1 – C2 listsub C1 C2 where C2- OCL constraints consist of an OCL expression of >includesAll(C2) is type Boolean and some declaration connecting the true OCL expression to an item in the class diagram. In Remove all the case of pre and post-conditions, the constraint C->excluding(e) rmall e C appearances of e from C is bound to an operation; invariants are bound to a Add the element e at class. C->including(e) ins C e the end of C (C+e) An OCL invariant is an OCL expression associated returns the with a class. It must be true for all instances of that C1- >intersection(C2) intersect C1 C2 intersection of C1 class type at any time. Its structure is: and C2 Union of C1 and C2 context ClassType inv: ExpOcl. union C1 C2 (C1+C2) (for BagType and SequenceType) C1->union(C2) Union for SetType An invariant is translated by the ASKCTL formula: remdupl (union C1 and OrdredType (no C2) multiplicity) INV(NF("",ML(ExpOcl))) th return the i element C->at(i) List.nth(C, i-1) of a collection where i>0 where: return the last  ML() is a mapping function that gets an List.nth(C, (length Sequence and OrdredSet C->last() C)-1) element of a list equivalent expression in ML code. where C->size()>0 return the first  NF() is the node function used as a state C->first() hd C element of a list subformula. Its arguments are a string and a where C->notEmpty() ML function which takes a state space node is true and returns a Boolean. The colection C->append(e) C^^[e] obtained by  INV(A) is a state formula witch is true if the appending e to C argument A is true for all reachable states The colection C->prepend(e) e::C obtained by from the current state. prepending e to C C->subSequence ( The sequence from i, j ) List.take(List.drop(C, position i to j Figure 1 shows the verification of an OCL invariant i-1), C- The ordredset from on the CP-net state space where the ML Boolean j-i+1); >subOrderedSet(i,j) position i to j expression (MLExp=ML(ExpOCL)) must hold in all The set containing all reachable nodes. listsub (remdupl C1->symmetric the elements that are (union C1 C2)) Difference(C2) in C1 or in C2 but not (intersect C1 C2) in both Reverse the collection C->reverse() rev C C The collection consisting of C with List.take(C,i- element e inserted at C->insertAt(i,e) 1)^^[e]^^ position I (for List.drop(C,i-1) OrdredSet and Sequence) indexOf e C = if Index of element e in List.nth(C,0) = e C->indexOf(e) the then 0 else indexOf OrderedSet C e (lt C) +1 Table 7. Mapping of collection operations Figure 1. Mapping of OCL invariant 4.1.6 Classes and objects A pre/post condition OCL is associated with an OCL expressions can refer to classes, attributes, operation of a class. The pre condition must be true assocaionEnds and operations of the class before the operation call and the post condition diagram. The class type class_name (att1:type1, must be true after the operation execution. Its structure is: ….,attn:typen) is declared in ML as an record type : Colset class_type = record att1:type1* ….*attn:typen 108 Context ClassType::Operation(Parameters:Types): the balance is displayed. In all cases, the client ReturnType gets his card at the operation end. Pre: ExpOcl1 Post: ExpOcl2 Thus, the static view of the ATM system is modeled by a class diagram (see figure 3), and an object A pre/post condition is translated by an ASKCTL diagram, see figure 4. The object diagram is used formula: to initialize the model for a possible execution. INV(AND(OR(NOT(NF("",Fir(t1))),NF("", Bank ML(ExpOcl1))),OR(OR(NOT(NF("",Fir(t1))), NOT(NF("",ML(ExpOcl1)))), ID : string PINs : set{integer} FORALL_NEXT(AND( NF("",Fir(t2)), ATM FORALL_NEXT( NF("",ML(ExpOcl2)))))))); check_PIN() 1 check_amount() ID: string where: update_account() * cash: integer  t1 and t2 are the derived transitions from the 1 state: integer sending and receiving events of the message tax: integer * “operation call”. Client ejected_money: integer  Fir(t) indicates the firing of a transition t. insert_card() ID: string enter_PIN()  FORALL_NEXT(A): used as a state formula, PIN: integer looks at immediate successors, is true if the max_amount: integer PIN_ok() argument, A, is hold for all immediate asked_amount: integer PIN_error() successors. old_balance: integer select_withdrawal() 1 enter_amount() new_balance: integer amount_ok() Figure 2 shows the verification of an OCL pre/post- req_PIN() amount_error() condition on the CP-net state space where the ML display_option() balance() Boolean pre-expression (MLExpPre = eject_card() select_balance() ML(ExpOCL1)) must be true just prior the operation req_amount() * req_balance() execution (state i) and the ML Boolean post- eject_money() expression (MLExpPost = ML(ExpOCL2)) must be print_balance() true just after the operation execution (state i+2). display_insufficient() Figure 3. ATM Class Diagram b1 : Bank a1 : ATM ID= « b1 » PINs = set{100, 200, 300,400} ID = ‘ a1’ cash = 100000 state = 1 tax = 50 c1 : Client ejected_money ID = ‘c1’ =«0» PIN = 100 Figure 2. Mapping of OCL pre/post condition max_amount = 5000 asked_amount = 4000 c2 : Client old_balance = 9000 ID = ‘c2’ 5. CASE STUDY new_balance = 8000 PIN = 200 Our approach of mapping and analysis is applied to max_amount = 4000 an ATM system. To start the application, the client asked_amount = 3000 inserts his card in the dispenser. He then enters his old_balance = 8000 personal identification number (PIN). In the new_balance = 7000 absence of error, he chooses to withdraw money or view his balance. Otherwise, he starts again the identification phase. To withdraw money, he Figure 4. ATM Object Diagram introduces the amount and recovers his money if the balance is sufficient. For account inquiry, only 109 e1 Using the simulation tool, we can examine different sd iod_atm init scenarios and explore the behaviour of the system. mer1 e2 Simulation provides a partial validation of the model. It is often used to debug its dynamics. The sd ident simulation of a HCPN can be either interactive or client atm bank automatic with graphical feedback showing visually os1insert_card() os2 the tokens movement, enabled transitions and os3 req_pin() os4 places marking. The simulation feedback can be os5 pin os6 check_pin() interpreted by a helpful sequence diagram for user os7 os8 alt os10 pin_ok() facilities and errors detection. os9 display_option() os12 os11 pin_error() superpage siod_atm eject_card() mer1 e1 p init insockP t e2 ident ident [pin_error] t t sub s [pin_ok] dec1 fork e3 dec1 fork p outsock t e3 dec2 p insock dec2 withdrawal p balance help ref ref ref s insock s s balance help Withdrawal Balance t withdrawal t sub t sub Help sub mer2 p outsock e4 mer2 p outsock final joint p t joint e4 final ident subpage s t ident in ident client p inport p atm insert p bank p Figure 5. ATM IOD diagram os1 p t os2 t os1 os2 p req p p t os3 os4 t To illustrate the behaviour view of the ATM system, pin p os3 a we present in figure 5 the Interaction Overview os7 os8 Diagram (IOD) of the ATM. The ATM IOD consists os4 t check t p os7 p of three sequence diagrams: client identification, os8 p p balance and withdrawal transaction; each of which models a part of the system interactions. alt1 ident {ok} s p We limit ourselves to only show the identification p alt insock t alt1 sub p alt outsock outport SD. We use a TranslatorTool that implements the mapping rules developed in [3] for automatically {error} t alt2 sub s alt2 t ident out generating a CP-net model from the ATM IOD in accordance with the ATM Class Diagram. Figure 6. ATM CP-net model The obtained CP-net model (see figure 4) is initialized by the multi-set of tokens derived from the ATM Object Diagram, see figure 4. The initial As for the state space analysis, it is one of the main multi-set of tokens is given as follows: formal analysis methods of Petri Net. It has proven successful in the verification of systems. Once the {("client", "c1", (100,5000,4000,9000,8000)), state space is generated for the resulting CP-net ("client", "c2", (200,4000,3000,8000,9000)), model, we obtain a text file which contains a ("atm", "a1", [100000,1,50,0]), standard report providing information about generic ("bank", "b1", (100,200,300,400))} properties such as state space statistics, boundedness properties, home properties and The resulting CP-net model is executed in liveness properties. CPNtools for simulation, state space analysis and system properties verification. 110 ML standard queries available in CPNtools may MLInv is a ML function which allows verifying the also be evaluated. In the case of negative answers, OCL invariant condition. the user is helped to investigate why an expected property does not hold. If an unexpected dead state Property 2: after an “insufficient balance” message is found a shortest path from the initial state to the is returned by the machine, the client balance must dead state is helpful information, as a be decreased by the tax value. counterexample. This situation may be interpreted to UML user with both a sequence diagram OCL pre/post-condition: describing the error trace (events sequence), and Context Client::insufficient() an object diagram describing the dead marking let c:Client (object values). POST: (a.new_balance = a.old_balance - a.ATM.cach) However, as UML users are not necessary familiar with input languages of CPNtools (CP-nets, ASKCTL formula (without detail for post- ASKCTL and CPN-ML). The specification of condition): system properties, to check the model consistency use (ogpath^"/ASKCTL/ASKCTLloader.sml"); with the expected properties of the real system, will be difficult for users to understand. So, we allow Val CTLformula2= INV(or(not NF(“”, fire(t1)), UML user to express system properties in OCL FORALL_NEXT( and( NF( “”, fire(t2)), language, as invariants and pre/post conditions, on FORALL_NEXT( NF(“”, MLpost)))))); the class diagram, then we automatically map eval_node CTLformula2 1 these constraints into ASKCTL formulas based on CPN-ML functions. Finally, we check OCL properties on CP-net state space trough ASKCTL where FORALL_NEXT() is used as a state formula. formulas. Positive responses are shown to UML It is true if its argument is true for all immediate user and negative responses are interpreted by a state successors. t1 and t2 are derived transitions counterexample through a sequence diagram and from the sending and receiving events of the call an object diagram. operation message. Fire(t) indicates that the transition t is enabled. MLpost is a ML function We express in what follows four OCL properties which allows verifying the OCL post-condition. checked over the state space of the resulting CP- net model in CPNtools environment. Propriety 3: The machine does not eject money if the requested sum is greater than the cash Property 1: ATM machine does not eject money if machine or greater than the maximum or exceeds the client asks for an amount higher than its the client's balance amount. balance. OCL invariant: OCL invariant: Context c: Client Context c:Client INV: (c.asked_amount+c.ATM.tax > c.balance) or inv: (c.asked_amount > c.balance) implies (c.asked_amount+ c.ATM.tax > c.max_amount) or (c.ATM.eject_money = 0) (c.asked_amount+a.ATM.tax > c.ATM.cash) implies c.ATM.eject_money=0 ASKCTL formula (without detail for invariant ASKCTL formula 3: condition): use (ogpath^"/ASKCTL/ASKCTLloader.sml"); use (ogpath^"/ASKCTL/ASKCTLloader.sml"); val CTLFormula3 = INV(NF("",MLInv)) ; val CTLFormula1 = INV( NF("",MLInv)); eval_node CTLFormula1 1 eval_node CTLFormula3 1; fun MLInv3 n = where INV() is a state formula which is true if its if (Mark.SubPageAmountError'P11 1 n) <> empty argument is true for all reachable states. then CheckEjctedMoney n Eval_node() is a function that allows to evaluate a else true state formula from a specified state node (initial fun CheckEjectedMoney n = state node = 1). It returns true or false, and in the let case of false, it also prints out a diagnostic report. val atm= List.nth(Mark.SubPageAmountError 'P11 Thus, the first code line allows loading the ASKCTL 1 n,0) :TOBJ; library. The ASKCTL library has two parts: one val class=(#1 atm): STRING; which implements the language of the logic, and val ID=(#2 atm) : STRING; one which implements the model checker [6]. val list=(#3 atm): INTlist; in 111 (class="atm") andalso (ID="a1") andalso et al. provide in [7] a formal semantics to OCL by (List.nth(list,3)=0) using OBTL (Object-Based Temporal Logic), which end facilitates the specification of dynamic and static properties of object-based systems. They do not Property 4: The machine rejects the user PIN if it expand OCL with temporal operators, but provide a does not appear in the bank data. The machine is theoretical precise mapping of a part of OCL into thus in a state of reject. OBTL. Cengarle and Knapp propose in [4] an extension of OCL, called OCL/RT, for modeling OCL pre/post condition: real-time and reactive systems. OCL/RT introduces Context Bank :: pin_error() a general notion of time and event to describe the Let b :bank temporal behavior of UML models. Mullins and PRE : b.PINsexcludes(b.client.PIN) Oarga provide in [15] an OCL extension, called POST : atm.state =0 EOCL, with CTL temporal operators. This extension is strongly inspired by BOTL, and allows model checking EOCL properties on UML models ASKCTL formula 4: expressed as abstract state machines. use (ogpath^"/ASKCTL/ASKCTLloader.sml"); Theoretically, our approach of OCL formalization val CTLFormula4 = INV( AND( OR( NOT( NF("", can be compared to [7] when translating invariants firt1)), and pre/post conditions to a variant of CTL logic. NF("",MLpre)),OR(OR(NOT(NF("",firt1)),NOT(NF("" But, practically, our work uses a specific logic , MLpre))), EXIST_NEXT( AND( NF( "", firt2), strongly based on a functional programming EXIST_NEXT( NF( "", MLpost))))))); language SML in CP-nets context. This allows eval_node CTLFormula4 1 detailed mapping of basic and complex types and operations of OCL language. Our approach is fun firt1 n = ((Mark.SubPagePinError'P20 1 n) <> implemented and integrated in a validation empty) framework of UML models by using CPNtools fun firt2 n = ((Mark.SubPagePinError'P_msg1 1 n) environment. <> empty)andalso((Mark.SubPagePinError'P10 1 n) <> empty) 7. CONCLUSION fun MLpre n = let To help and assist UML modelers verifying their val bank= List.nth(Mark.SubPagePinError'P20 1 specification, we proposed to automatically n,0) :TOBJ; translate OCL properties, specified on the class val list2=(#3 bank): INTlist; diagram, to CTL-like logic based on SML. We also val client= List.nth(Mark.SubPagePinError'P00 1 present in details the translation of basic and n,0) :TOBJ; val list0=(#3 client): INTlist; complex expressions of OCL by exploiting the in (not(checkpin list0 list2)) end expressiveness of the functional programming language CPN-ML. We relied on the class diagram fun MLpost n = for the static view of the system and the IOD let val atm= List.nth(Mark.SubPagePinError'P11 1 diagram for the behaviour view of the system. The n,0) :TOBJ; CP-net model derived from the UML description is val list1=(#3 atm): INTlist; in (List.nth(list1,1)=0) analysed by model-checking based on OCL end constraints derived to ASKCTL logic. To the best of our knowledge, it is the first work that uses where MLpre is a ML function which allows Standard ML to formulate OCL expressions in a verifying the OCL pre-condition. CP-net context. The resulting formulas are succinct and of reduced execution time as ASKCTL logic is based on the functional and recursive aspect of ML 6. RELATED WORKS as well as the Strongly Connected Component graph (SCC). ASKCTL formulas have been OCL has been formalized by various formal evaluated over the generated state space of CP- languages such as B, Z, CSP, PVS, mu-calculs net model within CPNtools environment. In case of and temporal logic. Many temporal extensions of negative answers, we propose to help the user OCL exist. Ziemann and Gogolla aim in [23] to investigating why an expected property does not expand the semantics of the language with a LTL- hold. For this purpose, a sequence diagram is based extension. Bill et al. present in [2] an OCL returned to the user relating the property error extension with CTL-based temporal operators. trace. Kanso and Taha propose in [12] a pattern-based extension of the OCL language to express temporal constraints on object-oriented systems. Distefano 112 For future works, we plan to improve our 11. Jensen, K., & Kristensen, L. M. implementation with regard to efficiency and (2009). Coloured Petri nets: modelling and usability. We also plan to integrate the proposed validation of concurrent systems. Springer. approach of mapping in a CASE tool (Computer- 12. Kanso, B., & Taha, S. (2013). Temporal Aided Software Engineering) of UML2 in order to Constraint Support for OCL. In Software generalize its application to other dynamic Language Engineering (pp. 83-103). Springer diagrams. Berlin Heidelberg. 13. Mandel, L., & Cengarle, M. V. (1999). On the 8. REFERENCES expressive power of the Object Constraint Language OCL. Available on the World Wide 1. Alhroob, A., Dahal, K., & Hossain, A. (2010, Web: http://www. fast. de/projeckte/forsoft/ocl. October). Transforming UML sequence diagram to high level Petri Net. In Software 14. Milner, R. (Ed.). (1997). The definition of Technology and Engineering (ICSTE), 2010 standard ML: revised. The MIT press. 2nd International Conference on (Vol. 1, pp. 15. Mullins, J., & Oarga, R. (2007). Model checking V1-260). IEEE. of extended OCL constraints on UML models in 2. Bill, R., Gabmeyer, S., Kaufmann, P., & Seidl, SOCLe. In Formal Methods for Open Object- M. (2013). OCL meets CTL: Towards CTL- Based Distributed Systems (pp. 59-75). Extended OCL Model Checking. In Springer Berlin Heidelberg. Proceedings of the MODELS 2013 OCL 16. OMG, Object Constraint Language 2.3.1, Doc Workshop} (Vol. 1092, pp. 13-22). Number: formal/2012-01-01, 2012. 3. Bennama, M., & Bouabana–Tebibel, T. (2013). 17. OMG, UML Superstructure Specification 2.4.1, Validation environment of UML2 IOD based on Doc Number: formal/2011-08-06, 2011. hierarchical coloured Petri nets. International Journal of Computer Applications in 18. Petri, C. A. (1962). Kommunikation mit Technology, 47(2), 227-240. Automaten. Bonn: Institut f¨ur Instrumentelle Mathematik, Schriften des IIM Nr. 2, 1962. 4. Cengarle, M. V., & Knapp, A. (2002). Towards ocl/rt. In FME 2002: Formal Methods—Getting 19. Ratzer, A. V., Wells, L., Lassen, H. M., IT Right (pp. 390-409). Springer Berlin Laursen, M., Qvortrup, J. F., Stissing, M. S., ... Heidelberg. & Jensen, K. (2003). CPN tools for editing, simulating, and analysing coloured Petri nets. 5. Cheng, A., Christensen, S., & Mortensen, K. H. In Applications and Theory of Petri Nets 2003 (1997). Model checking Coloured Petri Nets- (pp. 450-462). Springer Berlin Heidelberg. exploiting strongly connected components. DAIMI Report Series, 26(519). 20. Staines, T. S. (2008, March). Intuitive mapping of UML 2 activity diagrams into fundamental 6. Christensen, S., & Mortensen, H.K. (1996) modeling concept Petri net diagrams and ‘Design/CPN ASKCTL Manual Version 0.9’, colored Petri nets. ECBS 2008. 15th Annual University of Aarhus. IEEE International Conference and Workshop 7. Distefano, D., Katoen, J. P., & Rensink, A. on the (pp. 191-200). IEEE. (2000). On a temporal logic for object-based 21. Ullman, J. D. (1998). Elements of ML systems (pp. 305-325). Springer US. programming. 8. Edmund M. Clarke, E. A. Emerson, and A. P. 22. Zaidi, A. K., & Levis, A. H. (2006). Verification Sistla, “Automatic Verification of Finite State of System Architectures Using Modal Logics Concurrent System Using Temporal Logic”, and Formal Model Checking Techniques. In ACM Transactions on Programming Conference on Systems Engineering Research Languages and Systems, vol. 8(2), 1986, pp. (CSER). 244-263. 23. Ziemann, P., & Gogolla, M. (2003, January). 9. Fernandes, J. M., Tjell, S., Baek Jorgensen, J., Ocl extended with temporal logic. In & Ribeiro, Ó. (2007, May). Designing tool Perspectives of System Informatics (pp. 351- support for translating use cases and UML 2.0 357). Springer Berlin Heidelberg. sequence diagrams into a coloured Petri net. SCESM'07: ICSE Workshops 2007. Sixth International Workshop on (pp. 2-2). IEEE. 10. Jensen, K. (1998) An Introduction to the Practical Use of Coloured Petri Nets. Lectures on Petri Nets II: Applications, Lecture Notes in Computer Science, 1492, 237-292, 1998.