Enhancing state space reduction techniques for model checking

Model-checking is een techniek voor het automatisch opsporen van fouten in en de verificatie van hardware en software. De techniek is gebaseerd op het doorzoeken van de globale toestandsruimte van het systeem. Deze toestandsruimte groeit vaak exponentieel met de grootte van de systeembeschrijving. Als gevolg hiervan is een van de voornaamste knelpunten in model-checking de zogenaamde toestandsexplosie. Er bestaan veel aanpakken om met dit probleem om te gaan. We presenteren verbeteringen van sommige bestaande technieken voor reductie van de toestandsruimte die gebaseerd zijn op expliciete enumeratie van die ruimte. We schenken vooral aandacht aan het verbeteren van verscheidene algoritmen die, hoewel ze slechts een deel van de toestandsruimte onderzoeken, nog steeds gegeven een eigenschap kunnen bewijzen of weerleggen. In het bijzonder is ons onderzoek toegespitst op twee typen reducties. Het eerste type, parti¨eleordening (PO) reductie, buit de onafhankelijkheid van acties in het systeem uit. Het tweede type is een klasse van reducties die voordeel halen uit symmetrie¨en van het systeem. De voornaamste bijdragen van dit proefschrift in verband met de parti¨ele ordening reductie zijn de volgende: – Het gebruik van systeemhi¨erarchie voor effici¨entere parti¨ele-ordening reductie door klustering van processen – De meeste model-checking technieken beschouwen het model als een platte compositie van processen. We laten zien hoe de reductie kan profiteren van de systeemstructuur door uitbuiting van de hi¨erarchie in het systeem (Hoofdstuk 2). – Correcte syntactische criteria om onafhankelijke acties te vinden voor parti¨ele ordening reductie voor systemen met synchronizerende communicaties die gecombineerd zijn met prioriteit-keuze en/of zwakke fairness (Hoofdstuk 3). – Parti¨ele-ordening reductie voor discrete tijd – We laten zien hoe het algoritme voor parti¨ele ordening reductie zonder tijd aangepast kan worden, in het geval tijd gerepresenteerd wordt middels gehele getallen (Hoofdstuk 4). De bijdragen betreffende symmetrie-gebaseerde reducties kunnen als volgt samengevat worden: – Effici¨ente heuristieken voor het vinden van representanten van equivalentieklassen voor symmetrie-gebaseerde reductie (Hoofdstuk 6). – Een effici¨ent algoritme voor model-checking onder zwakke fairness met toestandsruimte reductietechnieken die gebaseerd zijn op symmetrie (Hoofdstuk 7). Het succes van model-checking is voornamelijk gebaseerd op de relatief gemakkelijke implementatie in software gereedschappen. Bijna alle bovengenoemde theoretische resultaten zijn ge¨implementeerd in de praktijk en de ontwikkelde prototype implementaties zijn ge¨evalueerd in praktijkstudies. Het meeste implementatie werk is gerelateerd aan de model checker Spin. Van de praktische bijdragen in dit document noemen we: – DT Spin – een uitbreiding van Spin met discrete tijd die het in het proefschrift gepresenteerd discrete-tijd PO reductie algoritme bevat (Hoofdstuk 4). – if2pml – een vertaler van de modelleertaal IF naar Spins invoertaal Promela, die als het tweede deel van een vertaler van SDL naar Promela bedoeld is (Hoofdstuk 5). – SymmSpin – een symmetrie-reductie pakket voor Spin, gebaseerd op de heuristiek beschreven in dit proefschrift (Hoofdstuk 6). De implementaties zijn getest op voorbeelden uit de literatuur en het bedrijfsleven met bemoedigende resultaten. In het bijzonder noemen we MASCARA – een industrieel protocol dat draadloze communicatie met ATM combineert (Hoofdstuk 5). De experimenten zijn niet alleen een aanwijzing voor de kwaliteit van de resultaten en de implementatie, maar ze waren en zijn ook een inspiratie voor nieuw theoretisch werk. Een typerend voorbeeld is de verenigbaarheid van parti¨ele ordening reductie met prioriteit-keuze en fairness in modellen met rendez-vous communicatie. De verbetering van het parti¨ele-ordening algoritme was rechtstreeks ge¨inspireerd door experimenten met Spin en zijn discrete-tijd uitbreiding DT Spin, ontwikkeld in dit proefschrift.