Home

UMC 3.3 User Guide - Formal Methods && Tools Group

1. null AttrName Selection VarName Selection ObjName self this IntExpr Number AttrName Selection VarName Selection Intexpr intop IntExpr VectorExpr head VectorExpr AttrName VarName VectorExpr VectorExpr VectorExpr tail StaticExpr Number ObjName null self this relop wen lt intop wou nyu mod TypeName int bool obj ClassName int bool obj ClassName An Overview of the Dynamic semantics of UMC models In the UML 1 4 standard definition there is a first attempt to assign a reasonably defined dynamic semantics i e the possible behaviours to the state machine associated with a statechart The basic concept used in the standard to define the possible evolutions of a the state machine configuration is the concept of run to completion step UMC follows these standard indications with a few simplifications due to the set of UML features not yet supported by UMC From a logic point of view the possible evolutions of a given state machine configuration can be discovered by performing the following substeps a Selecting current trigger The current event to be dispatched is selected from the object event queue which might also a system generated completion event b Dealing with active states triggers and guards It is identified
2. or The token as separator between Signals Operations Vars items and Defer events can be substituted by The token and in boolean expressions can be substituted by amp or amp amp The token or in boolean expressions can be substituted by or The token not in boolean expressions can be substituted by The token in boolean expressions can be substituted by The token in boolean expressions can be substituted by The token in assignments can be substituted by The token gt in Object instantiations can be substituted by or lt In the case of empty completion transitions the sequence gt can be substituted by gt Another completely alternative syntactic structure in Hugo style for transitions 1s also source gt target trigger guard actions In the definition of a Statepath inside source and target of a transition all the outer prefixes which are not necessary to univoquely identify a substate can be omitted e g Top S1 R2 S3 s4 can be substituted by s4 if such s4 is unique e g Top can be always omitted The keywords Vars Operations Signals Transitions can be followed by The token end can be followed by the name of the class Unsupported features With respect to UML 1 4 there are several statechart features which are not supported by the current release of UMC The most relevant of these unsupported features a
3. not max 2 not FixpointBody not 2 Even if monotonicity of a fixpoint formula is not strictly required it is not advised to make use of non monotonic formulas because their meaning in not necessarily intuitive E g the formula min Z not z holds for any state because its semantics is given by false or not false or not not false or Ra The above is equivalent to false or true or whose value is true It is likely that in future version of the tool the monotonicity of the formula will be required and checked The mu calculus is an very powerful logic and can be used to encode all the other CTL ACTL like temporal constructs However because of its low level of abstraction writing and understanding formulas written in pure calculus can be a particularly hard task For this reason it is useful to explicitly define the other CTL ACTL like modalities which allow a more natural expression of the system properties and a reasonably efficient way to 15 evaluate them the full mu calculus is known to have a complexity which is exponential w r t the alternation depth of the formula While the CTL ACTL modalities will be described later here we only show a few from simple to complex properties which unfortunately cannot be expressed in ACTL like modalities and hence need the explicit use of fixpoint operators There exist an infinite path whose evolution steps all satisfy the action expression b The above can be en
4. take_tray OUT eating Self DEPLANING deboard atLoc Destination gt FINAL PLANE STATECHART v ja allow_boarding T D T MyDest D T1 onboard Self atLoc boarding done LEAVING allow_takeott atLoc takeoff done aiLoc Ti take tray FLYING takeback_tray MyDestlanding_request Self LANDING jo allow_landing MyDest landing done Self atLoc MyDest T1 deboard 6 PASSENGER STATECHART STARTING atLoc checkin Destination Self N Ny TRYING CHECKIN 666 _ok checkin_closed stination Self atLoc checkiriDes BOARDING T onboard Plane y atLoc Plane EATING take tray OUT atLoc takeback_tray eating Self Destination delayed MyDest landing_request Self The initial deployment of the system is defined by the following Object declarations NITIAL VALUE FOR ATTRIBUTES MyPlane gt Planel Destination Destination gt Airport2 gt Airportl OBJECT CLASS Object Airportl Airport MyLink gt Airport2 Object Airport2 Airport MyLink gt Airportl1 Object Travelerl Passenger atLoc gt Airportl Object Traveler2 Passenger atLoc gt Airport2 Object Planel Plane atLoc gt Airportl 39 An example of property which can be verified is the following It is always true that Traveller1 performs an eating operation only while flying on Plan
5. A transition with more than one target is called a fork transition The trigger of a transition can be an event declaration exactly matching one of the definitions already given in the events section of the chart or the hyphen symbol which means the absence of any explicit trigger i e a completion transition If the trigger is an event declaration with formal parameters the name of the parameters can be used inside the actions part of the transition source gt target is a shortcut for source lt target The guard if present is a simple form of boolean expression involving the object attributes If the trigger of a transition is a synchronous event call operation then an explicit return action must be executed by the object in the same transition if we want to notify the completion of the call Moreover during the execution of a transition triggered by a synchronous call an implicit caller parameter of type obj is available such parameter identifies the calling object and can be used to notify the completion of the operation maybe also from subsequent transitions by the explicit sending of calling return signal this allows the support of some kind of delegations The Action Language The Actions part of a transition is a sequence of simple or composite actions A simple action can be an assignment of an expression to a local or transition variable the sending of an asynchronous signal to a t
6. forall globally exists until forall until exists until forall until exists until3 E FORM1 action expr action expr FORM2 forall until3 A 1 action expr U action expr2 FORM2 weak diamond gt gt action expr lt lt weak box action expr FORM More Shortcuts FINAL is a shortcut for not lt true gt true 4 The UMC tool and how to use it The UMC environment is actually two faced From one side we have a basic command line oriented umc tool easily portable to many platforms which implements the basic exploration and verification features From another side we have an experimental www interface an html browser is needed to view it which integrates the basic umc features with graphic features and further abstraction features and which allows to use the tool remotely from the web with all the advantages and disadvantages of the case 4 1 Command line interface umc is in its original form is a command line oriented tool which is called with a parameter which is the name of a lt file gt umc document containing the textual description of an UML model Starting umc lt umc mymodel umc Once started umc enters into a loop inside which it accepts logic formulas to be evaluated or other umc commands to be executed umc version 2 5 Loading the model from file my
7. min VARID FORM gt action expr gt FORM action expr FORM VARID expressions false tau and action expr and action expr or action expr or action expr enclosing basic mu formula maxfix maxfix minfix mu box action action expr true action expr action expr source action expr target event args Jattr attr 26100 simple expr lt uyn on au f n CTL ACTL like formulas not action expr obj a relop actl like formula exists next1l forall nextl exists next2 forall next2 exists future forall future exists globally forall globally exists untill forall untill exists until2 forall until2 exists until3 forall until3 weak diamond weak box EX FORM AX FORM EX action expr FORM action expr FORM EF FORM AF FORM EG FORM AG FORM 1 E FORM U FORM2 1 A 1 U FORM2 2 E FORM1 action expr U FORM2 2 A FORM1 action expr U 2 22 exists nextl forall nextl exists next2 forall next2 exists future forall future exists globally
8. op1 _caller obj x op2 _caller obj int op3 _caller obj z Classname w bool Vars v1 int 0 v2 Classname v3 bool True v1 0 vi 3 v2 s4 self s4 z 1 lt 0 m pP vl vl 1 v2 s4 self OUT print v1 end Classname 30 Observing the evolutions map Selecting the Model Evolutions button in the right column is shown a graphical map of the possible system evolutions starting from the current configuration The map is shown in SVG format hence an appropriate SVG viewer is needed so far the free Adobe SVG viewer seems to be the best plugin usable for this purpose In addition a JPG translation of the design can be requested and the original textual code in the dot formal can be viewed The nodes in the graph represent the system configurations and the edges the possible system evolutions In the design Edges are labelled with the observed signals generated by that evolution event which are not considered observable with respect to the current observation criteria are not shown The generated graph is truncated after a certain depth user customizable By clicking over one of its deepest leaves a new map is generated starting from that node Model Evolutions Chart Glass miyciass Set the graphics frame dimension to 1X 1 5X 3X 6X 12X Wars xcint Signals step Operations State top 12 A step x 0 O x 4 Object obj1 myclass
9. 1X 1 5X 3X 6X 12X Operati State top 5 Transtions 5 1 step 0 2 1 0 x Object obj1 myclass Export the graph in DOT format or as a JPG picture or as plain SVG data or as a TAB structure The following graph shows an abstract view of the model evolutions In particular it shows a complete trace minimization of the original evolutions tree built accordingly to the current observation criteria If you cannot visualize then picture below you probably need to install a svg viewer plug in like that of Adobe Use Command mouse to zoom in Command shift mouse to zoom out alttmouse to move the picture Use ctrl mouse to access the svg menu The formula is TRUE em configurations o Operation State top 2 step x 0 x 0 x x Selecting the Formula Definition button an editing area is shown on the right frame of UMC were the formula to be checked can be edited 33 Once the mu UCTL formula has been written we start the evaluation selecting the Verify formula button The evaluation is then started and its results shown in the same editing frame When the evaluation of a formula completes if we want more details on how the result was achieved we can select the Formula Explanation button which opens a pop up window in which is shown a fragment of the model Its which is sufficient to exemplify the validity of the formula Nodes of the Its are labelled with
10. NAME MyModel OBJECT QUEUE CURRENT TRIGGER CURRENT VARIABLES ACTIVE STATES Top sl FIREABLE TRANSITIONS 1 Tracing the system evolutions tree The trace command which takes as argument the depth at which the trace should be truncated allows to trace the possible system evolutions starting from the current configuration For each evolution it is shown the source and target configuration the evolving object and the sequence of signals if any generated by the evolution 24 If the showstuttering preference is set to true this is the default case umc generates a dummy ouT lostevent event signal each time a stuttering evolution occurs i e when an object discards the current triggering event because no fireable transitions are available trace 4 Cl MyModel gt 2 1 C2 is FINAL Interactively exploring the system evolutions tree The explore command starts a nested exploration cycle inside which the user is allowed to interactively select one of the possible evolutions from the current state display some information about the current configuration or to climb back in the evolutions tree explore Enter a number to select an evolution 1 to get more info on this state to exit b to go back one step tn to trace the LTS tree for n levels Current Configuration Cl Possible Evolutions 1 a gt C2 1 lt explore gt i CURRENT CONFIGURATION Cl OBJECT NAME MyMode
11. Oty 1340841 Obj 0 IOUE pera Export the graph in DOT format or as a JPG picture It is possible to observe the details of a specific system configuration clicking over the corresponding node The graph shows the model evolutions graph labelled accordingly to the current observation criteria The observation criteria can be checked or changed by acting on the default Preferences If you cannot visualize then picture below you probably need to install a svg viewer plug in like that of Adobe Use Command mouse to zoom in Command shift mouse to zoom out alt mouse to move the picture Use ctrl mouse to access the svg menu Clicking on one of the internal nodes instead a new window is opened pop up windows opening should be allowed containing the detailed description of that configuration 31 Configuration C1 Vars v1 0 v2 Obj1 v3 True Active States Top s1 Queue Possible System Evolutions 01 lt 02 Objt v1 3 s4 Obj1 Active Transitions 51 gt 52 v1 0 v1 3 v2 s4 self Abstracting the concrete model Selecting the Model Abstractions button it is possible to visualize a minimized evolution graph representing the system behaviour This functionality is useful when we are observing the system from an high level point of view and we focus our attention on just a small aspect of the system behaviour For example whenever we want to observe the evolution in time of just a single objec
12. P P allow_landing gt HANDLING ARRIVALS HANDLING ARRIVALS landing request P P landing delayed gt HANDLING ARRIVALS HANDLING ARRIVALS checkin D T T checkin_closed gt HANDLING_ARRIVALS HANDLING ARRIVALS landing done P MyPlane P gt HANDLING CHECKIN Class Plane Vars Tl obj MyDest obj atLoc obj Events allow _boarding T o0bj D o0bj allow_takeoff takeback_tray allow_landing landing delayed State Top BOARDING LEAVING FLYING LANDING BOARDING allow_boarding T D Tl T MyDest D Tl onboard Self atLoc boarding done gt LEAVING LEAVING allow_takeoff atLoc takeoff_done atLoc null Tl take_tray gt FLYING FLYING takeback_tray MyDest landing request Self gt LANDING LANDING landing delayed MyDest landing request Self gt LANDING LANDING allow_landing MyDest landing done Self atLoc MyDest T1l deboard gt BOARDING 38 onboard P obj take_tray deboard STARTING TRYING CHECKIN BOARDING FLYING DEPLANING FINAL gt TRYING CHECKIN gt TRYING CHECKIN P gt FLYING atLoc takeback_tray gt DEPLANING Class Passenger Vars atLoc obj Events checkin_ok State Top Destination obj checkin closed STARTING atLoc checkin Destination Self TRYING CHECKIN checkin_closed atLoc checkin Destination Self TRYING CHECKIN checkin_ok gt BOARDING BOARDING onboard P atLoc FLYING
13. directions We are interested in exploring and exploiting the advantages given by the on the fly approach to model construction and checking 5 2 9 We are interested in investigating the kind of user interface which might help a non expert user in taking advantage of formal specifications and verification techniques Weare interested in testing the appropriateness of the UML 19 26 methodology and in particular in the statecharts technology for the specification and verification of the dynamic behaviour of a system Weare interested in experimenting with several flavours of temporal logics which allow to take into consideration both the state oriented and the event oriented aspects of a system together with distribution and mobility aspects This experimentation is carried out through the actual development of a new verification tool UMC specifically tailored to the aims of the project The immediate purpose of the project is definitively not that one of building a commercial verification product e g targeting the verification of systems with a very large number of states even if the gained experience might certainly be useful for possible future extensions moving also in this direction So far the emphasis of the prototype development has been concentrated on the investigation of the desirable supported features and not yet on the quantatitive optimizations of them in terms of complexity memory resources performance
14. explicit 8 gt 260068660 parameter selects whether or not we want to label with tau the system evolutions without observable events when drawing the evolutions tree with the map command Getting help A brief summary of the available commands is visualized by issuing the help command or mo Exiting Finally the main umc loop is exited and the execution of umc abandoned by issuing the exit command or simply typing a dot Command line options Some of the already seen parameters of UMC can be set directly from the input command line and additional options are also available in this way The s parameter disables the automatic attempt to evaluate a formula with double Its_delpth limit if the previous bound is found insufficient A number given on the command line establishes the current initial Its depth limit as specified If a file name with the uctl suffix is present in the input command line then that file is supposed to contain the logic formula to be evaluated and the model checking is performed immediately and in a non interactive way E g umc model umc formula uctl s 100000 The model in file model umc is loaded and the formula in formula uctl is model checked starting with a maximum initial Its_depth of 100000 and without doubling the limit but reporting the failure if that limit is insufficient 27 4 2 Web interface The Web interface to umc is much more
15. parameters are constituted by a Select button through which we can select one of the predefined BLACK_BOX GRAY BOX WHITE BOX SELECTIVE INTERACTIVE CUSTOM observation modes and by a text area inside which we 34 can specify in the case of SELECTIVE INTERACTIVE CUSTOM observation modes further information identifying the objects the events and the attributes to which we are interested A picture representing the currently active Observation Mode is also shown on the left frame of the tool which if clicked over allows to observe of configure the preferences of the tool in the same way Preferences co v1 v2 v3 S1 52 53 54 0p1 0p2 0p3 print Signals step Observation Mode gt 51 step 0 s1 gt 52 O f 1 step Show Loss of Events as Error Signals Observe return events of observed calls Max Explanations depth in a single page Max Evolutions depth in a single picture Show Parameters of Events Show Target of Events Mark labels of evolutions without actions with tau Show evolving object in evolution label Initial Max Evaluation Depth Change Cancel 5 How UMC works The UMC structure is constituted essentially by 7 main modules Two modules are constituted by the parser of the UMC textual model description format and by the parser of the mu UCTL logic formulae Then we have two archiving modules a module implementing a database of explored system configurations and a module
16. queue of the object The keyword ASSERT can be omitted Boolean logical operators Logic formulas can be composed with the usual boolean operators which have the classical meaning The not operator has precedence over the others and or implies relational operators Since no specific binding priority between the relational operators is defined the boolean composition of formulas should not be ambiguous and parenthesis should be explicitly used to disambiguate when needed can be used as a shortcut for or 8 can be used as a shortcut for ana 7 can be used as a shortcut for not lt can be used as 8 shortcut for implies Basic mu calculus The basic mu calculus temporal operators are the box and diamond operators and the max and min fix point operators Diamond lt gt The diamond operator lt action expr gt SUBFORMULA allows to specify that a certain subformula should be true in at least one nextstate reachable in one step from the current state If an action expr is specified the nextstate should be reachable with a one step system evolution which satisfies the action expr 14 Box The box operator action expr SUBFORMULA allows to specify that a certain subformula should be true in all the nextstates reachable in one step from the current state if any If the current state has no successors the diamond is still satisfied If an action expr i
17. the path from 81 to s2p s1 included s2p excluded Formulal holds AL Formulal act1 U act2 Formula2 is equivalent to the fix point formula min Z Formulal and not FINAL and act2 and not tau and not actl Formula2 and actl or tau and not act2 Z and actl or tau and act2 Formula2 or Z and not actl and not act2 and not tau false So far the above are the only currently supported flavours of until operators Further flavours are sometimes used in other logics as for example versions of weak until or the release operator which is the dual of the normal until Weak Diamond lt lt act gt gt The formula lt lt act gt gt Formula holds in a state s1 if and only if Formula holds in s1 or in one of the states reachable in one or more steps from 81 performing only internal actions satisfying tau or actions satisfying act act is not allowed to contain tau as subexpression Notice that in the original ACTL the syntax of this temporal operator was lt act gt Formula now used for the basic mu calculus diamond operator From this point of view this operations constitutes a backword incompatibility between UMC and the original ACTL 20 Weak Box act The formula act Formula holds in state s1 if the formula Formula holds in all the states if any reachable from 81 performing an evolution whose label satisfies act possibly after a f
18. var is a free unused identifier for the loop index min and max are integer expressions and loop body is a sequence of statements Inside the loop body the loop index cannot be target of assignments Inside the loop body can appear exit statements Other syntactic issues In the current prototype type checking and many static analysis checks are not fully performed 1 6 the input specification is supposed to be mostly correct This is due partly to the fact that the UMC modelling language is not seen as the primary design tool a user should use but rather an intermediate language into which XMI models or other models are translated However in the absence of this higher lever translation phase some effort has been made in improving the direct usability of the UMC textual modelling language and this includes a limited form of static checking In the definition of the UMC textual modelling language we have preferred not to associate it with a rigid syntactic structure but to allow a great level of flexibility in order to simplify the possible translations and let the users to preserve as far as possible the concrete syntax to which they are used This is particularly true for example for the action language where we have tried not to adopt a fixed schema derived from the C language the JAVA language or any other specific language Several syntactic alternatives are therefore allowed Line comments can be introduced by prefixing them with
19. 3 23 35 37 40 41 42 UMC 3 3 User Guide Franco Mazzanti ISTI Technical Report 2006 TR 33 September 2006 Istituto di Scienza e Tecnologie dell Informazione Alessandro Faedo ISTI CNR Via A Moruzzi 1 56124 Pisa Italy franco mazzanti isti cnr it Abstract In this report we present the prototypical UMC verification tool under development at ISTI UMC accept a system specification given in UML like style as a collection of active objects modelled by state machines and whose behavior is described through statecharts On such systems UMC allows to verify properties specified in the mu UCTL logic a temporal logic which enriches the full mu calculus with the more abstract and weak CTL ACTL like temporal operators and with a rich set of state propositions and ACTL action expressions Both the basic command line oriented tool umc and its more user friendly web based interface are presented This web interface integrates also verification functionalities provided by the other environments EST FC2TOOLS which allow system abstraction and minimization Table of Contents 1 Introduction 2 The structure and semantics of UMC models 3 The structure and semantics of UCTL logics 4 The UMC tool and how to use it 5 How UMC works 6 The Airport example 7 Related Works and Conclusions 8 Known limitations availability acknowledgements 9 References 1 Introduction The goal of the UMC project 26 27 is to experiment in several
20. UT 16 28 project In this case an UML execution engine has been developed adopting the Open Caesar standard interface of the CADP environment In this way all the CADP 8 verifications tools including the on the fly Evaluator tool 24 can be applied also to this new engine As far as we now FMC and UMC are the only on the fly tools supporting full m calculus SPIN uses LTL CADP Evaluator the alternation free m calculus The fact of being able to state and check also structural properties of system configurations state attributes and predicates and not just events opens the door to the modelling and verification of several structural properties of parallel systems like topologic issues state invariants and mobility issues 40 8 Known limitations availability acknowledgements UML Issues UMC does not currently support all the features of UML1 4 state machines In particular UMC suffers the following limitations Events Only asynchronous signals and call operations are supported Time events are not supported States Internal transitions Enter Exit Do activities are not supported History states Sync states Choice pseudo states are not supported Transitions Initial default transitions do not have actions static and dynamic choice transitions are not supported Completion transitions cannot appear in more than one region of concurrent state Other Sub machines are not supported Some of the missing f
21. and only if Formula2 holds in 81 or if for all paths p starting from 81 Formula2 holds in a state s2p reachable in one or more steps from s1 performing only unobservable actions satisfying tau or actions satisfying act and Formula1 holds in all the intermediate states along the path from s1 to 920 s1 included S2p excluded AL Formulal U Formula2 is equivalent to the fix point formula min 2 Formula2 or Formulal and AX act or tau 2 The formula E Formulal actl U act2 Formula2 holds ina state s1 if exists at least one path p starting from 51 made by a possibly empty sequence of unobservable evolutions satisfying tau or evolutions whose label satisfies act1 followed by a conclusive evolution whose label satisfies act2 which leads to a state S2p in which holds Formula2 and in all the intermediate states along the path from sl to s2p s1 included s2p excluded Formulal holds E Formulal act U act2 Formula2 is equivalent to the fix point formula min Z Formulal and lt act2 gt Formula2 or gt 80 1 or tau gt Z The formula A Formulal actl U act2 Formula2 holds ina state 81 if and only if all paths p starting from 51 are made by a possibly empty sequence of unobservable evolutions satisfying tau or evolutions whose label satisfies act1 followed by a conclusive evolution whose label satisfies act2 which leads to a state S2p in which holds Formula2 and in all the intermediate states along
22. arget object the calling of a synchronous call operation on a target object an assignment of a synchronous function call to a local or transition variable the declaration of a temporary variable the exit from a loop or the return from an operation call A signal is similar to an event declaration but its arguments are constituted by value expressions instead that by formal parameters A signal is preceded by a target specification the meaning is that the signal is sent to the events queue of the specified destination object The action of sending a signal or calling an operation specifies the target object the term self can be used to denote the sending object itself if no destination is specified then self is implicitly assumed the signal being sent and possibly the list of actual parameters A temporary transition variable declaration can appear inside an action sequence with its scope extending till the end of the sequence A transition variable declaration is similar to a local attribute declaration but does not allow an explicit initialization A composite action can be a conditional statement or a loop statement A conditional statement has the form if condition then then part if condition then then part else else part where condition if a boolean expression and then part and else part are sequences of actions A loop has the form for var in min max loop body where
23. ass is used to describe the dynamic behaviour of the corresponding objects A state machine with its events queue is associated to each active object of the system Non active objects play the role of interfaces towards the outside of the system and can only be the target of signals A system is constituted by fixed static set of objects so far no dynamic object creation and a system is an input closed system i e the input source is modelled as an active object interacting with the rest of the system There is a predefined non active out Class and a predefined out object which can be used to model the sending of signals to the outside of the system and there is a predefined non active ERR Class and a predefined ERR object which can be used to model the notification or error signals to the outside of the system further non active classes and objects can be defined by defining classes without statechart At least one active object must be defined and the declaration of an object must appear after the declaration of the class to which it belongs In the following section we describe in more detail the two syntactic model components namely classes and objects in the subsequent one we describe an overview of their semantics Classes and Objects The behaviour of a the set of objects belonging to a class is defined by a statechart diagram associated with the class itself In particular the definition of a class statechart consi
24. coded as max Z lt b gt Z There is a reachable livelock i e a loop of tau evolutions somewhere The above can be encoded as EF max Y lt tau gt Y For all paths in which event a never occurs eventually the predicate P will hold The above can be encoded as min Z P or not final and not a Z There exist a path such that an evolution which satisfies the action expression a occurs infinitely often The above can be encoded as max 2 min W lt a gt 2 or lt not a gt W There exist a path such that the state predicate p is satisfied infinitely often by its states sequence The above can be encoded as max Z min W p and lt gt Z or not p and lt gt W There exist a path from certain point of which the state predicate p holds infinitely often and state predicate q does no longer hold The above can be encoded as EF max zZ min W p and not q and lt gt Z or not p and not q and lt gt W For all paths if an evolution which satisfies the action expression a is possible an infinite number of times then an evolution which satisfies a is done an infinite number of times 05 ww i e does not exist a path such that from e certain point a is not done anymore but nevertheless 6 7 is infinitely possible The above can be encoded as not EF max zZ min W lt a gt true and lt not a gt Z or not lt a gt true an
25. complex and rich of features since it exploits several other packages and tools developed as part of the project or available from the net Among these externally developed tools we must mention the Graphviz package for the generation of ps svg and jpg images the Ghostview package for the translations of ps info pdf the Fc2tools and EST package for the minimization of automata according to some equivalences Tcl Tk Other internally developed tools are the xmi2umc package for the extraction of umc classes from an XMI model description of an UML system the umc2tab and tofc2 totdot tools for the translation of a finite UMC model into specifically formatted finite LTS usable by other tools wi ISTITUTO DI SCIENZA E TECNOLOGIE Pyama METHODS amp amp TOOLS DELUINFORMAZIONE A FAEDO LABORATORY Welcome to UMC Documentation The Structure of UMC Models The Structure of UMC Logics Requirements HTML4 0 browser with javascript DHTML and SVG support e g MacOS X Mozilla Firefox 1 0 Safari Internet Explorer with SVG3 Windows Internet Explorer SVG3 or Mozilla Firefox SVG6 Linux OS not tested Mozilla Firefox 1 0 SVG3 properly configured should be OK Solaris OS not tested not able to build appropriate browser Links SVG3 and its Linux installation notes SVG6 and its Windows installation notes original Firefox and more Firefox ports Author Franco Mazzanti _http fmt isti cnr it mazzanti Credi
26. ct should receive only events defined in its class interface if such spurious undeclared events are sent they will be discarded when dispatched Private Attributes The attributes local variables defined for the objects of a class are defined in the Vars section of a class They can be explicitly typed and they can be provided with an initial static value If no explicit initial value is specified the default value for the type is used WAPI type itera Statechart Structure The statechart structure of a class is given by defining the nested structure of the states and the set of transitions which connects them The nested structure of the states is defined by a sequence of composite state definitions which starts from the definition of the top level state The definition of outer states must precede the definition of its nested substates The top level state of a statechart must be a composite sequential state A composite sequential state is defined by a list of substates which can be composite sequential states composite parallel states or simple states The name initial denotes the default initial pseudostate of a composite sequential state and must appear as first substate if no initial pseudostate is explicitly provided the first substate of the sequence is implicitly assumed as default initial substate For any simple state appearing in the definition of a composite sequential state it is not necessa
27. d lt not a gt Action Expressions Basic Action Expressions The basic form of action expression is the true or false predicate or a basic action predicate about the actions performed by the system evolution In particular The action expression true is satisfied by all system evolutions The action expression false is not satisfied by any system evolution The action expression obj is satisfied by any system evolution in which object obj is the one which evolves 16 The actions expression targetobj event_id is satisfied only by system evolution which generate the event event_id and send it to the object 582865002 The action expression event_id is satisfied only by those system evolutions which do generate an event event_id possibly with some parameters notice that event_id might be just one of the events generated by the evolution The actions expression event_id args is satisfied only by system evolution which generate the event event_id event_id with the specified args where args is a comma separated sequence of static values or E g the action expression callop 3 is satisfied by all evolution in which the signal or operation callop which has two parameters is being executed and in with the second argument of the event has value 3 Examplel1 The actions expression sourceobj targetobj event_id args 18 satisfied only by system evolutions which object
28. e state space as it may happen for UML state machines Indeed a problem of the above evaluation schema is that in case of infinite state machines it might fail to produce a result even for some cases in which a result might be produced in a finite number of steps This is a consequence of the depth first recursive structure of algorithm The solution taken to solve this problem consists in adopting a bounded model checking approach 2 1 6 the evaluation is started assuming a certain value as maximum depth limit of the evaluation In this case if a result of the evaluation a formula is given inside the requested depth then the result holds for the whole system otherwise the depth limit is increased and the evaluation restarted This approach initially introduced in UMC to overcome the problem of infinite state machines happens to be quite useful also for another reason Setting a small initial depth limit and a small automatic increment of it at each re evaluation failure when we finally find a result we can have a reasonable almost minimal explanation for it and this could be very useful also in the case of finite states machines 36 The web interface The web interface is an additional layer constructed over the basic umc tool It is constituted by a set of cgi scripts which are called whenever an umc operation is requested and which allow to subsequently check whether the requested operations is completed The client side part of
29. eatures might be added in future versions of UMC We do not see any intrinsic difficulty in modelling also the currently omitted aspects even if for the purposes of the umc project their support is probably not essential UMC Issues Performance is definitely not a target for the current version of the tool We are currently more interested in experimenting with user friendliness and easiness of verification Many strong optimizations could be done Availability The UMC basic tool is constituted by a single program written in Ada and its binary code easily portable and compilable for many platforms is freely available For source code distribution please contact the author The WWW interface is currently accessible from http matrix isti cnr it FMT Tools there is no guarantee that it will remain accessible in the future At the present time some work is still needed in order to make it easily portable to other systems Acknowledgements The XMItoUMC translation has been developed in tcl tk by Marco Fabbri The airport example has been developed in the context of the AGILE project Useful feedback and suggestions have come also from the QUACK and PRIDE projects and from many colleagues among which Stefania Gnesi Sandro Fantechi Diego Latella and Mieke Massink Parts of this report have been extracted from 10 3 AGILE project IST 2001 32747 by the proactive Initiative on Global Computing 4 QUACK A Platform for the Quality of Ne
30. el This property can be written in mu ACTL as AG EX eating Travelerl true lt ASSERT Travelerl atLoc Planel amp ASSERT Planel atLoc null1 7 Related Works and Conclusions Linear time model checking of UML Statechart Diagrams is addressed in 19 10 and 24 In 11 a simple branching time model checking approach to the formal verification of UML Statechart Diagrams was presented exploiting the classical model checking facilities provided by the AMC model checker available in JACK We are currently aware of three available tools for model checking UML systems described as sets of communicating state machines HUGO 22 26 and vUML 22 take the approach of translating the model into the Promela language using SPIN 15 as the underlying verification engine We have not had direct experience with these tools but clearly in this case the properties to be verified need to be mapped into LTL logic While vVUML is restricted to deadlock checking HUGO is mainly intended to verify whether certain specified collaborations are indeed feasible for a set of UML state machines In both cases the UML coverage of the tools is wider than ours because it includes UML call operations history states and internal state activities A timed version of HUGO called HUGO RT 17 has also been developed which maps into the UPPAAL verification engine instead than into SPIN A third interesting approach is that one adopted in the ongoing UMLA
31. enerated when the activity of a state is terminated and that these completion events have precedence over the other events possibly already enqueued in the object events queue The set of possible evolutions of an initial model are in general not finite In fact even if we consider only limited integer types which is a reasonable assumption we can still have infinitely growing queues of events The following is an example of very simple model presenting an infinite behaviour Chart Main is Signals a State Top sl Transitions sl a self a self a lt 1 end When coming to give a formal framework to the above informal description of a run to completion step and when coming to model the parallel evolution of state machines some aspects which are not precisely and univoquely defined by the UML standard often intentionally have to be in some way fixed With respect to this UMC makes certain assumptions which even if compatible with the UML standard are not necessarily the only possible choice 1 Atomicity of transition effects w r t internal object concurrency The whole sequence of actions constituting the actions part of statechart transition is supposed to be executed with respect to the other concurrent transitions of the same object as an indivisible atomic activity 1 6 two parallel statechart transitions fireable together in the current state machine configuration cannot interfere one with the other but the
32. eration call If more than one return statements are executed by the run to completion step triggered by a call the last return event overrides the previous events this might eventually be an error syntactically and statically checked If no return statement is executed by the run to completion step triggered by a call then no return event is generated and the caller remains suspended until a return signal is eventually received 7 Parallel completions events In our model we suppose that all completion events generated by a run to completion step are dispatched all together in a unique step 3 The structure and semantics of UCTL logics The logics supported by UMC is essentially the full modal propositional mu calculus extended with higher level CTL ACTL like operators and structured action expressions Notice that if a system has an infinite number of states the termination of the evaluation of a formula is not guaranteed to succeed In fact if such evaluation requires the analysis of an infinite number of states the evaluation itself never terminates For example the formula AG predicate will certainly fail to return a value if the system is infinite while the other 1 This assumption is related to an ambiguity of the UML definition of priority of join transitions in which all the sources have the same depth In this cases the priority being defined as that of the deepest source leaves some open space to multiple interprations
33. etween the attributes variables of the source and target states names ending with They have the form lt target_var gt lt relop gt lt source_var_expr gt where lt relop gt is one of nen n ct 7 eo sr Examples are xt gt x objl x objl obj2 x 1 objl obj2 x objl y ACTL LIKE temporal operators Next EX AX ET AT The Exists Next operator EX action expr subformula holds in the current state if and only if there exists a transition from the current state whose label satisfies the action predicate which leads to state in which the subformula holds It is exactly equivalent to the basic diamond operator lt action expr gt SUBFORMULA The Always Next operator Ax action expr subformula holds in the current state if and only if all the transitions which exit from the current state have a label which satisfies the action predicate and lead to state in which subformula holds Moreover the current state must not be final 1 e at least a transition must exist AX action expr subformula is equivalent in basic mu calculus to lt action expr gt true and not lt action expr gt not subformula and not lt not action expr gt true ET subformula is equivalent to EX tau subformula AT subformula is equivalent to AX tau subformula EX subformula is equivalent to EX true subformula AX subformula is equivalent to true subfor
34. g parameters affects the visualization of graphic output in dot format representing the system evolutions tree In particular The max_explanation_depth parameter constrains the maximal depth of the explanations steps visualized in consequence of a why or mapwhy command 26 The max_evolutions_ depth parameter constrains the maximal depth of the evolution steps visualized in consequence of a trace command without arguments or by the map command The showstuttering parameter defines whether or not to make visible stuttering transitions by adding fake ERR lostevent signal in stuttering transitions absence of stuttering is usually an interesting property of the system The showparams parameter selects whether or not the current value of the parameters of signals and calls are actually to be displayed in the evolutions tree generated by the map command The showtarget parameter selects whether or not we want to display the target object in signal and operations call when drawing the evolutions tree with the map command The observereturns parameter selects whether or not we want to draw the return signals generated when an operation call completes when drawing the evolutions tree with the map command The showevolvingobject parameter selects whether or not we want to visualize the name of the evolving object inside the system evolutions when drawing the evolutions tree with the map command The
35. h IEEE International High Assurance Systems Engineering Symposium pages 46 55 IEEE Computer Society Press 1999 S Gnesi and F Mazzanti On the Fly Verification of Networks of Automata International Conference on Parallel and Distributed Processing Techniques and Applications PDPTA 99 S Gnesi and F Mazzanti On the Fly model checkling of communicating UML State Machines submitted for publication M Hennessy R Milner Algebraic Laws for Nondeterminism and Concurrency JACM 32 137 161 1985 G J Holzmann The SPIN Model Checer IEEE TSE 23 1997 pp 279 295 W M Ho and Le Guennec A Pennaneac h F J z quel J M Umlaut an extendible UML transformation framework INRIA RR 3775 1999 http www inria fr RRRT RR 3775 html A Knapp S Merz and C Rauh Model Checking Timed UML State Machines and Collaborations FTRTFT 2002 7th International Symposium on Formal Techniques in Real Time and Fault Tolerant Systems Springer LNCS to appear 2002 D Kozen Results on the Propositional m calculus Theoretical Computer Science 27 333 354 1983 Jacobson I Booch G Rumbaugh J The Unified Modeling Language Reference Manual Addison Wesley 1999 1 2 10 11 12 13 14 15 16 gt PRIDE ambiente di PRogettazione Integrato per sistemi DEpendable Italian Space Agency 2002 42 D Latella I Majzik and M Massink Automatic verification of 1111 diagrams using the SPIN model chec
36. he fix point formula min Z Formula and AX Z Until The formula E Formulal U Formula2 holds in a state sl if and only if Formula2 holds in 51 or if Formula2 holds in a state s2 reachable in one or more steps from 51 and Formulal holds in all the intermediate states along the path from 81 to s2 s1 included s2 excluded E Formulal U Formula2 is equivalent to the fix point formula min Z Formula2 or Formulal and gt lt 2 The formula Formulal U Formula2 holds in a state 81 if and only if Formula2 holds in s1 or if for all paths p starting from s1 Formula2 holds in a state S2p reachable in one or more steps from 81 and Formula holds in all the intermediate states along the path from 51 to S2p s1 included S2p excluded Formulal U Formula2 is equivalent to the fix point formula min 2 Formula2 or Formulal and AX 2 The formula E Formulal act U Formula2 holds in a state sl if and only if Formula2 holds in 51 or if Formula2 holds in a state s2 reachable in one or more steps from 81 performing only unobservable actions satisfying tau or actions satisfying act and Formulal holds in all the intermediate states along the path from 81 to s2 s1 included 2 excluded E Formulal act U Formula2 is equivalent to the fix point formula min 2 Formula2 or Formulal and lt act or tau gt 2 19 The formula A Formulal act U Formula2 holds in a state sl if
37. implementing a database of started completed in progress aborted computations of logic formulae at configurations Moreover we have a module which abstracts from the internal details of system configurations providing abstract iterations routines over the possible evolutions from a configuration into the next reachable configurations This abstract iteration module is used by two other modules a logic module which implements the on the fly verification algorithm for mu UCTL and an exploration module which is support the interactive exploration of the system evolutions Our approach to the on the fly model checking of a mu UCTL logic formula has been initially presented in 13 In that case the system to be verified was defined by a network of synchronised agents working in parallel The model checker named FMC was included in Jack 4 an environment based on the use of process algebras automata and temporal logic formalisms supporting many phases of the system development process The model checker 35 presented here UMC is based on the same ideas of FMC but working over a set of communicating i e exchanging signals UML State machines Even though the code for both tools FMC and UMC has been almost completely rewritten several times the underlying logic schema has remained the same The basic idea behind FMC and UMC is that given a system state the validity of a formula on that state can be evaluated analysing the transit
38. ined by an or operator boolexprl and boolexpr2 and A vector expression is constituted by list of comma separated items enclosed by brackets Tobjl obj2 ob3j3 The allowed operations over vector values are the selection of an item of the vector vector index where index ranges from 0 to vectorsize 1 the selection of the first element of the vector vector head equivalent to vector 0 the selection of the rest of the vector once the first element has been skipped vector tail the evaluation of the vector length vector length which is an integer value the concatenation of two vectors vectorl vector2 Identifiers are case sensitive and built over letters digits and _ underscores Erroneous selection operations on incorrectly sized vectors indexing head just return a default value for the type Signals and Operations The events handled by the class are distinguished between asynchronous signals and synchronous call operations they are correspondingly declared in the Signals and Operations sections of a class Call operations can also have a return type which is one the predefined types Signals _Sig id Params _ signals Operations Popa Params returntype operations Parameters of events can be explicitly typed and they do have only an implicit in mode It is not statically enforced checked the fact that an obje
39. inite sequence of unobservable evolutions satisfying tau act is not allowed to contain tau as subexpression act Formula can be translated as max Z EX tau Z amp EX act Formula and is equivalent to lt act gt Formula Notice that in the original ACTL the syntax of this temporal operator was act Formula now used for the basic mu calculus box operator From this point of view this operations constitutes a backword incompatibility between UMC and the original ACTL The UCTL Grammar item denotes 0 or more occurrences of the item item denotes 0 or 1 occurrence of the item item denotes a terminal character sequence item item denotes indicates alternative items umc formulas FORM state predicate and sequence or sequence negation implication basic mu formula actl like formula state predicates state predicate true false simple expr Me uo hat fs lt a 4a simple expr simple expr basic expr basic expr basic expr basic expr obj Jattr attr value boolean logical operators and sequence FORM and FORM and FORM or sequence FORM or FORM or FORM negation not FORM implication FORM lt FORM 21 a FORM 02 basic mu calculus minfix mu box mu diamond fixid max VARID FORM
40. ions allowed in that state and analysing the validity of some sub formula in only some of the next reachable states in a recursive way as shown by the following schema Env represents the current context in which a given formula is evaluated which gives a precise meaning in terms of already started computations to the free variables of the formula Evaluate F Formula Env Environment S State is if we have already done this evaluation and the result is available then return the already known result elsif we are already trying to evaluate F in S with Env then return true or false depending on maximum or minimum fixed point semantics else Keep track of the fact that we are trying to evaluate F in S with Env e g push the pair F S in a stack for each sub formula F and next state S which needs to be evaluated loop call recursively Evaluate F Env S if the result of Evaluate F Env S is sufficient to establish the result of evaluate F Env S then exit from the loop end if end loop at this point we have in any case a final result Keep track of the fact that we are no longer trying to evaluate F in 5 with Env Possibly keep track of the performed evaluation and result return the final result end if end Evaluate This approach seems promising when applied to UML state machines or groups of communicating state machines because it can easily be extended also to the case of potentially infinit
41. ker Technical Report CNUCE B4 1999 008 Consiglio Nazionale delle Ricerche Istituto CNUCE 1999 D Latella I Majzik and M Massink Towards a formal operational semantics of UML statechart diagrams IFIP TC6 WG6 1 FMOODS 99 pages 331 347 Kluwer Academic Publishers 1999 J Lilus I Porres Paltor VUML a Tool for Verifying UML Models 14th IEEE International Conference on Automated Software Engineering ASE 99 pp 255 258 1999 http www pst informatik uni muenchen de projekte hugo R Mateescu M Sighireanu Efficient On the fly Model Checking for regular Alternation Free m Calculus Science of Computer Programming 46 3 2003 OMG Unified Modeling Language Specification Version 1 4 beta R1 November 2000 http www omg org technology documents formal uml htm T Sch fer A Knapp and S Merz Model Checking UML State Machines and Collaborations Proc Wsh Software Model Checking 55 3 Electronic Notes in Theoretical Computer Science Paris 2001 UML All pUrposes Transformer http www irisa fr pampa UMLAUT R Wieringa and J Broersen A minimal transition system semantics for lightweight class and behavioral diagrams ICSE 98 Workshop on Precise Semantics for Software Modeling Techniques 1998 S Gnesi F Mazzanti A Model Checking Verification Environment for UML Statecharts XLIII Congresso Annuale AICA Udine 5 7 Ottobre 2005 S Gnesi F Mazzanti On the fly model checking of communicating UML State Machines Seco
42. l OBJECT QUEUE CURRENT TRIGGER CURRENT VARIABLES ACTIVE STATES Top sl FIREABLE TRANSITIONS 1 Current Configuration Cl Possible Evolutions 1 a gt C2 1 lt explore gt 1 Current Configuration C2 Possible Evolutions 1 OUT lostevent a gt C3 lt explore gt b Current Configuration Cl Possible Evolutions 1 a gt C2 1 lt explore gt Moving to another_specific configuration The initial configuration of the system has name C1 as the exploration of the system evolutions proceeds new configurations are discovered on the fly and named C2 C3 and so on Notice that the name of the configuration depends from the order in which the system evolutions are explored and different names can be given to the same actual configurations in different run of the tools if the system configurations are explored in a different order The initial command set the initial configuration 1 6 C1 as the current configuration 25 The moveto Ci command set Ci as current configuration if such a configuration has indeed been generated trace 2 C1l MyModel 8 lt C2 1 C2 MyModel OUT lostevent a gt C3 moveto 2 Current Configuration C2 initial Current Configuration Cl Viewing and adjusting some tool preferences and parameters The behaviour of the umc tool can be customized according to some parameters The set command allows to obse
43. model umc Enter an ACTL formula or a command or exit with Verifying a Formula If a logic formula is inserted it must fit a single line it is immediately evaluated and further input is awaited remember that the evaluation might diverge in the case of infinite state systems 23 EF ET true reprinted formula Starting Evaluation with LTS Bound set to 1024 The formula is FALSE Looking at_the explanations of the result Once a logic formula has been evaluated we can ask for an explanation of how the result has been deduced which results in the printing of all the deduction steps leading to the result This is achieved with the why command Alternatively the tabwhy command saves in the current directory a file explanation tab containing an example counterexample for the validity of the formula the formula EF ET true is FOUND_FALSE in State Cl because The formula ET true is FOUND_FALSE in State Cl tabwhy Explanation Model generated Browsing into the current configuration detail The info command allows to observe the internal details of the current configuration These details include for each active object of the model the name of the object the status of its event queue the status of its variables the current trigger if any the set of currently active states and the set of the currently fireable transitions info CURRENT CONFIGURATION Cl OBJECT
44. mula Beware in the original ACTL definition the action expression true in the context of the Next operators had the meaning of any observable event while here it has the meaning of any event either observable or not Eventually alias Future 18 The formula EF Formula holds in a state s1 if and only if Formula holds in s1 or in one of the states reachable in one or more steps from s1 The formula AF Formula holds in a state s1 if and only if Formula holds in s1 or in one of the states reachable in one or more steps from s1 for all the possible paths starting from s1 EF Formula is equivalent to its dual not AG not Formula and is equivalent to the fix point formula min 2 Formula or gt lt 2 not EG not Formula and is equivalent to the min 2 Formula or AX 2 AF Formula is equivalent to its dual fix point formula Globall The formula EG Formula holds in a state s1 if and only if Formula holds in s1 and in all the states reachable in one or more steps from s1 along at least one path starting from s1 The formula AG Formula holds in a state s1 if and only if Formula holds in s1 for all the states reachable in one or more steps from 81 along any path EG Formula is equivalent to its dual not AF not Formula and is equivalent to the fix point formula min 2 Formula and gt lt zZ AG Formula is equivalent to its dual EF Formula and is equivalent to t
45. n 11 6 Dealing with serialisation For each subset identified at the previous step if the subset contains more than one transition we generate the set of all the possible sequences of transitions deriving from all the possible serialisations of the transitions in the subset Each such sequence of transitions defines a possible evolution of the given machine configuration f Computing the target configuration The next state machine configuration resulting after this evolution if obtained by removing the dispatched event if any from state machine event queue modifying the values of the state machine variables as specified by the sequence of sequences of actions as requested by the firing transitions modifying the events queue of the state machine by adding the signals specified by the sequence of sequences of actions in their order The above steps defines the possible effects of starting a run to completion step Once such a step is started it can atomically complete with the execution of all the involved actions or become suspended over some synchronous call operation In this second case the local variables of the object are updated and the generated events delivered to the system just before the evolving object becomes suspended on the call operation The run to completion step will be eventually resumed when a return signal is received from the called object Notice also that implicit completion events are g
46. nd ACIS International Conference on Software Engineering Research Management and Applications SERA2004 Los Angeles USA 5 7 May 2004 43 17 18 19 20 21 22 23 24 25 26 27
47. path Statepath top Name Name Trigger EventName ParamName ParamName Guard BoolBoolExpr Actions Stm Stm Object Object ObjName ClassName Initializations Initializations AttrName gt StaticExpr AttrName gt StaticExpr action statements Stm Assignment SignalSending OperationCall FunctionCall Conditionalstm Loopstm VarDecl Returnstm ExitStm Assignment TargetExpr Expr SignalSending ObjExpr SignalName Expr Expr OperationCall ObjExpr OpName Expr Expr FunctionCall TargetVar ObjExpr OpName Expr Expr ConditionalStm if BoolBoolExpr then Actions else Actions Loopstm for LoopIndex in IntExpr IntExpr Actions VarDecl VarName TypeName ReturnStm return Expr Expr ExitStm exit TargetExpr AttrName Selection VarName Selection Selection IntExpr names and expressions Expr Expr BoolBoolExpr IntExpr ObjExpr VectorExpr BoolBoolExpr BoolExpr and BoolExpr BoolExpr or BoolExpr not BoolExpr BoolExpr BoolExpr true false AttrName Selection VarName Selection Expr Expr Expr Expr IntExpr relop IntExpr 10 ObjExpr
48. re History Deep History Synch states state Entry Exit Do activities Dynamic Choice Static Choice transitions Change and Time events None of the above limitations is intrinsic to the tool and further versions of the prototype are likely to overcome them The UMC Grammar item denotes 0 or more occurrences of the item item denotes 0 or 1 occurrence of the item item denotes a terminal character sequence item item denotes indicates alternative items Model Class Object Class class ClassName is Signals Signal Signal Operations Operation Operation Vars Attribute Attribute State top Composite State Statepath State Transitions Transition end ClassName Signal SignalName ParamName TypeName ParamName TypeName Operation OpName Name TypeName Name TypeName TypeName Attribute AttrName TypeName StaticExpr State Composite Parallel Composite StateName StateName Defers Defer Defer Parallel Name Name Defers Defer Defer StateName Name final initial Defer EventName ParamName ParamName Transition Statepaths Trigger Guard Actions gt Statepaths Statepaths Statepath Statepath State
49. ree of observability of the generated model events In particular When the white_box observation mode is selected all events are considered observable these are all change event caused by assignments all signals all operations all returns When the gray observation mode is selected are considered observable only signals and operation calls but not the change events caused by assignments When the black_box observation mode is selected are considered observable only the signals this includes all OUT and ERR signals sent by the system to the outside i e all signals not targeted to another active object of the model When the custom observation mode is selected the user is required to explicitly list the events and the object attributes of interest thus making observable only certain assignments signals and operation calls 17 When the selective observation mode is selected the user is required to explicitly list the objects of interest thus making observable only the signals and operation calls received and generated by them and the assignments made by them When the interactions observation mode is selected the user is required to explicitly list the objects of interest thus making observable only the signals and operation calls exchanged between any two objects of the list Evolution predicates Evolution predicates are a form of action expression which describes a relation b
50. rve the current status of them or change their value set initial_lts_depth 0 max_explanation_depth 100 max_evolutions_depth 10 showparams TRUE showtarget TRUE showstuttering TRUE observereturns FALSE observationmode GRAY_BOX showevolvingobject TRUE explicit_tau_requested FALSE The initial_lts_depth parameter affects the way in which the on the fly evaluation of a formula proceeds In particular it sets the initial depth limit at which a depth first subcomputation should be truncated in favour of other less deep subcomputations If no answer about the validity of a formula can be given with the current Its_depth limit the evaluation is restarted with a doubled Its_dept limit The observationmode parameters allow to define the user policy in terms of observability of events set observationmode BLACK 80 only outgoing signals are observed set observationmode GRAY BOX all signal and operation events observed set observationmode WHITE Box all signal operations and assignments observed set observationmode SELECTIVE obj1 0bj2 0bj3 all events involving any of given objects including local assignments are observed set observationmode INTERACTIVE 0bj1 0bj2 0jb3 all signals and operations exchanged between any two given objects are observed set observationmode CUSTOM 0bj1 x op obj3 y sig the evolutions of the given object attributes and the exchanges of the given signals and operations are observed The remainin
51. ry to give any further explicit definition A composite parallel state is defined as a parallel composition of several composite sequential substates also called regions of the parallel state For each region must subsequently be given an explicitly definition as a composite sequential state State SERENA 50008067 substates Defers State State id Region Region _ regions Defers A composite state definition can also define the set of events deferred while active A Defers clause defines the list of events matching the profile as declared in the Signals or Operations sections of the class to de deferred Defers Biga Params defers The set of transitions of the class statechart is defined in the Transitions section of the class The definition of a transition contains a set of source states a trigger an optional guard an optional list of actions and a set of target states Transitions Actions part _ Aros Each state of the source or target is identified by its composite_name which is a path at most starting from the top state which univoquely identifies the state A transition with more than one source is called a join transition In the case of joins transitions the first state in the source list is required to be the most transitively nested source state In this sense the first state univoquely determinates the priority of the transition
52. s specified the subformula should be true in all the nextstates reachable with a one step system evolution which satisfies the action expr if any such nextstates exist action expr SUBFORMULA 1S equivalent to not lt action expr gt not SUBFORMULA Max and Min FixPoints The power of mu calculus is achieved through the two fixed point operators max and min The fixedpoint identifier can only appear inside the fixedpoint body of the formula In state s the formula max Z FixedPointBody z is true if and only if the following infinite formula is true in s FixedPointBody true and FixedPointBody FixedPointBody true and FixedPointBody FixedPointBody FixedPointBody true and and In state s the formula min 2 FixedPointBody z is true if and only if the following infinite formula is true is s FixedPointBody false or FixedPointBody FixedPointBody false or FixedPointBody FixedPointBody FixedPointBody false or sean OD For example the following formula max 2 lt a gt z holds ina state 81 if and only if there is a next state s2 reachable with an evolutions satisfying a in which z holds again i e if there exists an infinite path of evolutions satisfying a which starts from s1 Of the two fixpoint operators only one might be considered primitive as the other one can be derived from the first Le max Z FixpointBody Z is equivalent to not min Z not FixpointBody not 2 min 2 FixpointBody Z is equivalent to
53. s transition variables can be of one of the system predefined types These types are the basic int bool and obj types or a Class type denoted by a Classname or the corresponding vector version of them int bool and obj types or a Classname The default value for an integer variable is 0 for a boolean variable is false for an object is null for vectors is the empty vector Expressions and Identifiers An integer expression is either an integer literal the name of an integer attribute or parameter or a parenthesized integer expression a vector length expression a selection from an integer vector or an composite expression built over one of the integer operands 6 799 66 9499 1 mod An object expression is either self or this or null or the name of object attribute or parameter both self and this denote the executing object or a selection from an object vector A boolean expression is either the boolean literal true or false or name of a bool attribute a selection from an bool vector an equality comparison between two object or vector expressions obj _exprl obj_expr2 obj_exprl obj_expr2 a relational expression between two integer expression int_expr1 relop intexpr2 where relop is gt lt gt lt or a sequence of boolean expression all joined by an and operator or all jo
54. sourceobj generate a signal event_id with the specified args being sent to object denoted by targetobj Example2 The action expression event_id is satisfied by the system evolutions labeled with any of the following labels event_id event _id 3 target event_id targetlevent_id 0 first _event target event_id 1 2 3 other events Boolean Compositions of Action Expressions An action expression can be a boolean composition of other action expressions The action expression pred1 or pred2 is satisfied by the system evolutions which satisfy either pred1 or pred2 The action expression predl and pred2 is satisfied by the system evolutions which satisfy both pred1 or pred2 The action expression not pred1 is satisfied by the system evolutions which do not satisfy the action predicate pred1 Observable Events and Observation Modes The concept of observable event is touched when we either make use of the tau action expression or when the weak ACTL like logical operators are used box diamond until The action expression tau is satisfied only by the system evolutions which do not generate any observable event these include both system evolutions which do not generate any event at all and system evolutions which generate only events explicitly tagged as non observable by the user In fact the user has the choice to select a particular observation mode in which the UMC is run which affects the deg
55. stability As such the prototype in its current proof of concept status is good for education purposes and academic experimentations but definitely not ready for an official public release or for use in a real industrial environment The development of the tool builds over the experience obtained with the previous development of FMC see 13 another on the fly model checker for networks of automata specified in the 102 format or as a collection of regular CCS basic Lotos agents In our case the model under investigation is specified by a textual description of a set of UML statechart diagrams one for each class of objects which constitutes the system and by a set of objects instantiations The properties to be verified are specified as mu UCTL formulas a temporal logic with the power of full mu calculus which includes the high level composite operators typical of branching time action based logic ACTL 6 The reference dynamic semantics for UML statecharts is as far as possible corresponding to the official semantics as given in 26 as already formally described in 1 21 29 with some limitations 2 The structure and semantics of UMC models A complete UMC model description is given by providing by a set of class definitions and a set of object instantiations Class definitions represent a template for the set of active or non active objects of the system In the case of active objects a statechart diagram associated to cl
56. sts in the introduction of the class name the list of events which trigger the transitions of the objects of the class signals or call operations the list of private attributes variables local to the objects of the class the structure of the states of the class nodes of the class statechart diagram the transitions of the objects of the class edges of the class statechart diagram Class 7618885067 is Signals Operations Local Vars State top SUBSE Vsubstates _ Deters states Transitions x Trigger Args Guard Actions part gt Target end In the case of non active objects the corresponding class declarations can only define the list of accepted Signals and Operations no Local Vars States or Transitions can be introduced Once the needed classes are have their behavior defined by the appropriate statechart we can define the actual evolving system as a set of object instances Each object instance is declared by an object declaration which introduces the object name the name of its class and possibly any specific initial values for its attributes Object Obj ld 61855 6 Actualizations This initial values can be literals or names of other objects possibly also objects which will be declared later in the text Predefined Types The parameters in the interface profile of the events supported by a class signals and operations the class local variables and the clas
57. t attribute or a few kind of interactions among the objects In these cases the actual system transitions are likely to be constituted in the most part by tau transitions Directly observing the concrete transition tree would not allow to grasp the correctness of the system behaviour Observing instead a minimized version the system evolution graph may directly and intuitively reveal important correctness properties of the system The kind of minimization currently performed by UMC is the so called complete trace minimization and is achieved by making use of the EST toolset Also in this case the map is shown in SVG format in addition a JPG translation of the design can be requested the original textual code in the dot formal can be viewed and a representation of the Its in the tab format can be obtained We should note that abstract minimization of a system can only be achieved if the system is finite In fact the minimization algorithms are directly applied on an explicit representation of the all the system evolutions as a single automaton and the generation of this automaton will never terminate is the system is infinite Moreover the complexity of minimization is likely to be exponential in the case of full trace minimization and this tends to make minimizations practically unfeasable for systems of a finite but relevant size 32 Abstract Minimized Model Evolutions Chart Set the graphics frame dimension to
58. the interface the umc html page implements a connectionless kind of interaction with server asking for operations and subsequently cyclically rechecking whether that operation has been performed this approach is needed because in general a verification of a formula might require a long time which would trigger internal timeouts both from in the client browser and in the web server side The umc client html code makes use of several features dynamic html frames javascript and seems to works both on reasonably recent browsers like Netscape Navigator from version 4 7 up and with Internet Explorer 6 The Airport example Let as consider as a toy example a system constituted by two airports two passengers one at each airport and a plane The plane is supposed to carry exactly one passenger and flies if it has passengers between the two airports Departing passengers try to check in at the airport and than board the plane We contemplate only one observable action performed by the passengers during the flight namely the consumption of a meal The complete dynamic behaviour of the objects of classes Passenger Airport and Plane is shown below both in the form of statecharts diagrams and in the umc textual form eo gt created landing request P checkin D T P Janding_delayed y T checkin_closed f HANDLING lt 4 j HANDLING CHECKIN N pE LANDING checkin D T DeMyLink T checkin_ok landing _request P P allo
59. the left sides changes as new activities become possible supposing the model does not contain syntactic errors The model has been successfully loaded It is now possible to import create modify a model Model Definition to observe the model evolutions Model Evolutions to generate minimized model abstractions Model Abstractions Object obj1 myclass to verify the validity of temporal logic formulas Formula Definition written in full mu calculus enriched with CTL ACTL operators to configure the tool w r t the observation modes and other parametric aspects Preferences 29 01355 myclass1 Vars Signals step Operations State top 12 Transtions 2 gt 51 step x 0 51 gt 52 k 0 x 1 step Object obj1 myclass At this point the possible new activities are the following Observing the model statecharts Observing the evolutions map Abstracting the concrete model Editing and checking a formula Customizing some user preferences These activities are now described in more detail Observing the model statecharts Clicking over the image shown here in the left frame on UMC a new pop up window is opened which contains formatted description of the current classes constituting the model where all the statecharts are shown in a graphical format Class Classname is Signals s1 2 x 3 y bool 4 z Classname Operations
60. the relevant formulas and their validity in that state green true red false Moreover clicking over a node of the example we can observe all the internal details of that system configuration values of attributes active transitions possible configuration evolutions which may help in understanding the validity of subformulas in that configuration state Sample Example CounterExample model evolutions submap Set the graphics frame dimension to 1X 1 5X 8X 12X You can observe the details of a configuration clicking over the corresponding node If If you cannot visualize then picture below you probably need to install a svg viewer plug in like that of Adobe Use Command mouse to zoom in Command shift mouse to zoom out alt mouse to move the picture Use ctrl mouse to access the svg menu Customizing some user preferences The behaviour of the underlying umc tool and in particular the abstraction level observations point of view can be customized according to some parameters when the Preferences button is the control part of the window is selected The possible options are the same as those explained in Section 4 1 under the title Viewing and adjusting some tool preferences and parameters Here we only recall the Observation Mode parameters which are those allowing to specify which events are we interested to observe when drawing graphs or checking the system behavior These Observation Mode
61. the set of transitions whose source states are active in the current configuration whose trigger satisfies the currently dispatched event if any of the state machine events queue and whose guards evaluate to true in the current configuration The resulting set is called the set of enabled transitions w r t active states trigger guards If the set is empty the run to completion step terminates here with the removal of the dispatched event from the events queue unless deferred c Dealing with priorities If the previous set is not empty according to the relative priority between transitions which is a partial ordering we find a maximal subset of the transitions identified at the previous step so that there are no two transition inside the set of which one has a priority lower than the priority of the other there are no transitions inside the set with a priority which is lower than the priority of any other transition outside the set d Dealing with conflicts Given the set of maximum priority enabled transitions some of which might be executed in parallel we must find all its maximal subsets such that no two transitions in the subset are in conflict two transitions are in conflict if the intersections of the set of states they exit is not empty Notice that if a statechart has no parallel substates then each of these subsets will contain exactly one transition These subsets represent a set of concurrently fireable transitio
62. ts Graphics generated with GraphViz _http www graphviz org Automata minimization with fc2tools _http www sop inria fr meije verification and EST _http ims uni mb si EST XMI analysis by Marco Fabbri The UMC www page is constituted by two main sections a left column containing a menu of commands a set of status lights and two clickable images for configuring the tool preferences and displaying the current model structure and a right column used to display the I O interactions text editing graph drawing between the tool and the user The first step in performing a system analysis is the definition of the model A model can be inserted in its textual form or reloaded from the server in the case the tool session is for some reason closed and later restarted or imported from a pre existing local text file or extracted from an existing XMI model this functionality is currently very badly supported and generated code in an obsolete format which requires further corrections by hand Alternatively one of the predefined existing examples can be selected 28 allowed comment delimi all these 0 allowed comment delimit class definition ame wrint bool self 0UT print v1 Object 0011 Classname v2 gt 0011 static object instantiation Once the model has been defined we should pass to the basic umc tool this is done with the Load Current Model button Once loaded the menu of
63. w Generation Integrated Embedded Systems Pr MURST 40 41 Feedback Please submit bug reports comments and suggestions to franco mazzantiWisti cnr it 9 References M von der Beeck Formalization of UML Statecharts UML 2001 Confrence LNCS 2185 Springer Verlag pp 406 421 2001 A Biere A Cimatti E M Clarke and Y Zhu Symbolic Model Checking without BDDs TACAS 99 LNCS 1579 Springer Verlag 1999 A Bouali S Gnesi S Larosa The integration Project for the JACK Environment Bulletin of the EATCS n 54 pp 207 223 1994 E M Clarke E A Emerson and A P Sistla Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specification ACM Transaction on Programming Languages and Systems 8 pp 244 263 1986 R De Nicola F W Vaandrager Action versus State based Logics for Transition Systems Proceedings Ecole de Printemps on Semantics of Concurrency LNCS 469 pp 407 419 1990 A Fantechi S Gnesi F Mazzanti R Pugliese E Tronci A Symbolic Model Checker for ACTL Applied Formal Methods FM Trends 98 LNCS 1641 Springer Verlag 1999 J C Fernandez H Garavel A Kerbrat L Mounier R Mateescu and Sighineanu M CAPD a Protocol Validation and Verification Toolbox In CAV 96 LNCS 1102 Springer Verlag 1996 see also http www inrialpes fr vasy cadp S Gnesi D Latella and M Massink Model checking UML statechart diagrams using JACK In A Williams editor Fourt
64. w_landing MyPlane_allow_boarding landing_request P anding P checkin D T P landing delayed Fe agi Toe Y 7 _ i close T checkin_closed HANDLING HANDLING BOARDING ARRIVALS landing_request P P landing delayed HANDLING TAKEOFF 37 Class Airport Vars MyPlane obj atLoc obj MyLink obj Events landing request P obj checkin D obj T obj boarding done takeoff_done landing done P obj State Top created HANDLING CHECKIN HANDLING_BOARDING HANDLING TAKEOFF HANDLING LANDING HANDLING ARRIVALS Transitions created MyPlane null gt HANDLING LANDING created MyPlane null lt HANDLING CHECKIN HANDLING CHECKIN landing _request P P landing delayed gt HANDLING CHECKIN HANDLING CHECKIN checkin D T D MyLink T checkin_ok MyPlane allow_boarding T D gt HANDLING BOARDING HANDLING BOARDING landing _request P P landing delayed gt HANDLING BOARDING HANDLING BOARDING checkin D T T checkin_closed gt HANDLING BOARDING HANDLING BOARDING boarding_done MyPlane allow_takeoff gt HANDLING TAKEOFF HANDLING TAKEOFF landing _request P P landing delayed gt HANDLING TAKEOFF HANDLING TAKEOFF checkin D T T checkin_closed gt HANDLING_TAKEOFF HANDLING TAKEOFF takeoff done MyPlane null gt HANDLING LANDING HANDLING LANDING checkin D T T checkin_closed gt HANDLING_LANDING HANDLING LANDING landing request
65. when there is not a unique deepest source 2 From this poi of view the UML semantics is not very clear 13 formula EF predicate will return a defined value if and only if a configuration satisfying the predicate exists at some finite depth of the evolutions tree In general a definite result will be produced by the tool if and only if a finite example or counterexample for the formula does exist State Predicates The simplest form of logic formula is a StatePredicate A StatePredicate can be either the formula true or the formula false or a predicate on the internal structure of a system configuration The formula true clearly holds for any state the formula false never holds in any state A StatePredicate can also be relation between simple expressions involving attributes and values such formulas hold for all the states in which the evaluation of the relation is true Examples ASSERT obj objattr intattr gt 0 ASSERT obj3 x 1 gt objl yt obj2 z The allowed relational operators are lt gt lt gt The simple expression can be an object attribute a numeric value or a sum of them The obj prefix of the attribute can be omitted is the system is constituted by a single active object E g x lt y is a valid state predicate for a single object system The special keyword queuesize acts like an object attribute and denotes the current length of the events
66. y are executed in a sequential way in any order Notice that this does not mean that 12 statechart transition are atomic with respect to the system behavior since its activity can contain synchronous call causing suspensions resumptions of the activity 2 Atomicity of object evolutions w r t system evolutions Given a model constituted by more than one state machine a system evolution is constituted by any single evolution of any single state machine I e state machine evolutions are considered atomic and indivisible at system level when no synchronous calls are involved 3 Reliable point to point and untimed communications The propagation of signals inside a state machine and among state machines is considered instantaneous and without duplication or losses of messages this is an aspect intentionally left as unspecified by the UML standard the communication is direct and one to one no broadcasts 4 FIFO event queues The events queue associated with a state machine handles its events in a FIFO way this is an aspect intentionally left as unspecified by the UML standard 5 Well definedness of priorities The relative priority of a join transition is always well defined identified with the priority of the first of its source states and statically fixed 6 Completion of operation calls The return signal from an operation function call occurs when the return statement is executed inside the transition triggered by the op

UMC 3.3 User Guide - Formal Methods && Tools Group

Contents

Download Pdf Manuals

Related Search

Related Contents

UMC 3.3 User Guide - Formal Methods &amp;&amp; Tools Group

Contents

Download Pdf Manuals

Related Search

Related Contents

UMC 3.3 User Guide - Formal Methods && Tools Group