Model Checking Timed Automata - Techniques and App

ModelCheckingTimedAutomataTechniquesandApplicationsMartijnHendriksCopyrightc2006MartijnHendriks,Oosterhout,TheNetherlandsISBN90-9020378-8IPAdissertationseries2006-06TypesetwithLATEX2εPrintedbyPrintPartnersIpskamp,EnschedeTheworkinthisthesishasbeencarriedoutundertheauspicesoftheresearchschoolIPA(InstituteforProgrammingresearchandAlgorithmics).IthasbeensupportedbytheEuropeanCommunityProjectIST-2001-35304AMETIST.ModelCheckingTimedAutomataTechniquesandApplicationseenwetenschappelijkeproeveophetgebiedvandeNatuurwetenschappen,WiskundeenInformaticaProefschriftterverkrijgingvandegraadvandoctoraandeRadboudUniversiteitNijmegenopgezagvandeRectorMagnificusprof.dr.C.W.P.M.Blom,volgensbesluitvanhetCollegevanDecaneninhetopenbaarteverdedigenopdinsdag4april2006desnamiddagsom3.30uurpreciesdoorMartijnHendriksgeborenop20augustus1976teCanberra,Australi¨ePromotor:Prof.dr.FritsW.VaandragerManuscriptcommissie:Prof.dr.RajeevAlur,UniversityofPennsylvania,UnitedStatesProf.dr.ir.Joost-PieterKatoen,RWTHAachenUniversity,GermanyDr.SergioYovine,CNRS,FrancePrefaceFirstofall,IthankFritsVaandragerandJozefHoomanforconvincingmetoworkonaPhDprojectandforprovidingaveryfreeandstimulatingatmosphereforresearch:Ihavelearnedalottheselastfouryears!FormostofmytimeasaPhDstudentIhavebeenworkingintheAMETISTprojectwhichgavemetheopportunitytomeetandinteractwithawholegroupofinternationalresearchersduringthebi-oreventri-annualmeetingsinniceplaces.IthankallAMETISTpeoplefortheseinspiringmeetings.Theresearchpaperscon-stitutingthisthesisoriginatenearlyallfromtheAMETISTprojectandwouldnothaveexistedwithoutmyco-authors.GerdBehrmann,EdBrinksma,LingCheung,KimLarsen,AngelikaMader,PeterNiebert,BarendvandenNieuwelaar,FritsVaandragerandMarcelVerhoef,thankyou!Furthermore,Iwanttothanktheread-ingcommittee,RajeevAlur,Joost-PieterKatoenandSergioYovine,fortheireffortandforprovidingmanyusefulcommentsthathaveimprovedthisthesis.Thedailylifeonthe6thfloorisverypleasant.IthankallpeoplefromtheITAandSOSgroupsforthisniceenvironment.IespeciallythankMir`eseWillems,MariavanKuppenveldandDesireeHermansfortheirhelpwiththemanypracticalproblems.IalsothankHarcoKuppensforhishelpwiththeoftenoccurringcom-puterdifficulties.WithouthishandcraftedbackuputilitythatraninparallelwiththeC&CZbackup(thatcannotalwaysbetrustedasIexperienced...),Iwouldhavehadtoretypethiswholethesisduringthelastfall.DuringmystayintheITTgroupIhavealsoparticipatedinsometeachingactiv-itieswhichIfoundveryinterestinganduseful.ThereforeIthankHannoWupper,HansMeijerandStijnHoppenbrouwersforgivingmetheopportunitytogathersometeachingexperienceintheBewerenenBewijzencourse.Inthecurriculumvitaethatisincludedattheendofthisbook,youcanreadthatIstartedoutstudyingchemistry.ThatdidnotworkoutverywellandIdecidedtoswitchtocomputerscience.ThisprovedtobeaverygoodchoiceandIthankmyfamilyforsupportingit.Femke,thankyouforyourlove.viPREFACEContentsPrefacev1Introduction11.1TheQualityofComputerSystems.................11.2ModelChecking...........................21.3OverviewofthisThesis.......................51.4Conclusions.............................82ExactAccelerationofReal-TimeModelChecking112.1Introduction.............................112.2TimedAutomata..........................122.3PredictableDelaysofEdgeSequences...............142.4AccelerationofTimedAutomata..................182.5ExperimentalResults........................222.6Conclusions.............................263EnhancingUppaalbyExploitingSymmetry293.1Introduction.............................293.2ATheoryofSymmetry.......................313.3FromUppaaltoSUppaal......................333.4ExtractionofAutomorphisms....................463.5Conclusions.............................694AddingSymmetryReductiontoUppaal714.1Introduction.............................714.2ModelCheckingandSymmetryReduction.............734.3AddingScalarsetstoUppaal....................754.4UsingScalarsetsforSymmetryReduction.............764.5ExperimentalResults........................884.6Conclusions.............................905ModelCheckerAidedDesignofaControllerforaWaferScanner935.1Introduction.............................935.2TheEUVMachine.........................965.3LeastRestrictiveDeadlockAvoidancePolicy...........975.4ThroughputAnalysis........................1045.5Conclusions.............................116viiiCONTENTS6ProductionSchedulingbyReachabilityAnalysis1196.1Introduction.............................1196.2SchedulingwithTimedAutomata.................1206.3DescriptionoftheCaseStudy...................1216.4ModelingwithTimedAutomata..................1236.5ModelCheckingExperiments...................1286.6StochasticAnalysis.........................1316.7EvaluationandConclusion.....................1317ModelCheckingtheTimetoReachAgreement1337.1Introduction.............................1337.2TimedAutomata..........................1357.3DescriptionoftheAlgorithm....................1367.4VerificationoftheTimeoutTask..................1387.5VerificationoftheAlgorithm....................1417.6Conclusions.............................14