ThespecificationandanalysisofnetworkembeddedsystemZHANGGuan-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．Thestatetransitioncanbeexpressedasaconsequentoccurrenceofasetofeventswiththeirtimeconstraints．Suchamethoddoesnotsupportsynchronouscommunication．Petrinetscandescribemanyconcurrencyfeatures，butitonlyisamode1．Ithasnocalculi．MethodsbasedonProcessalgebrauseinterleavingmodelstospecifyconcurrency．Typicalexamplesare，and．SuchmethodscanrepresentdetailedbehaviorofsystemsandbothCCSandCSPhavegoodalgebraicproperties．Theynotonlycanmodelbehaviorofsystems，butalsohaveareasoningcalculisystem．Tousesuchmethodsunderreal-timeenvironments，manyextensionshavebeenintroducedbymanyresearchers．SomeexamplesaretimedCCS(TCCS)，CCSwith，CSPwithdelayand，etc．In，LeeproposedanACSRframework，whichisakindoftimedprocessalgebrabasedontheCCSmode1．Thismethodincorporatessynchronous，time，resourcerequirementsandprioritiesintoCCS．Itsupportsmodularspecificationandvalidationofthesystem．Itisveryadaptivetoanal...
