广工动漫外文文献Word文档格式.docx
- 文档编号:3770901
- 上传时间:2023-05-02
- 格式:DOCX
- 页数:39
- 大小:207.88KB
广工动漫外文文献Word文档格式.docx
《广工动漫外文文献Word文档格式.docx》由会员分享,可在线阅读,更多相关《广工动漫外文文献Word文档格式.docx(39页珍藏版)》请在冰点文库上搜索。
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]
[Liu,2004b]),thecombinationofUnifiedModelingLanguage(UML)andObjectConstraintLanguage(OCL)(WarmerandKleppe,1999),andCleanroom([Millsetal.,1987]
[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]
[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]
[Liuetal.,1998b]).Ithasalsobeenappliedinthedevelopmentofnetworkprotocols([Taguchi,2000]
[Liu,2003a])andofsomecommercially-basedsystems([Liuetal.,1999],[Liu,2003b]
[Liu,2004a]).Inadditiontoitsdirectapplications,SOFLhasbeenusedasthebase-languagefordevelopingaspect-orientedspecificationparadigm(ShenandChen,2005),modellingtechnologyfordevelopingmiddleware-basedtransactionmanagement(Chenetal.,2005),andtestingtechniques([Liu,1999]
[OffuttandLiu,1999]).Togetherwiththeprogressinsupporttools,SOFLhasagreatpotentialforindustrialapplicationinthefuture.ThefinalreasonisthatourexpertiseinSOFLandpreviousexperienceinresearchonSOFLspecificationreviewenableustohaveagoodinsightintothefundamentalprincipleoftheproposedanimationandtoeffectivelydevelopthetechniqueandthetool.AlthoughthediscussioninthispaperisbasedontheSOFLspecificationlanguage,theproposedanimationtechniquecanbeeasilyextendedforanimationsofspecificationsinotherrelatedlanguages,suchasVDM-SLandDFD.
There
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 动漫 外文 文献