VIATRA - visual automated transformations for formal verification and validation of UML mod

  • 格式:pdf
  • 大小:99.65 KB
  • 文档页数:10

VIATRA-VisualAutomatedTransformationsforFormalVerificationandValidationofUMLModels(Tooldemonstration)

Gy¨orgyCsert´anG´aborHuszerlIstv´anMajzikZsigmondPapAndr´asPatariczaD´anielVarr´oBudapestUniversityofTechnologyandEconomicsDepartmentofMeasurementandInformationSystemsvarro,pataric@mit.bme.hu

AbstractTheVIATRA(VIsualAutomatedmodelTRAnsforma-tions)frameworkisatransformation-basedverificationandvalidationenvironmentforimprovingthequalityofsystemsdesignedwithintheUnifiedModelingLanguagebyauto-maticallycheckingconsistency,completeness,anddepend-abilityrequirements.Inthecurrentpaper,wepresentanoverviewof(i)themajordesigngoalsanddecisions,(ii)theunderlyingformalmethodologybasedonmetamodel-ingandgraphtransformation(iii)thesoftwarearchitecturebasedupontheXMIstandard,(iv)andseveralbenchmarkapplicationsoftheVIATRAframework.

1.IntroductionTheadventofvisualdesignlanguagespromisesnotonlyabetterrequirementcaptureandeasiersoftwarearchitec-tureprocess,butaradicalincreaseinsoftwareproductiv-ity,aswell.Thisincreasecanreachasmuchasoneorderofmagnitudeiftheentireprocessiscompletelyautomatedstartingfromtheearlyspecificationuntilanautomatedcodegeneration.UML,theUnifiedModelingLanguage[17],wasstan-dardizedbytheObjectManagementGroup(OMG)anditsrapidspreadasthedominantobject-orientedCASEtech-nologyclearlyindicatesthemarketneedforeffectivevisualdesigntechnologies.However,theuseofvisualCASEmethodologiesdoesassureneitherthecorrectnessofthedesign,noritsdepend-ability.Thedesignercanstillconstructsyntacticallycorrectbutsemanticallyincorrectmodelsjustinthesamewayaserroneousprogramscanbewritteninanarbitraryhigh-levelprogramminglanguage.Moreover,theoriginalUMLstan-dardwasnotintendedtocapturenon-functionalrequire-ments,likedependability.Theassuranceofthequalitativecorrectnessofasystemnecessitatesthecheckingof(i)thecompletenessandcon-sistencyofthesystemspecification,(ii)globalcorrectnessattributes,likethedeadlockfreedomofthedesign,and(iii)application-specificrequirements,likesafetyrequirementsofthetargetfieldofapplication.Thedependabilityofthetargetapplicationnecessitatesthefulfillmentofseveralquantitativerequirements,aswell.Forinstance,(i)timelinessoftheapplicationisoneofthemajorcriteriainreal-timesystemdesign,or(ii)reliabilityandavailabilitymeasuresarecrucialinthesystemdesignphaseduringtheselectionprocessamongalternatives.Duringthelastdecadescomputersciencehassuccess-fullyattackedthemajorityofthisproblemsbyprovidingmathematicmethodsandtoolsforthemodelingandanaly-sisofdependabilityattributes.However,thesemethodsarenotwidelyusedinthein-dustryprimarilyduetothehighlevelofabstractnessofthemathematicalmodelingandanalysistechniques.Addition-ally,thepropercoverageofthedifferentaspectsofdepend-abilityrequiresthecombineduseofavarietyofdifferentmathematicalparadigms.Thetediousnessofthismathematicalprocessconfinestheuseofanalysismethodstotheveryspecializedwork-groupsintheindustry,primarilydealingwithmission-criticalapplications.OntheotherhandtheassuranceofaproperqualityoftheservicesdeliveredbyacomplexITsystemdemandsmoreandmoretheprovenqualityofthetargetdesign.AformerESPRITprojectundertheacronymHIDE(car-riedouttogetherwithFAUErlangen,CNUCEPisaandtwoindustrialpartners[3])hasshownthefeasibilityofanau-tomated,multi-aspectdependabilityevaluationofUMLde-signsintermsoftheexpressivenessofthemodels,andthe

1run-timecomplexityofthemathematicalanalysis.TheworkflowofmathematicalmodelanalysisofHIDEwascomposedofthefollowingmainsteps:

EnrichmentoftheUMLmodelofthetargetdesignbylocaldependabilityattributes(likefaultandrepairrates)associatedtotheindividualcomponents.Anexpertcanestimatetheseattributesinaverysimilarwayastheparameterizationoftraditionaldependabil-itymodels;

Inclusionofqualitativerequirementsintheformofacheckingautomaton1

Automaticderivationofmathematicalmodels(likehi-erarchicalautomataandtemporallogicfortheproofoflogiccorrectness,orSPNforthequantitativeeval-uationofdependability)fromtheUMLmodelofthetargetdesignunderevaluation.

Back-annotationoftheresultsfromthemathematicalanalysistotheUMLmodelforpresentationtothede-signer.

2.Designguidelinesforatransformationframework

AnimportantexperiencegainedfromHIDEwasthatanad-hocimplementationoftransformationslackstheneces-sarypreciseness,thusimplementationerrorscanmakethetransformationsbetheweakestpointinthechainoftoolsservingfordependabilityevaluation.Thiswayamathematicallypreciseparadigmwassearchedforleadingtoageneral-purposeframeworkforthedefinitionandimplementationoftransformations.Anotherargumenttowardstheuseofsuchaframeworkwastheneedforahigh-degreeofflexibilityduetothefol-lowingmainreasons: