网络嵌入式系统的描述与分析

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]ACSRVPisanextensionofACSRwithdynamicprioritiesandavalue-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