您好,欢迎访问三七文档
当前位置:首页 > 研究报告 > 信息产业 > 网络嵌入式系统的描述与分析
JournalofHarbinInstituteofTechnology(NewSeries)Vo1.12,No.4,20051ThespecificationandanalysisofnetworkembeddedsystemZHANGGuan-huaZHANGLian-huaBAIying-cai(Dept.ofComputerScienceandTechnology,ShanghaiJiaotongUniversity,Shanghai200030,China)Abstract:Thispaperproposesaformalmethodwhichisusedtomodelandanalyzenetworkdevicessuchasrouters.Itisbasedonanalgebraicprocesscalled“ACSR-VP”,whichenhancestheoriginalCCSalgebraicprocessbyincorporatingthenotionsoftime,resourcerequirements,dynamicprioritization,andsynchronization.Therefore,althoughtherearemanyformalmethodstoanalyzethetimedconcurrencysystem,ACSR-VP,duetoitsprominentfeatures,isbestfitforanalysisofaresourceboundedreal-timesystem.ThispaperextendsACSR-VPtoEACSR-VP,whichismoreadaptivetothefeaturesofnetworkdevicesandspecializesinanalyzingthiskindofembeddedsystem.EACSR-VPaddsthenotionofn-waycommunicationwhichallowsmorethantwoprocessestoparticipateinsynchronization.Italsoenhancesvalue-passingcapabilitieswhichmakeformoreflexiblespecifications.Finally,specifications,verificationandanalysismethodswithEACSR-VPareintroducedbyacasestudyofrouterwithmultipleinputqueues.Keywords:Formalmethod;processalgebra;networkdevices;modelingCLCnumber:TP393Documentcode:AArticleID:1005-91l3(2005)O4-0434-06TherapidgrowthoftheInternethasdemonstratedthelargedemandfornetworkdevicessuchasroutersandswitches.Withwidelyusedapplicationssuchasmultimedia,thefunctionsoftherouterbecomesmoreandmorecomplicatedandtheimplementationanddesignofroutersbecomesincreasinglydifficult.Therefore,evenatrivialerrormayleadtotheredesignofthewholesystem.Tomitigatethisrisk,aniterativeprocessofdesign-implementation-designisrequired.Consequently,thedevelopmentcostisveryexpensive.Theformalmethodcanbeusedtospecifythesystembeforeitsimplementationandanalysistovalidateandtestit.Asaresult.allerrorscanbecorrectedduringthedesignprocessandsubsequentlydevelopmentcostisgreatlyreduced.Researchonformalmethodsforrea1-timeembeddedsystemsisveryactive.Mostoftheworkfallsintofourmaincategories:timedlogics,automatatheory,Petrinetsandprocessalgebra.Inmethodsbasedontimedlogics,systemsaredescribedbyasetofassertionsandpropertiesarerepresentedastheorems.Apropertyholdsforasystemifitcanbelogicallyreasonedfromtheassertions.Suchmethodscanprocessstrictreasoningbuttheydonothaveanexecutionmodelandthereforetheycannotleadtoanimplementationdirectly.Intimedautomatamethods,computationmodelsarerepresentedusingfinitestateautomataandasetofclockdataassociatedwithit.ThestatetransitionThespecificationandanalysisofnetworkembeddedsystem2canbeexpressedasaconsequentoccurrenceofasetofeventswiththeirtimeconstraints.Suchamethoddoesnotsupportsynchronouscommunication.Petrinetscandescribemanyconcurrencyfeatures,butitonlyisamode1.Ithasnocalculi.MethodsbasedonProcessalgebrauseinterleavingmodelstospecifyconcurrency.Typicalexamplesare[1]CCS,[2]CSPand[3]ACP.SuchmethodscanrepresentdetailedbehaviorofsystemsandbothCCSandCSPhavegoodalgebraicproperties.Theynotonlycanmodelbehaviorofsystems,butalsohaveareasoningcalculisystem.Tousesuchmethodsunderreal-timeenvironments,manyextensionshavebeenintroducedbymanyresearchers.SomeexamplesaretimedCCS(TCCS),CCSwith[4]priorities,CSPwithdelay[5,6]operationand[7]ACP,etc.In[8]Re.f,LeeproposedanACSRframework,whichisakindoftimedprocessalgebrabasedontheCCSmode1.Thismethodincorporatessynchronous,time,resourcerequirementsandprioritiesintoCCS.Itsupportsmodularspecificationandvalidationofthesystem.Itisveryadaptivetoanalyzeresourceboundsystemssuchasrouters.[9]ACSRVPisanextensionofACSRwithdynamicprioritiesandavalue-passingmechanismasfollows:1)prioritiescouldbevalueexpressionscontainingvariables;2)aninstantaneouseventisaddedwithavalueexpressiontorepresentvalue-passing.Thenetworkembeddedsystembelongstoareal-timeembeddedsystemwithboundedresources.It’smaintaskistoprocessinputpacketsandacertainpacketforwardingratemustbesatisfied.Althoughmuchresearchofformalmethodsforembeddedsystemshasbeendone,thereisnospecialfocusesonnetworkdevices.ThispaperextendsACSR-VPtoEACSR-VP,whichismoreadaptivetofeaturesofnetworkdevicesandpresentsspecificsinanalyzingthiskindofembeddedsystem.ThismethodinheritsmanyofthebestcharacteristicsofACSR-VPandaddsseveralnovelconcepts.Firstly.thenotionofn-waycommunicationisadded,whichallowsmorethantwoprocessestoparticipateinsynchronization.Secondly,thispaperenhancesvalue-passingcapabilitieswhichmakevaluespassthroughmorethantwopossibleprocesses.Italsoaddssubscriptingtothelabelofinstantaneouseventtomakevalue-passingmoreflexible.Value-passingalsocanthenbeusedtorecordthestateofexecution.Atlast,dynamicprioritiesareusedtoimplementalgorithmicschedulinginputqueuesandsynchronizationamonginputqueueprocessesandroutingprocess.Thispaperisorganizedasfollows:inSection1,thesyntaxofEACSR-VPisdefinedanditssemanticsisexplained;Section2introducesspecification,validationandspecificationmethodbythecasestudyofrouterwithmultipleinputqueues;finally,Section3presentsthepaper’sconclusions.1EACSR-VPJournalofHarbinInstituteofTechnology(NewSeries)Vo1.12,No.4,200531.1SyntaxDefinition1Thedo
本文标题:网络嵌入式系统的描述与分析
链接地址:https://www.777doc.com/doc-8690064 .html