ON MODEL CHECKING THE DYNAMICS OF OBJECT-BASED SOF

DINODISTEFANOOnmodelcheckingthedynamicsofobject-basedsoftwareafoundationalapproachDistefano,DinoOnmodelcheckingthedynamicsofobject-basedsoftware:afoundationalap-proach/DinoDistefano-Ph.D.thesis,UniversityofTwente,2003ISBN90-365-1975-6IPADissertationSeriesNo:2003-09CTITPh.D.thesisseriesNo:03-58TheworkinthisthesishasbeencarriedoutundertheauspicesoftheresearchschoolIPA(InstituteforProgrammingresearchandAlgorithmics)andwithinthecontextoftheCentreforTelematicsandInformationTechnology(CTIT).Publisher:TwenteUniversityPress,P.O.Box217,7500AEEnschede,theNetherlands,:OceFacilityServices,EnschedeCoverdesignbyDanielaDistefanoCopyrightcDinoDistefano,Enschede,2003Nopartofthisworkmaybereproducedbyprint,photocopyoranyothermeanswithoutthepermissioninwritingfromthepublisher.ISBN90-365-1975-6ISSN1381-3617ONMODELCHECKINGTHEDYNAMICSOFOBJECT-BASEDSOFTWARE:AFOUNDATIONALAPPROACHPROEFSCHRIFTterverkrijgingvandegraadvandoctoraandeUniversiteitTwente,opgezagvanderectormagnicus,prof.dr.F.A.vanVught,volgensbesluitvanhetCollegevoorPromotiesinhetopenbaarteverdedigenopvrijdag7november2003te16.45uurdoorDinoSalvoDistefanogeborenop20juli1973teCatania,ItalieDitproefschriftisgoedgekeurddoor:prof.dr.H.Brinksma(promotor)dr.ir.J.-P.Katoen(assistent-promotor)dr.ir.A.Rensink(assistent-promotor)Thanksto...ThankstoEdBrinksma,mypromotor,forgivingmethepossibilitytostartasPh.D.studentinhisFMTgroupfouryearsago.IhavereallyenjoyedthesparklingscienticenvironmentwhichEdhascreatedinthegroup.Althoughheisusuallyextremelybusy,hehasalwaysbeenreadytondtimetodiscusswithmeallkindsofissues.ThankstoJoost-PieterKatoenandArendRensink,mydailysupervisors.WorkingonaPh.D.thesisisoftenalonelyandfrustratingexercise.MinewouldnothavebeenanexceptionifArendandJoost-Pieterwerenotthere.Asamatteroffact,theexistenceofthisthesisismostlyduetothecontinuouscarethatIhavereceivedfrombothofthemduringtheseyears.Iwillneverforgetourshortmeetingsthatalwaysturnedintolonghoursbrainstormingatthewhite-board.AftereachofthemIwasbusyforweekstryingtoworkoutnewproblems.Itisfairtosaythatalmosttheentiretyoftheresultscontainedinthisthesisoriginatedfromthosemeetings.Duringtheyears,Joost-PieterandArendpatientlycuredmyunfortunate,sloppyattitude.Inmanydicultoccasionstheyhelpedmeand|despiteallthedisastersIwasablecomeupwith|theycontinuedtobelievethatIcouldreachtheend.Also,theytaughtmehowtotranslatethoseobscureideasIhadinmymindintoscience,andhowtocommunicatethemtoothers.Ifyouareoneofthe(un)fortunateread-ersthatwillgobeyondChapter2,andnditunreadable,trytoimaginehowitwasbeforeArendandJoost-Pieterstruggledyearsconvincingmetomakethingseasier.Iconsidermyselffortunatetohavehadtheopportunitytolearnfromthem.ThankstoMehmetAksit,JohnHatcli,AnnekeKleppe,John-JulesMeijer,andMoolySagivforacceptingthedutyofbeingmembersofthepromotioncommissionandreadthedissertation.ThankstoHolgerHermannsandPedroD'Argeniomy\paranymphs.Unfor-tunately,theyhavenotbeendirectlyinvolvedinmyresearch.However,Iliketothinkthatthelongtriptothecompletionofthisthesisstartedonceuponatime(onenightinFebruary/March1999)inaMexicanrestaurantinEnschede.TherePedroandHolgerinvitedmefordinneraftertheformalinterviewwithiiiThanksto...theseniormembersofthegroup.AlthoughaftersometimeIlearnedthatthisisthestandardhiringprocedureattheFMTgroup,thatdinnerwasstillspecial1.Thatfamousnight,helpingthemselveswithseveralCoronas2,theyconvincedmethatFMTwastherightplaceformydoctoralstudies.True.Fortunately,thefunsharedtogetherontheCorona-nightdidnotturnouttobeanisolatedcase.Onthecontrary,itwasonlythebeginning.Sincethatnight,theyhavebeenformetheepitomeoftruescientists.Inthisrespect,andonseveraloccasionsHolgerandPedrohaveinuencedmeandcontributedtowardsmydevelopmentasascientist.ThankstoTheoRuyswhohasbeenalwaysreadytoanswerawiderangeofquestions;fromscience,tobureaucracy,tomythesis.Eventhemostsillyquestions.Hewasevenabletomakemefeelunashamedof\mijnABNneder-lands.TheohasprovidedmewithsomeniceLATEXstylesthathaveimprovedtheappearanceofthethesisandtranslatedthesummary3.ThankstoJokeLammerinkwhosehelphasbeenusefulforallthosebureau-craticmattersacomputernerdhastofaceineverydaylife.Doyouhaveanyideawhatusuallyhappenswhentwentyorsocomputerscientistsareaban-donedinthosefewweeksthesecretaryisonholidayleave?Itisalwaysacatastrophe.TousethestandardFMTexample,considerthosedeadlocksit-uationslike:entireweeksspentwithcoeewithoutsugar;orsugarwithoutcoee;orwithcoeeandsugarbutnocoee-lters;etc.Ifthisisnotenoughyoucantrytomakesomefancypermutationsoftheterms:coee,sugar,with,without,|andalso|reisdeclaratie,werkgeversverklaring.ThankstoRicKlaren,myocemate,whosavedmeinseveraloccasionsfrommywell-establishedinabilitytocopewithcomputers,operatingsystems,finddirwhereithastocomefromjxargsln-s,shellscripts,installations,fancytools,andsoon.ThankstoJohnHatcliandMattDwyerforhavingprovidedmewiththepossibilitytospendthreeinspiringmonthsatKansasStateUniversity.There,Ibecameawareandinterestedinabstraction,whichbroadenedmyviewonthisresearcheld.ThankstoRaduIosifandGeorgJungforinte