Real Time Systems Strati cation, Convergence and T

RealTimeSystems:Stratiation,ConvergeneandTransieneSupratikMukhopadhyay1AndreasPodelski1RajdeepNiyogi21MaxPlankInstitutfurInformatik,ImStadtwald,66123Saarbruken(Germany)fsupratik,podelskigmpi-sb.mpg.de2IndianInstituteofTehnologyKharagpur,Indiarajdeepse.iitkgp.ernet.inAbstratFirst,weintroduestratiedtimedlogiproesses(STLP’s)formodelingstratiedorhierarhialrealtimesystems.Seond,wepresentanalgorithmfordetetingonvergeneofrealtimesystemsbyreduingtheproblemtothatofomputingmodeltheoretisemantisofstratiedtimedlogiproesses.Third,wedeneformallyanotionoftransieneforrealtimesystemsharaterizingthetransientbehaviorofsuhsystems.Wealsopresentanalgorithmfordetetingwhetherarealtimesystemhasatransientbehavior.1IntrodutionRealtimesystemshavebeenthetargetofextensiveamountofresearhintheveriationommunityforthelastfewyears(seee.g.,[AD94,LPY95,DT98,HNSY94℄).Aplethoraofmodelshavebeenproposedforapturingrealtimee.g.,thetimedautomatonmodel[AD94℄,thetimedtransitionsystemmodel[HMP91℄,thetimedproessalgebramodel[Yi91℄,thetimedPetrinetmodel[BD91℄.Butstritlyspeaking,noneofthesemodelshavebeenlogi-based.Aneetofthislakofinspirationfromlogiinthesemodelshavebeenthatmostoftheveriationalgorithmsarefousedmoreondatastrutureaspets(e.g.,BDD’s)ratherthandrawinginspirationfrom(andfousingon)tehniquesbasedonlogi.ButasImmermanpointsoutin[Imm98℄thatmodelhekinganddatabasequeryevaluationareessentiallythesamething.Hene,thesametehniquesfrommodeltheoryanddatabases,thataresoeetiveinthelattersetting,shouldretaintheireetivenessintheformeraswell.WhiletehniquesfromnitemodeltheoryhavebeensuessfullyappliedtodesigneÆientalgorithmsformodelhekingfornitestatesystems[IV97,AI99,GGV99,RRR+97℄,theyareunlikelytoahievesuhresultswhenappliedtosystemswithinnitestatespaeslikerealtimesystemsoronstraintdatabases.Tworeentextensionsofnitemodeltheoryviz,metanitemodeltheory[GG97℄andnitelyrepresentablemodeltheory[GS95℄,havebeenproposedfordealingwithsuh\innitestatesystems.Ofthese,theformerallowsonlyrestritedaesstotheinnitenumerialdomain,andhene,doesnotseemtobesuitablefordealingwithrealtimesystemswhihrequireanintimateaesstotheinnitetimedomain.FinitelyrepresentableThispaperonsistsof19pagesoftextand4pagesofAppendix.Ithasbeenwritteninmoredetailthanaonferenepapershouldbe.Ifaepted,thepaperwillbeshortened.1modeltheoryontheotherhand,whilebeingabletodealwith\innitestatesystemslikeonstraintdatabases[KKR95℄,notonlywitnesses(likeitsniteounterpart)thefailureoflassialtoolsfrommodeltheoryliketheompatnesstheorem[GS95℄,butalso,(unlikeitsniteounterpart)ofthefailureoftoolslikeloality[Gai93℄and0=1laws[Fag76℄;hene,newtoolsthatexpliitlydealwithnitelyrepresentablestruturesneedtobedeveloped.Itisnottheintentionofthispapertodevelopnewtehniquesfordealingwithsuhnitelyrepresentablestrutures[GS95℄.Rather,weshowhowthealready-existingtehniquesfordealingwithnitelyrepresentablestrutureslikeonstraintdatabasesanbeusedformodelingandveriationofrealtimesystems.Ourontributionsinthispaperareasfollows:First,weextendtheTimedLogiProess(TLP)modelforrealtimesystemsintroduedin[MP99℄toinorporatestratied(orasadehierarhial)realtimesystems(seesetion2.3).Tobepreise,weidentifystratiedTLP’sasafragmentofonstraintquerylanguagesoverreals[KKR95,JM94,Rev90,Rev95℄abletomodelasadehierarhialrealtimesystems1.Ithasbeenourobservationthatmulti-stageasadesystems(likemulti-stagerokets)arebettermodeledasstratiedsystemsratherthanasmonolithiones2.Astratiedmodelingreduesthelogialomplexityofadesignbyallowingadesignertoreasonaboutherdesignhierarhially,onestageatatime.Itallowsthedesignertospeifysystemsbystep-wiserenement,andtoviewitatdierentlevelsofgranularity.Moreoveritreduestheomplexityofveriationbyreduingtheveriationproblemforthewholesystemtothatforeahstageseparatelyandthenarryingovertheresultstothenexthigherstages.Noneofthemodelsofrealtimesystemsdesribedabovesupportstratiedreasoning.StratiedTLP’sprovideaninterleavingmodelforasadehierarhialrealtimesystems.Theyansimulatehierarhialrealtimesystems\lok-step,atanarbitraryabstrationlevel.Unlikethemodelsofrealtimesystemsdesribedabove,thestratiedTLP(STLP)modelisalogi-basedmodel.Beingalogi-basedmodel,STLP’seasetheomplexityofthedesignbyallowingadesignertoreasonaboutherdesignatahigherabstrationlevel{separatingthehighlevellogialpartfromthelowlevelontrolowpart.Itfailitates\rapiddesignbyallowingadesignertoreasonaboutherdesigndelaratively{asasetofaxioms.Moreover,beingafragmentofonstraintquerylanguagesoverreals[JM94,KKR95,Rev90,Rev95℄,STLP’ssupportpreisemathematialsemantisbasedonrst-orderorxpointlogiwithonstraintsoverrealswhihfailitatesformalanalysisofsystembehaviors(notethatonstraintquerylanguagesoverrealsandheneSTLP’sarefragmentsofxpointlogiwithonstraintsoverreals).STLP’salsosupport\alternation(thoughinarestritedform),whihisnotsupportedbyanyofthemodelsforrealtimesystemsdesribedabove(omparethereentmodeloftimedalternatingtreeautomata[DW99℄),andheneareabletomodel\openstratiedrealtimesystems.Ourseondontributioninthispaperisthatwereduetheproblemofdetetingonvergene(a.k.a.zenoness[HNSY94℄