Cet ouvrage fait partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour le lire en ligne
En savoir plus

Model checking nondeterministic and randomly timed systems [Elektronische Ressource] / by Martin Richard Neuhäußer

De
268 pages
ModelCheckingNondeterministicandRandomlyTimedSystemsMartinR.Neuha¨ußerGraduationcommittee:Prof.Dr.Ir.A.J.Mouthaan UniversityofTwente,(chairman) eNetherlandsProf.Dr.Ir.Joost-PieterKatoen RWTHAachen/UniversityofTwente,(promotor) Germany/eNetherlandsDr.Marie¨lleI.A.Stoelinga UniversityofTwente,eNetherlands(referent)Prof.Dr.JosC.M.Baeten EindhovenUniversityofTechnology,eNetherlandsProf.Dr.Ir.BoudewijnR.Haverkort UniversityofTwente,eNetherlandsProf.Dr.-Ing.HolgerHermanns SaarlandUniversity,GermanyProf.Dr.JacoC.vandePol UniversityofTwente,eNetherlandsProf.Dr.RobertoSegala UniversityofVerona,ItalyIPADissertationSeries????-??.CTITPh.D.-esisSeriesNo.??-???,ISSN????-????.ISBN:???-??-???-????-?.eresearchreportedinthisdissertationhasbeencarriedoutundertheauspicesoftheInsti-tuteforProgrammingResearchandAlgorithmics(IPA)andwithinthecontextoftheCenterforTelematicsandInformationTechnology(CTIT).eresearchfundingwasprovidedbytheNWOGrantthroughtheproject:VerifyingQuantitativePropertiesofEmbeddedSo?ware(QUPES).Translationoftheabstract:VietYenNguyen(MSc).ATypesetinLTX.ECoverdesign:AnjaBalsfullandPublisher:Wo¨hrmannPrintService-http://www.wps.nl.Copyright©????byMartinR.Neuha¨ußer,Aachen,Germany.MODELCHECKINGNONDETERMINISTICANDRANDOMLYTIMEDSYSTEMSDissertationtoobtainthedoctor’sdegreeattheUniversityofTwente,ontheauthorityoftherectormagni?cus,Prof.Dr.H.Brinksma,onaccountofthedecisionofthegraduationcommitteetobepubliclydefendedonFriday,January??,????at??:?
Voir plus Voir moins

ModelCheckingNondeterministicand
RandomlyTimedSystems
MartinR.Neuha¨ußerGraduationcommittee:
Prof.Dr.Ir.A.J.Mouthaan UniversityofTwente,
(chairman) eNetherlands
Prof.Dr.Ir.Joost-PieterKatoen RWTHAachen/UniversityofTwente,
(promotor) Germany/eNetherlands
Dr.Marie¨lleI.A.Stoelinga UniversityofTwente,eNetherlands
(referent)
Prof.Dr.JosC.M.Baeten EindhovenUniversityofTechnology,eNetherlands
Prof.Dr.Ir.BoudewijnR.Haverkort UniversityofTwente,eNetherlands
Prof.Dr.-Ing.HolgerHermanns SaarlandUniversity,Germany
Prof.Dr.JacoC.vandePol UniversityofTwente,eNetherlands
Prof.Dr.RobertoSegala UniversityofVerona,Italy
IPADissertationSeries????-??.
CTITPh.D.-esisSeriesNo.??-???,ISSN????-????.
ISBN:???-??-???-????-?.
eresearchreportedinthisdissertationhasbeencarriedoutundertheauspicesoftheInsti-
tuteforProgrammingResearchandAlgorithmics(IPA)andwithinthecontextoftheCenterfor
TelematicsandInformationTechnology(CTIT).eresearchfundingwasprovidedbytheNWO
Grantthroughtheproject:VerifyingQuantitativePropertiesofEmbeddedSo?ware(QUPES).
Translationoftheabstract:VietYenNguyen(MSc).
ATypesetinLTX.E
Coverdesign:AnjaBalsfulland
Publisher:Wo¨hrmannPrintService-http://www.wps.nl.
Copyright©????byMartinR.Neuha¨ußer,Aachen,Germany.MODELCHECKING
NONDETERMINISTICAND
RANDOMLYTIMEDSYSTEMS
Dissertation
toobtainthedoctor’sdegree
attheUniversityofTwente,ontheauthorityof
therectormagni?cus,Prof.Dr.H.Brinksma,
onaccountofthedecisionofthegraduationcommittee
tobepubliclydefended
onFriday,January??,????at??:??
by
MartinRichardNeuha¨ußer
bornon??September????
inKulmbach,Germanyedissertationhasbeenapprovedbythepromotor:
Prof. Dr.Ir.Joost-PieterKatoenModelCheckingNondeterministicand
RandomlyTimedSystems
VonderFakulta¨tfu¨rMathematik,Informatikund
Naturwissenscha?enderRheinisch-Westfa¨lischenTechnischen
HochschuleAachenzurErlangungdesakademischenGrades
einesDoktorsderNaturwissenscha?engenehmigteDissertation
vorgelegtvon
Diplom-Informatiker
MartinRichardNeuha¨ußer
aus
Kulmbach
Berichter: Prof.Dr.Ir.Joost-PieterKatoen
Prof.Dr.FranckvanBreugel
¨ ¨TagdermundlichenPrufung:??.Januar????
DieseDissertationistaufdenInternetseitenderHochschulbibliothekonlineverfu¨gbar.Abstract
Formalmethodsinitiallyfocusedonthemathematicallyprecisespeci?cation,designand
analysisoffunctionalaspectsofso?wareandhardwaresystems.Inthiscontext,model
checkinghasprovedtobetremendouslysuccessfulinanalyzingqualitativeproperties
ofdistributedsystems. isobservationhasencouragedpeopleinthe?eldofperfor-
manceanddependabilityevaluationtoextendexistingmodelcheckingtechniquesto
alsoaccountforquantitativemeasures.Asaresult,nowadays,theautomaticanalysisof
Markovianmodelshasbecomeanindispensabletoolforthedesignandevaluationof
safetyandperformancecriticalsystems.
Markovianmodelsareclassi?edaccordingtotheirunderlyingnotionoftime,being
eitherdiscreteorcontinuous. Inthediscrete-timesetting,Markovdecisionprocesses
areanondeterministicmodelwhichiswidelyknowninmathematics,computerscience
andoperationsresearch. Moreover,e?cientalgorithmsareavailablefortheiranalysis.
isstandsinsharpcontrasttothecontinuous-timesetting,wherenotechniquesexist
toanalyzemodelsthatcombinestochastictimingandnondeterminism.Inthepresent
thesis,webridgethisgapandproposequanti?ablyprecisemodelcheckingalgorithms
foravarietyofnondeterministicandstochasticmodels.
We?rstconsidercontinuous-timeMarkovdecisionprocesses(CTMDPs).Touniquely
determinethequantitativepropertiesofaCTMDP,allitsnondeterministicchoicesmust
beresolvedaccordingtosomestrategy.erefore,weproposeahierarchyofscheduler
classesandinvestigatetheirimpactontheachievableperformanceanddependability
measures. Inthiscontext,weidentifylateschedulers,whichresolvethenondetermin-
ismasneatlyaspossible.Apartfromtheirinterestingtheoreticalproperties,theyfacili-
tatetheanalysisoflocallyuniformCTMDPsconsiderably.InalocallyuniformCTMDP,
thetiminginastateisindependentofthescheduler.isobservationculminatesinan
e?cientandquanti?ablypreciseapproximationalgorithmforlocallyuniformCTMDPs.
IncontrasttoCTMDPswhichcloselyentanglenondeterminismandstochastictime,
interactiveMarkovchains(IMCs)areahighlyversatilemodelthatstrictlyuncouplesthe
twoaspects.Duetothisseparationofconcerns,IMCsarelocallyuniformbyde?nition.
isallowsustoapplyanalysistechniqueswhicharesimilartothosethatwedeveloped
forlocallyuniformCTMDPs,alsotoIMCs.Inthisway,wesolvetheopenproblemof
modelcheckingarbitraryIMCs.
Inthenextstep,wereturntoCTMDPsandprovethattheycanbetransformedinto
alternatingIMCsinameasurepreservingway.Asourproofdoesnotrelyonlocaluni-
formity,itenablestheanalysisofquantitativemeasuresonarbitraryCTMDPsbymodel
checkingtheirinducedIMCs. However,theunderlyingschedulerclassslightlydi?ersviii
fromthelateschedulersthatweusedinitially.Infact,itcoincideswiththetime-andhis-
torydependentschedulersthatareproposedintheliterature.us,ourresultforIMCs
alsosolvesthelongstandingproblemofmodelcheckingarbitraryCTMDPs.
However,theapplicabilityofmodelcheckingislimitedbytheinfamousstatespaceex-
plosionproblem:Evensystemsofmoderatesizeo?enyieldmodelswithanexponentially
largerstatespacethatfoilstheiranalysis.Totacklethisproblem,manytechniqueshave
beendevelopedthatminimizethestatespacewhilepreservingimportantpropertiesof
themodel.Inprocessalgebras, bisimulation minimizationidenti?esprocesseswiththe
samequantitativebehaviorandreplacesequivalentonesbyasinglerepresentative.De-
pendingontheredundancyinthemodel,thiscanleadtoenormousreductionsinthe
sizeofthestatespace. AsIMCshaveaprocessalgebraicbackground,itisnotsurpris-
ingthatbisimulationminimizationisreadilyavailableforthem.However,thisisnotthe
caseforCTMDPs. atiswhyweintroducebisimulationminimizationforCTMDPs
andprovethatitpreservesallquantitativemeasures.
Finally,weapplytheachievedresultsandproposeanalternativesemanticsfor gener-
alizedstochasticPetrinets(GSPN),whichavoidstheshortcomingsofearlierde?nitions
thatwereneededtoruleoutnondeterministicchoices.Moreprecisely,wetransforma
GSPNmodelintoanequivalentIMCwhichcanbemodelchecked.
Toshowtheapplicabilityofourapproach,weanalyze the dependabilityof a worksta-
tion clusterwhichismodeledbyanondeterministicGSPN.ecomparisonofourre-
sultswiththosethatareavailableintheliteratureisilluminating:Whenthelatterwere
published,noanalysistechniquefornondeterministicandrandomlytimedsystemswas
available.erefore,thenondeterministicchoicesintheGSPNmodelwerereplacedby
staticprobabilitydistributions.
Formeasuresthataremostlyindependentoftheschedulingpolicy,ourresultscoin-
cidewiththoseintheliterature. However,forothermeasures,choosingantagonistic
schedulersmitigatestheinferreddependabilitycharacteristicofthesystemthatwestudy
byupto??%.esefalsepositivesintheearlieranalysesclearlyprovethenecessityof
nondeterministicmodelinginthe?eldofperformanceanddependabilityanalysis.Samenvatting
Formelemethodenwordenvanoudshertoegepastmeteenwiskundigrigoureuzebena-
deringvanspeci?catie,ontwerpenanalysevanfunctioneleaspecteninhard-enso?ware.
Metnamemodelcheckingbleekenormsuccesvoltezijnomkwalitatieveeigenschappen
vangedistribueerdesystementeanalyseren.Ditmoedigdeonderzoekersinperforman-
ceevaluatieenbetrouwbaarheidsanalyseaanomdiezelfdetechniekentebenuttenvoor
kwantitatieveanalyses.AlsgevolgdaarvanisdeautomatischeanalysevanMarkovmo-
delleneenonmisbaarmiddelgewordenvoorhetontwerpenevaluatievanbetrouwbare
systemen.
Markovmodellenwordendoorgaansgeclassi?ceerdaandehandvanhunonderliggen-
deinterpretatievantijd,hetzijdiscreetofcontinu.Betre?endeheteerstgenoemde,zijn
Markovdecisionprocesseswijdverspreidindewiskunde,informaticaenoperationele
research.Erzijne?cie¨ntealgoritmenbeschikbaaromdezemodellenteanalyseren.Dit
staatinscherpcontrastmethaarcontinue-tijdstegenhanger.Erwarentothedennoggeen
techniekenontwikkeldvoormodellenmetstochastischetimingennon-determinisme.
Inditproefschri?overbruggenwedezetekortkomingmetonzebehandelingvankwan-
titiefpreciezemodelcheckingalgoritmesvooreenscalavannon-deterministischeen
stochastischemodellen.
WebehandeleneerstContinuous-TimeMarkovDecisionProcesses(CTMDPs).Om
dekwantitatieveeigenschappenvaneennon-deterministischmodeltebepalenmoeten
allenon-deterministischekeuzesvastgelegdwordenvolgenseenstrategie.Omdiereden
presenterenwijeenhierarchievanschedulerklassesenonderzoekenwijhunimpactop
performanceenbetrouwbaarheidsmaten.Indezecontextidenti?cerenwedeklassevan
”lateschedulers”. Naasthuninteressantetheoretischeeigenschappen,faciliterenzijde
analysevanlokaaluniformCTMDPs.Voordezeschedulersenmodellenpresenterenwe
namelijkeenpreciesbenaderingsalgoritme.
IntegenstellingtotCTMDPs,waarbijnon-determinismeenstochastischetijdsterk
verstrengeldzijn,zijnInteractiveMarkovChains(IMCs)eenextreemveelzijdigforma-
lismewaarindezetweeaspectenzijnontkoppeld.DoordezeontkoppelingzijnIMCsper
de?nitielokaaluniform.Detechniekendiewehebbenontwikkeldvoorlokaaluniform
CTMDPszijnconceptueelvergelijkbaarmetdievoorIMCs.Opdezewijzehebbenwe
hetopenstaandemodelcheckingprobleemvanIMCsopgelost.
VervolgenslatenwezienhoeCTMDPsa2eeldbaarzijnopalternerendeIMCswaarbij
dematenbehoudenblijven. OnsbewijsvanditresultaatvereistnietdatdeCTMDP
lokaaluniformis. DitmaaktkwantitatieveanalysesmogelijkvooralgemeneCTMDPs
doorhungeinduceerdeIMCsteanalyseren.Deschedulerklassediehierbijnodigiswijktx
enigszinsafvandiewegebruiktenomlokaaluniformCTMDPsteanalyseren. Sterker
nog,dieafwijkendeklassevaltsamenmetdetijds-enhistoriea8ankelijkeschedulers
diebekendzijnindeliteratuur.Deresultatenlossenderhalveeenlangdurigopenstaand
probleemop,namelijkhetmodelcheckenvanarbitraireCTMDPs.
Detoepassingvanmodelcheckingisechtergelimiteerddoordefameuzeexplosievan
detoestandsruimte.Zelfssystemenvangemiddeldecomplexiteitleidenvaaktoteenex-
ponentieelgroeiendetoestandsruimtewathetmodelcheckenbemoeilijkt.Omditpro-
bleemaantepakkenzijnerveletechniekenontwikkelddiedetoestandsruimteminima-
liserenterwijlhaareigenschappenintactblijven.Inprocesalgebra’sidenti?ceertbisimu-
latieminimalisatiedeprocessendieeenzelfdekwantitatiefgedragvertonenenvervangt
dezedooreenenkelrepresentatiefgedrag.A8ankelijkvanderedundantieinhetmodel
kandetoestandsruimteaanzienlijkreduceren. AangezienIMCsalsbasisdienenvoor
stochastischeprocesalgebra’sishetnietverwonderlijkdaterreedsbisimulatieminimali-
satietechniekenvoorIMCsbestaan.DitisechterniethetgevalvoorCTMDPs.Daarom
onderzochtenwijtevensbisimulatieminimalisatievoorCTMDPsenbewijzendatdie
allekwantitatievematenintacthoudt.
Tenslottepassenweonzeresultatentoeenpresenterenweeenalternatievesemantiek
voorgeneralizedstochasticPetrinets(GSPNs). Dezevermijdtdetekortkomingenvan
voorgaandede?nitiesindeliteratuurdienodigwarenomnon-deterministischekeuzes
teomzeilen.HiertoebeeldenweeenGSPNmodelafophaarequivalenteIMCmodeldie
vervolgensmetonzetechniekengemodelchecktkanworden.
Terdemonstratievanonzeaanpak,analyserenwijdebetrouwbaarheidvaneenwork-
stationclusterdiegemodelleerdisalseenniet-deterministischeGSPN.Eenvergelijking
vanonzeresultatenmetdieuitdeliteratuurlevertenkeleinteressantebevindingenop.
Hierdientvermeldtewordendatdeeerdergepubliceerderesultatenverkregenzijndoor
niet-deterministischekeuzemomentendooruniformekansverdelingentevervangen.
Voormatendiegrotendeelsona8ankelijkzijnvandeschedulingtactiek,komenonze
resultatenovereenmetdebestaande.Echter,vooranderematenleidtdekeuzevananto-
gonistischeschedulerstoteenverslechteringvandeverkregenbetrouwbaarheidskarak-
teristiekenmetmaarliefst??%.Dezeuitkomstentonendenoodzaakvanhetmeenemen
vanniet-deterministischekeuzesindeprestatie-enbetrouwbaarheidsanalyseonomsto-
telijkaan.