Thc purposc of this paper is to discuss currcnt trends of such UML statc mactrine model chccking rnethods, where model checkirrg is perforrrred by translation into formal notations. Formal methods have shown their advantages for functional requircments' inconsistency checking and their climirration at early stages of development and for cnrichirrg graphical notations to reveal vaguerress and inaccuracics as discussed in this paper.
UML state rnachines, rnodel checking, forrnal notations and
The design of system models and their modeling is widely used practice at the
early stages of software devclopment life cycle. Models provide better
understanding of proposed system and allow making correct decisions concerning the
implcmentation. For such purposes, thc diagrams, which are bascd on some
graphical notations, are uscd most common. To enablc communication bctween
developers, model diagrams have particular (standardizcd) underlying
graphicai nol,al,ions.Among srtch graphical notalions is Unified Modeling Language
(UML) [
Howcvcr, currently availablc tools arc mostly immature in a sense,that generated code rnust be ma,nuallyrefined to irnplernent algorithms and systenr behavior conccived by the devcloper. The most essential barrier to implement model driven devclopment vision is incomplete syntax and semantics of such graphical tcchnologies, which can yield to inconsistent interpretations evcn at thc initial stagcs of system dcsign.
Eveu crtrrent UML 2.0 specification allows semanticallv incompletc model specifications for use in scena,rio"UML-As-Sketch", and trends show that this situation will remain such also in the future. This means, that UML models can and will be designed both formally and informally. The only requiremcnt is that formal UML semantics must bc a subset of thc full UML semantics.
On the other hand, therc are tools, which provide automated code generation (usually only framework) directly from UML models, and vice versa. However, code gencratcd in this nanner, either rnust be nranually rcfined with algorithms that UML modeling tools cannot expresscxplicitly or the generated code is not sufficientlv effective fbr production.
Ncverthcless, to rlrakc confidence about correctuess of clcsigncclrnoclel and gencrated codc (even partial), thcre must be done additional checks,which arc in higher abstraction lcvels than codc in high level programming languages. Namely, model checking must be carricd out, to check whether particular model is semantically completc and self-consistent. Such chccks, for example, can be done with the help of formal mcthods. Wherewith, therc is a need for translation of gra,phicalnotations into some forrnal specification notation, which after.walds is analyzcd and executcd in the appropriate tools.
This is evcn more important for system's dynamic or behaui,oralmod,elqwhen developer needsassurance,that the model exprcssesproposed system's bchavior appropriatcly. For such cases,therc arc devclopcd methods and their supporting tools, thc brief survey and analysis of which is discussedin this paper.
The paper discussescurrcnt trcnds of such UML state machine model checking mcthods, whcre modcls arc translated into formal notations. The comparative analysis of four such formal model checking methods is given. Finally, thc paper concludcs with thc outline of current possibilities for formal model chccking of UML state machine models with the help of formal methods.
Formal model checking has proved to have a number of benefits, which gives detailcd vicw about the systcm bcing implcmented at thc stagesof systcm analysis and design. For example, modcl checking allows to: o validate behavior at the initial stages of system's design; o Reveal and eliminate functional requrements errors before implementation; o Obtain (automatically generate) formally "executable" model specification (i.e. systcm's prototypc); o Validate consisl,encvand complel,enessof model specificat,ion,and more.
To make model checking effect,iveand automated, model formal synt,ax and serna'trticsmust be defined. Otherwise, rnodel carr be viewed only as a, sketch, and inconsistenciesand contradictions must bc validated manually by using devcloper's knowledge.
Thc most important thing in modcl checking is that models allow systcm analysis at high abstraction levcls, where nondeterministic and parallel actions may take placc. Thus, cxecutable codc generation from the model and checking of such code may not always give expected results. Developer must not only analyzecach modcl's node interconnectionswith other nodes, but also. and more
TheAnalysis of UML StateMachine Formal CheckingMethods I 33 importantly, look at thc model as a whole and evcn in conncction with other models, where thc same artifact is viewed from differcnt aspects or viewpoints.
It is especially important in modeling system's behavior. Even if the model reflects system's bchavior in tirne, usually it is shown in the fbrrn of static diagram. If such models arc '(cxccuted" before they arc transformed into code, it is possible l,o reveal some deficiencies,which may show up only in t,hemn-time, but not in thc compile-time.
The ncxt scction discussesin dctail the possibilities of chccking system's
behavior from UML state machines [
As the subjcct for comparison and analysis, we chose four formal model checking methods (approachcs), which providc mcans of translating statc machine models into formal notations for actual model checking. The mcthods are the following: a Fernd,ndez-Tovalrewrite logic ; o Zhao graph transformation ; O Knapp-Merz Hugo/ RT tool; a Sekerinski-Ztrob abstract machine notation and B;
This decision is based solely on a variety of implementation forms. The only common thing among chosen methods is that they formalize UML state machine notation by transfbrming models into fbrmal specifications with which fbrmal modcl chccking is performcd. From the implementation viewpoint, thcsc methods are complctely independcnt from each other. There are many othcr methods available, but thc sclection for this rcsearch was bascd on the degree of involvcd formal mcthods and notations.
Jos6 Luis Fern6ndez Alem6n and Ambrosio 'foval Alvarez propose UML metamodel based method, which formalizes UML state machine diagrams in rewrite logic [ ]. To accomplis]r t]ris, they apply rewrite logic and the specification language Maudc.
Yu Zhao with colleagues [
Alcxander Knapp and Stephan Merz propose model chccking approach bascd
on rclations between different UML diagram types [
The la-st of the reviewed methods is proposed bv Emil Sekerinski and Rafik
Zurob.In it, thc statechart diagrams are translated into Abstract Machine
Notation (AMN) of B method [
Fernandez-Toval
Zhao
Knapp-Merz Rewritelogic /
Maude
Graph transformationsand
Petrinets
Hugo/RT
Yes
Sekerinski
Zurob AMN and B method /iState
Yes Underlying theory / tool Has support for static semantic Has support for dynamic semantic Model can be executed UsesUML metamodel Automatic output of model errors
Can generate source code
Yes Yes
No Only for checking of static semantics
Yes N o Yes N o
Panly (only for static semantics)
Partly (mustusePetrinet debugging)
Partly Partly Yes (by translatinginto (by translating
Javacode) into code) In any tool which Yes Yes supportsexecution (for demonstration (asfinal product of Petrinetmodels ouroosesonlv) code)
Yes
Partly (only for static semantic)
Yes (for demonstration pumosesonly)
Partly (only for static semantic)
Yes Yes in Harel's notation, but taking into account the origins of UML statc machine diagrarrts,ttreir method can be modified for application to UML state rnachines.
Summary of reviewed methods is givcn in Table 1. First column lists comparative propcrties and thc rest of columns contain property values for each method. Chosen comparison characteristics are based on scmantics (both, static and dynamic) handling and analysis of model checking results.
Revicw of the mcthods revealcd, that thc main problem to handle, is the formalization level of UML state machine operational semantics (mathematical foundat,ion for inl,erpretation and execution sequence),which is not fully defined by UML designers. This mcans, that fbnnalization may be different f?orn one method to another and thus made incompatible, and lead to different interpretations, espccially in thc aspect of cxccution.
Possiblc solution to this problem could be thc translation of UML state machinesirrto hiera,rchicalfinite state autorna,ta,H.owever, it doesnot provide mea,ns for description of some esscntialUML state machine properties, for cxample, activitics, input and otttpttt actions, finishing evenl,sand transit,ions,historical and branching pseudostates,and adaptation of them arc not trivial.
All reviewed mcthods supports checking of static semantics-thcy can give answer to whcther modcl is complcte-with cntry, initial state, intermcdiate states and final state and exit, but cannot give answer whether it is logical. Checking of dynamic semantics is allowcd in methods with executable formal specifications.
TheAnalysis of UML StateMachine Formal Checking Methods
The purpose of checking of dynamic semantics is to clarify, whether model clcments are well connected. This is accomplished by selection of appropriate formal notation,, as in Zhao's method, where formalization in Pctri nets and tool availability enables morc throughout model checking. Model exccution is cxploratiort of rnodel state space. Becausc statc space can be infinite, rnodel execution strategies (espccially for nondeterministic and concurrent states) dctermine whcther results will bc adcquatc.
However, all reviewed mcthods havc common characteristic. Namely, they all are bascd orr UML rnetarnodel, which cnables easerrefineurentsof the method, when UML state machine metamodel definition change.Additionally, metamodel inconsistenciesand missing definitions must be corrected.
Howcver formal or automatcd model checking may be, inevitably, thcrc arc situations in which decisions must bc made by the model developer. Nevertheless, his or hcr dccision may largely depend on information about current model and lurther refinement. Fbr such cases,the tool must output appropriate model checking results. All reviewed methods output inconsistenciesof model static semantics, nonethclcss,model behavior correctncssand inconsistency elimination is solely on developers' compctcnce and intuition.
Finally, in the context of model driven development, comprehensivc codc gcneration from the modcl is essentialstep, which gives confidcncc that transfbrmation is perfbrrned wittr strict rules and that code indeed reflects developed modcl. Unfortunately, in revicwcd methods this step is still immaturc, if supportcd at all. The result is whether inefficient from run-time vicwpoint (KnappMerz's method) or define restrictions against model properties and programming languagcs (Sekerinski-Zurob's mcthod). 4
In this paper wc outlined selection of formal model checking methods, the main distinction of which is their usc of model translations into formal notations and fbrmal specification languages particularly, with the aim to utilize advantages of formal specifications in rccovery of inconsistencies and their eliminations. The paper outlined main problcms developer must deal with when UML state machinc diagram model checking is performed.
The common conclusion is that there are many different methods available, but none of them covers all aspects of bchavioral model checking-cach has its own advantages and disadvantages. Howcvcr, the most notable shortcoming is that current UML specification is not fully formalized, which, in turn, makes method creators do their own formalization, which may differ from othcr formalization approaches,though slightly.
This topic is also important in the context of model driven development, whcre models are supposed to be the main artifact of system's dcsign. In fact, the more elaborated tools developers will havc the more high-level abstraction chccks they will be able to perform, thc more precise models will be developed and generated code will be more effective.
This research was conducted as part of ongoing research for implementation
of framework for Modcl Driven Architecture extension with formal methods [
The common conclusion is that the modcl checking still is mainly guided by thc developer, and for automatically generated code to be fully optimized for particular modcl, therc is the nccd for further rescarch. In addition, formal methods are subject to critique for their large learning curve and missing effective tool support; howevcr, formal methods applications has proved as advantageous in functional requirement inconsistency checking and their elimination at early stages of system's devclopment, and for cnriching graphical notations to revcal vagucness and inaccuracies, as was discussed in this paper.
Thi,s work has been partlg supported by the European Soci,al Fund w,ithi,n the Nati,onal Programme "Support for the carry'ing out doctoral studg program's and post-doctoral researches"project "Support for the deuelopment of doctoral studi,es at Ri,ga Techni,cal Un'iuers,itg".