广工动漫外文文献.docx

广工动漫外文文献.docx

《广工动漫外文文献.docx》由会员分享，可在线阅读，更多相关《广工动漫外文文献.docx（39页珍藏版）》请在冰点文库上搜索。

广工动漫外文文献

2012广工工商管理动漫外文文献原文

Anautomatedapproachtospecificationanimationforvalidation

ShaoyingLiua,

HaoWangb

aDepartmentofComputerScience,HoseiUniversity,3-7-2Kajino-cho,Koganei-shi,Tokyo184-8584,Japan

bShanghaiJiaotongUniversity,China

Received14November2005.Revised30November2006.Accepted7December2006.Availableonline20December2006.

http:

//dx.doi.org/10.1016/j.jss.2006.12.540,HowtoCiteorLinkUsingDOI

CitedbyinScopus（9）

Permissions&Reprints

Abstract

Formalspecificationhasbeenincreasinglyadoptedforthedevelopmentofsoftwaresystemsofthehighestintegrity.However,thereadabilityofspecificationsforlarge-scaleandcomplexsystemscanbesopoorthateventhedevelopersmaynoteasilyunderstandwhethertheirspecificationsdefinethe“intendedbehaviors”.Inthispaper,wedescribeasoftwaretoolthatsupportstheanimationofspecificationsbysimulatingtheirfunctionalscenariosusingtheMessageSequenceChart（MSC）.Thetoolextractsautomaticallyfunctionalscenariosfromaspecificationandgeneratesamessagesequencechartforeachofthemforasyntacticlevelanalysis.Thetoolcanalsoexecuteafunctionalscenariowithtestcasesforasemanticlevelanalysisifalltheprocessesinvolvedinthescenarioaredefinedusingexplicitspecifications.Withthetoolsupporttheanimationofaspecificationcanbecarriedoutincrementallytoassistitsusertoreviewtheadequacyofthespecification.Wepresentacasestudyapplyingthetooltoanimateaformalspecificationforalibrarysystemandevaluateitsresult.

Keywords

Specificationanimation;

Validation;

Formalspecification

1.Introduction

Itiswellrecognizedthatstartingthedevelopmentofasoftwaresystemofthehighestintegritybywritingitsspecificationinaformalnotationissubstantiallybeneficial（[BowenandHinchey,1999] and [HincheyandBowen,1999]）.Duetothewell-definedsyntaxandsemanticsoftheformalnotation,theformalspecificationprovidespreciseandconciserequirementsfortheproposedsoftwaresystem.Inparticular,formalspecificationlanguageswiththefeatureofintegratingtextualformalnotationswithintuitivegraphicalnotationsdevelopedinrecentyears,suchastheStructuredObject-OrientedFormalLanguage（SOFL）（[Liuetal.,1998c] and [Liu,2004b]）,thecombinationofUnifiedModelingLanguage（UML）andObjectConstraintLanguage（OCL）（WarmerandKleppe,1999）,andCleanroom（[Millsetal.,1987] and [LingerandTrammell,1999]）,haveevengreaterpotentialtobeadoptedbypractitionersforwiderapplications.Apartfromtheadvantageofforcingdevelopers（thepersonswhobuildsystems）toclarifyambiguitiesinrequirementsbywritingformalspecifications,theresultantspecificationsalsoofferafirmgroundfortheverificationandvalidationoftheformallydefinedfunctionsandotherimportantproperties（e.g.,safety,security）undereffectiveandefficienttoolsupport.However,asLevesonpointsoutin（Leveson,2000）,theadoptionofformalspecificationsinindustryalsofacesvariouschallenges.Oneimportantchallengeisthatformalspecificationsareusuallywritteninacomplexstructureandaredifficulttoreadandunderstand.Thisispartiallybecauselargescalesystemstendtohaveacomplexfunctionalityandproperties,andtheformalizationofthemusuallyleadstoacomplexstructureoftheinvolvedcomponentsandtheconcentrationofdetailedformalexpressionsdefiningthefunctionsofoperations.Itisalsobecauseformalspecificationsmaynotintuitivelyreflectthecorrespondingconceptsandbehaviorsofsystemsintherealworld.Forthisreason,itisnoteasyforpeopletobuildamental“bridge”betweenexpressionsinformalspecificationsandperceptionsofthecorrespondingsystemsintherealworld.Ofcourse,thelackoftraininginformalspecificationmayexacerbatethedifficultyinpractice.

Sincedetectingerrorsinrequirementsspecificationsreducesmuchmorecostthandetectingerrorsinprograms（Boehm,1981）,itissignificantlybeneficialtoverifyandvalidatespecificationsbeforetheirimplementations.Specificationanimationwasdevelopedasaneffectivetechniqueforthispurpose.AsMillerandStrooperpointedoutin（StrooperandMiller,2001）,animationservestwopurposes:

（1）givingendusersandfieldexpertsachancetointeractwiththespecificationandobserveitsoperationalbehavior,and

（2）providingthespecifierwithconcreteexamplesofhowthespecificationbehaves,sothattheycancheckwhetherthespecificationreflectstheintendedpropertiesoftheirdesign.Sometoolshavebeenbuilttosupportanimationofdifferentspecificationlanguages,suchasPiZA（Hewittetal.,1997）,ZALanimationsystem（Morreyetal.,1998）,Possum（Hazeletal.,1997）,B-Modelanimator（WaeselynckandBehnia,1998）,andANGOR（Combesetal.,2002）,butmostofthosetoolsfocusontheapproachsimilartotesting:

executingspecificationswithsampleinputvaluesandanalyzingtheresults.Ingeneral,thiskindoftechniquerequiresatranslationfromaformalspecificationlanguagetoanexecutableprogramminglanguage（e.g.,PrologorLISP）,whichimposesmanyrestrictionstothestyleofthespecificationswritteninthespecificationlanguage.Italsodisallowstheuserofthetooltoanalyzethecontentsofthespecifications.

Inthispaperweproposeadifferentapproachtospecificationanimationthatfacilitatesreviewsofspecifications.Usingthisapproach,areviewer（thepersonwhoconductstheanimation）readsthroughthetargetspecificationtodigestthecontentsandtoanalyzethepotentialbehaviorsofthespecificationinordertodetecterrorsinrelationtothevalidityorconsistencyofthespecification.Themajorprincipleunderlyingtheanimationapproachistoallowthereviewertocheckeverypossiblefunctionalscenariodefinedinthespecification.Afunctionalscenarioisasequenceofoperationsthatdefinesaspecifickindofbehavior.AnexampleofsuchascenarioistowithdrawmoneyfromanAutomatedTellerMachine（ATM）:

receivingtherequest,checkingthecardandpassword,andfinallyprovidingtherequestedamount.Wehavedevelopedasoftwaretooltosupportthisapproach.Thetoolautomaticallygeneratesallthepossiblefunctionalscenariosforagivenspecification.Italsoprovidesassistancetothereviewerinanimatingeachsinglescenariobysimulatingthepotentialbehaviorintermsoftransforminganinputtoanoutputthroughthesequentialexecutionsoftheoperationsinvolvedinthescenario.AsdescribedindetailinSection4,thetoolofferssupportforbothsyntacticandsemanticlevelanimations,andprovidesaneffectivemechanismtofacilitatethereviewertoflexiblycontroltheanimationprocess.Wehavealsoconductedacasestudyusingthetoolfortheanimationofalibrarysystem.Ourexperienceshowsthatthetooliseasytouseandeffectiveindetectingerrors,althoughtherearealsoaspectsforfurtherimprovement,asdescribedindetailinSection5.

Sincetheanimationtoolneedstosupportaspecificformalnotation,wechoosetheStructuredObject-orientedFormalLanguage（SOFL）（[Liu,2004b] and [Liuetal.,1998c]）asthetargetlanguagetosupportforthreereasons.OnereasonisthatSOFLintegratesthecommonlyusedformalmethodViennaDevelopmentMethod（VDM）（Jones,1990）withtheintuitivedataflowdiagram（DFD）（Yourdon,1989）.TheDFDisusedtomodelthearchitectureofasystemandanextendedVDMspecificationlanguage（VDM-SL）isadoptedtoformallydefineallthecomponentsinvolvedintheCDFD,suchasprocesses,dataflows,anddatastores.SinceDFDisintuitiveandwidelyappliedbypractitionersforsystemanalysisanddesign（Yourdon,1989）andVDM-SLoffersapowerfulnotationforpreciselydefiningthecomponentsofDFD,SOFLspecificationsarecomprehensibleatboththearchitecturelevelandthecomponentlevel.Thiswillpotentiallybenefitthecommunicationsbetweentheendusersandthedevelopers,andevenamongthedevelopers.Thispropertyisespeciallyimportantforspecificationanimationbecausethecommunicationsbetweenthedevelopersandtheendusersmayberequiredduringtheanimationprocessinordertomakecorrectjudgementsinvalidatingthespecification.ThesecondreasonisthatSOFLhasbeentaughttobothundergraduatesandgraduatesoverthelastsevenyears,especiallyinJapanandChina.Ithasbeenappliedtothemodellingofcomputer-controlledsafety-criticalsystems,suchastherailwaycrossingcontrollerincollaborationwithMitsubishiElectricResearchInstitute（[Liuetal.,1998a] and [Liuetal.,1998b]）.Ithasalsobeenappliedinthedevelopmentofnetworkprotocols（[Taguchi,2000] and [Liu,2003a]）andofsomecommercially-basedsystems（[Liuetal.,1999],[Liu,2003b] and [Liu,2004a]）.Inadditiontoitsdirectapplications,SOFLhasbeenusedasthebase-languagefordevelopingaspect-orientedspecificationparadigm（ShenandChen,2005）,modellingtechnologyfordevelopingmiddleware-basedtransactionmanagement（Chenetal.,2005）,andtestingtechniques（[Liu,1999] and [OffuttandLiu,1999]）.Togetherwiththeprogressinsupporttools,SOFLhasagreatpotentialforindustrialapplicationinthefuture.ThefinalreasonisthatourexpertiseinSOFLandpreviousexperienceinresearchonSOFLspecificationreviewenableustohaveagoodinsightintothefundamentalprincipleoftheproposedanimationandtoeffectivelydevelopthetechniqueandthetool.AlthoughthediscussioninthispaperisbasedontheSOFLspecificationlanguage,theproposedanimationtechniquecanbeeasilyextendedforanimationsofspecificationsinotherrelatedlanguages,suchasVDM-SLandDFD.

There