TOWARDS FORMAL VERIFICATION OF MODEL TRANSFORMATIONS

varromit.bme.hu As the Unified Modeling Language is evolving into a family of languages with inpidually specified semantics, there is an increasing need for highly automated and provenly correct model transformations that would assure the integration of

AbstractAstheUni edModelingLanguageisevolvingintoafamilyoflanguageswith

inpiduallyspeci edsemantics,thereisanincreasingneedforhighlyauto-

matedandprovenlycorrectmodeltransformationsthatwouldassuretheinte-

grationoflocalviewsofthesystem(intheformofdifferentdiagrams)intoa

consistentglobalview.Graphtransformationprovidesaneasy-to-understand

visualspeci cationtechniquetoformallycapturetherulesofsuchtransforma-

tions.Inthepaper,wesummarizetheconceptsofVIATRA,thegeneralpurpose

modeltransformationsystemtogetherwiththemajorcorrectnessrequirements

andamodelcheckingbasedveri cationmethodformodeltransformations.

Keywords:modeltransformation,modeltransitionsystems,graphtransformation,UML,

formalveri cation,

Nowadays,theUni edModelingLanguage(UML)hasbecomethedomi-natingspeci cationandmodelinglanguageforthedesignprocessofsoftware.However,despiteitsindustrialsuccessasbeingauni edandvisualnotation,theimprecisenessofUML(i.e.,thelackofformalsemantics)isstillthemajorfactorthathindersthegeneraluseofUMLasaprimarysourcelanguagefor(i)automatedtoolsofformalveri cationandvalidationexploitingtheresultsinthetheoryofformalmethods,and(ii)automatedcodegeneratorsthatwouldyieldaprovenlycorrectfunctionalcoreoftargetapplication.

Recentinitiatives(UML2.0RequestforProposal)oftheObjectManage-mentGroup(OMG)aimattore-architecturethesingleandmonolithlanguageThisworkwassupportedbytheHungarianNationalScienti cFoundationGrant(OTKA030804).

varromit.bme.hu As the Unified Modeling Language is evolving into a family of languages with inpidually specified semantics, there is an increasing need for highly automated and provenly correct model transformations that would assure the integration of

intoafamilyoflanguages(builtaroundakernelmetamodelinglanguage)eachhavingitsownwell-de nedsemantics.

However,astheformalseman-

ticsofdifferentviewsofthesystem(i.e.,separatediagramslikeclassdiagrams,statecharts,sequencediagrams,etc.)mightbede nedindifferentsemanticdomain(e.g.,byPetrinets,SOSrules,graphtransformationsystemsetc.),theintegrationofsuchlocalviewsintoaconsistentglobalviewofthesystemre-quiresaprecisespeci cationandveri cationoftransformationswithinandbetweenUMLmodels.

Inpractice,transformationsarenecessitatedforseveralpurposes:(i)modeltransformationswithinalanguageshouldcontrolthecorrectnessofconsecu-tivemodelre nementsteps,(ii)modeltransformationsbetweendifferentlan-guagesshouldprovideprecisemeanstoprojectthesemanticcontentofadia-gramintoanotherone,whichisindispensableforaconsistentglobalviewofthesystemunderdesign,and(iii)avisualUMLmodel(i.e.,asentenceintheUMLlanguagefamily)shouldbetransformedintoitssemanticdomain(calledmodelinterpretation).

AstheabstractsyntaxofUMLmodelsisde nedvisuallybyacorrespond-ingmetamodel.Astraightforwardrepresentationofsuchmodelscanrelyontheuseofdirected,typed,andattributedgraphsastheunderlyingsemanticdomain.Therefore,theuseofgraphtransformation[7]forcapturingthese-manticsofUMLmodelsandtheirtransformationsisanaturalchoicewhichalso tswelltoengineeringpracticesasaconsequenceofitsvisualexpres-siveness[3,4,9,11].

However,duetoahugeabstractiongapbetweenvisualUMLmodelsandformalmathematicaldescriptions,thespeci cationandimplementationofmodeltransformationsystemsarehighlypronetohumanerrors,whichnecessitatesahighlyautomatedveri cationandprogramgenerationmethodforsuchsys-tems.

VIATRA(VIsualAutomatedmodel

TRAnsformations[11],seeFigure1)isaprototypetoolbeingdevelopedattheBudapestUniversityofTechnologyandEconomics,thatprovidesagen-eralmeanstospecify,implementandverifyvariousmodeltransformations(tailoredespeciallytoUML-basedtransformations).

1AsthebeginningofatypicalinteractionwithVIATRA,thetransforma-tiondesignerconstructsthemetamodelsofthesourcelanguage(typi-callyUMLitself)andthetargetlanguages(formalmodelssuchasPetriNets,Kripkeautomaton,etc.)intheformofUMLclassdiagramsex-portedintothestandardXMIformat.

varromit.bme.hu As the Unified Modeling Language is evolving into a family of languages with inpidually specified semantics, there is an increasing need for highly automated and provenly correct model transformations that would assure the integration of

1

TheVIATRAenvironment

2Afterwards,thetransformationrulesarespeci edinavisualnotationbasedonaUMLpro letailoredtographtransformationsystems.

3Fromthisvisualdescription,themodeltransformationprogramisgener-atedautomaticallyintheformofaPrologprogram(see[10]forfurtherdetailsonautomatedprogramgenerationinVIATRA).

4ThisPrologprogramtakesasourceUMLmodelasinputandgeneratesthetargetmathematicalmodelastheoutput(sinceallmodelsarerepre-sentedinVIATRAusingtheXMIstandardtheunderlyingPrologengineishiddenfromtheuser).

5Theresultsofthemathematicalanalysiscanbeback–annotatedintothesourcelanguagebyadditionalmodeltransformations.

ThemaincontributionoftheVIATRAapproachisits exibilityandpre-cisenessforautomatedmodeltransformationsaimingattoinvestigateandfor-mallyverifyUMLmodelsfromdifferentaspects(suchaslogicalcorrectness,dependabilityandperformabilityanalysis).However,suchatransformationbasedautomaticmodelgenerationapproachmightnotassureahigherqualityofsystemveri cation,unlessthefaithfulnessandconsistencyofUMLmodelsandtheabstractmathematicalstructuresofformalanalysiscanbeguaranteed(preferably,formallyproven).Inthecurrentpaper,afterabriefsummaryofconceptswediscussthemajorcorrectnessrequirementsandamodelcheckingbasedveri cationapproachofmodeltransformationsystems.

WeinformallysummarizebelowthemajormodeltransformationconceptsofVIATRA.Models(andmetamodels,whichdescribetheabstractsyntaxof

varromit.bme.hu As the Unified Mo …… 此处隐藏：17015字，全部文档内容请下载后查看。喜欢就下载吧 ……