搜索
ComposableModelsforTimingandLivenessAnalysisinDistributedReal-TimeEmbeddedSystemsMiddlewareVenkitaSubramonianandChristopherGill C´esarS´anchezandHennyB.Sipma venkita,cdgill @cse.wustl.edu cesar,sipma @cs.stanford.eduCSEDepartment,WashingtonUniversity,St.Louis,MOCSDepartment,StanfordUniversity,Stanford,CAAbstractMiddlewarefordistributedreal-timeembedded(DRE)systemshasgrownincreasinglycomplex,toaddressfunctionalandtemporalrequirementsofdiverseapplications.Whilecurrentapproachestomodelingmiddlewarehaveeasedthetaskofassembling,deployingandconfiguringmiddlewareandtheapplicationsthatuseit,alower-levelsetofformalmodelsisneededtouncoversubtletimingandlivenesshazardsintroducedbyinterferencebetweenandwithindistributedcomputations,particularlyinthefaceofalternativemiddlewareconcurrencystrategies.Inthispaper,weproposetimedautomataasaformalmodeloflow-levelmiddlewarebuildingblocksfromwhichavarietydifferentmiddlewareconfigurationscanbeconstructed.Whencombinedwithanalysistechniquessuchasmodelchecking,thisformalmodelcanhelpdevelopersinverifyingthecorrectnessofvariousmiddlewareconfigurationswithrespecttothetimingandlivenessconstraintsofeachparticularapplication.Keywords.Model-drivenMiddleware,EmbeddedSystemsMiddleware,FormalMiddleware.TechnicalArea.OperatingSystemsandMiddleware1IntroductionSignificantresearchoverthepastdecadehasmademiddlewaremorecustomizablethroughtheuseofpattern-orientedsoftwareframeworks[1,2].Althoughthishasmademiddlewaresolutionssuitableforawiderrangeofapplications,managingtheresultingmultiplicityofcustomizationoptionshasbecomeanincreasingconcern.Toallowmiddlewaretobecustomizedtomeetthestringentdemandsofdifferentdistributedreal-timeembedded(DRE)applications,recentresearchhasfocusedonapplyingmodel-driventech-niquestoDREmiddleware[3].Althoughcurrentmodel-drivenmiddlewareapproachesfacilitatethecorrectassembly,deploymentandconfigurationofDREapplicationsandmiddleware,weargueinthispaperthatamoredetailedandformalbasisforreasoningabouttimingandlivenesspropertiesinavarietyofdifferentmiddlewareconfigurationsisbothnecessaryandpossible.Formalmodelshavebeenusedtouncoverhigh-leveldesignflawsearlyinsystemdevelopment[4,5].However,suchmodelsarecurrentlydifficulttomaintainadequatelyasthesystem’sspecificationisrefinedsuccessivelythroughoutthesystemdevelopment ThisresearchwassupportedinpartbyNSFCAREERawardCCF-0448562. ThisresearchwassupportedinpartbyNSFgrantsCCR-01-21403,CCR-02-20134,CCR-02-09237,CNS-0411363,andCCF-0430102,AROgrantDAAD19-01-1-0723,andNAVY/ONRcontractN00014-03-1-0939.1life-cycle.Forexample,decisionsregardingthedeploymentofapplicationcomponentsontoend-systems,orthechoiceofmiddlewareconcurrencystrategies,oftenarenotreflectedinthesehigh-levelmodels.Thismayresultinsubtletimingandlivenesshazardsfromunexpectedinterferencebetweenthemiddlewarepoliciesandmechanismsusedbyasetofdistributedcomputations.ServiceRequestor ServiceProvider Channel Channel Channel Channel event demultiplexer Channel event demultiplexer Send Request Receive Request Event-driven Event-driven Event-driven Time-driven Figure1.RemoteFunctionCallasaTimeandEvent-drivenInteractionFigure1showshowasystemthatisspecifiedwithonlytime-drivenconstraintsinitshigh-levelmodelmayberefinedintoatimeandevent-drivensystemduringitsdesignandimplementationphases.Inthehigh-levelmodel,apurelytime-triggeredrequestissentfromaservicerequestertoaserviceproviderthroughamiddleware-implementedremotefunctioncall.However,theimplementationofthisremotefunctioncallgoesthroughmultiplemiddleware,OSandnetworkprocessingstacks,eachofwhichlikelycontainsevent-drivensystemelements.Forexample,Figure1showsmiddlewarebasedeventdemultiplexersonthesenderandreceiverside,whichenableasinglethreadoneachsidetobeusedtodemultiplexI/Oevents(e.g.,packetarrivalsandtransmissions)fromandontomultipleinteractionchannels(e.g.,socketsandpipes).Eventheinteractionchannelsarelikelytobeeventdriven,forexamplewhenIPpacketsarriveandaremovedfromthenetworkinterfacecardintoanapplication-accessibletransport-layerbuffer.Thisexampleillustratesthegeneralconcernthatmanyoftheabstractionsusedduringhigh-levelmodeling,suchasthenotionofapurelytime-driveninteractionbetweentheservicerequesterandtheserviceprovider,maybecomedecreasinglyrepresentativeofthesystemduringitsdesignandimplementation.Thismayinturnresultinachasmbetweenthehigh-levelmodelandtheactualimplementation,unlesstheabstractionsusedinthehighlevelmodelcanberefinedduringdesignandimplementation.Thus,afoundationalsetofformalmodelsthatcanexpressboth(1)high-levelabstractionssuchastimedremotemethodinvocations,and(2)low-levelrefinementssuchasconcurrencyandinteractionsemanticsbetweentheobjectsthatimplementthehigh-levelmodel,isneededtosupportverificationofthehighlevelmodelintermsofitslow-leveldesignandimplementation.Furthermore,theinsightsobtainedfrommodelingandanalysisshouldbemadeavailableandusedwhilemakingdesignandde-velopmentdecisions,andvice-versa.Suchaclosecorrespondencebetweenthesystemmodeling,analysis,designanddevelopmentactivitiesoffersthefollowingbenefits:(1)morecomplete,detailedandexecuta