Het schrijven van foutenvrije computerprogramma's (software) blijkt nog steedsudgeen eenvoudige opgave. Incorrecte software kan aanleiding geven tot ongewenste,udkostbare en soms zelfs levensbedreigende situaties. Parallelle programma's, datudwil zeggen programma's geschreven voor een systeem bestaande uit meerdere,udtegelijkertijd opererende processoren, zijn in dit opzicht alleen maar lastiger: deudinteractie tussen de verschillende processoren compliceert de zaak.udHet vastleggen van de eigenschappen waaraan een programma moet voldoenudgebeurt door middel van het opstellen van een (formele) specicatie. Een vanudde methoden om te garanderen dat een programma voldoet aan zijn specicatieudis het leveren van een (wiskundig) bewijs hiervan. Het formaat waarin zo'n be-udwijs wordt gegeven alsmede de geldigheid van de atomaire bewijsstappen wordenudbeschreven door zogenaamde programmalogica's, ofwel logica's waarin naast deudgebruikelijke beweringen (bijvoorbeeld over variabelen) ook de syntax van deudprogrammeertaal een rol speelt.udDit proefschrift richt zich op een specieke klasse van programmalogica's, ookudwel Hoare-logica's genoemd naar een van de pioniers op het gebied.udGlobaal gezien bestaat het proefschrift uit twee delen. Het eerste deel startudmet een algemene inleiding in kennislogica. Kennislogica kan ruwweg wordenudbeschouwd als eerste orde logica waaraan een modaliteit is toegevoegd die eenud(geformaliseerde notie van) kennis beschrijft.udHet volgende hoofdstuk geeft een overzicht van een aantal manieren waarop ditudkennisbegrip vormgegeven kan worden in de context van gedistribueerde, of pa-udrallelle systemen. Door datgene wat een processor kan observeren met betrekkingudtot een complete executie van het gehele systeem van processoren te vari?eren,udverkrijgen we een aantal noties van kennis (binnen een gedistribueerd systeem);udbinnen deze verschillende kennisnoties kunnen we dan een klassicering aanbren-udgen met betrekking tot de kracht van die noties.udHet laatste hoofdstuk van het eerste deel beschrijft een bewijssysteem met be-udhulp waarvan beweringen met betrekking tot de kennis van processoren in eenud191?192 SAMENVATTINGudgedistribueerd systeem kunnen worden afgeleid. Het bewijssysteem, overigensudalle bewijssystemen in dit proefschrift, is compositioneel wat er in grote lijnen opudneerkomt dat de correctheid van het complete parallelle programma kan wordenudafgeleid uit de correctheid van de afzonderlijke componenten.udIn het tweede deel beschouwen we bewijssystemen voor programma's waarin deudcommunicatie tussen de verschillende componenten van een parallel systeem (deudprocessen) niet gelijktijdig verloopt; dit heet ook wel asynchrone communicatie.udDe algemene doelstelling van dit tweede deel bestaat uit het minimalizeren vanudde assertietaal , de taal waarmee binnen het bewijssysteem beweringen over deudprocessen (het programma) kunnen worden geformuleerd. Het bepalen van zulkeudminimale (abstracte) assertietalen biedt voordelen bij het top-down ontwerp vanudprogramma's.udHet eerste hoofdstuk van het tweede deel laat zien dat het mogelijk is een com-udpositioneel bewijssysteem te baseren op een assertietaal die de beschrijving vanudprocessen alleen toelaat middels de beschrijving van de communicatie-acties perudcommunicatie-kanaal. Hiervoor is het wel vereist dat de programmeertaal in es-udsentie deterministisch is.udHet volgende hoofdstuk beschrijft een case-study: de correctheid van een gedis-udtribueerd algorithme voor het bepalen van de topologie van een netwerk wordtudafgeleid. Hierbij maken we gebruik van het bewijssysteem uit hoofdstuk 6 enudvan PVS, een tool voor het interactief genereren en checken van bewijzen. Zoudlaten we enerzijds zien hoe de (beperkte) programmeertaal van hoofdstuk 6 tochudinteressante voorbeelden toestaat, terwijl anderzijds wordt ge?llustreerd hoe deudessentie van het bewijs semi-automatisch kan worden afgeleid. Het gebruik vanuddergelijke tools heeft als voordeel dat triviale details automatisch kunnen wordenudafgehandeld, zodat de gebruiker zich kan concentreren op de daadwerkelijk lastigeudbewijsstappen.udIn het laatste hoofdstuk richten we ons op een niet-deterministische program-udmeertaal. Ook nu zijn we in staat de assertietaal te beperken ten opzichte vanudvergelijkbare bewijssystemen. We introduceren de notie van abstract history, dieud(samen met de communicatie-informatie per kanaal) een abstractie is van de ge-udbruikelijke history (een beschrijving van een proces door middel van een volledigeudopsomming van zijn communicaties). Een bijkomend voordeel hiervan is datudhet gedeelte van de logica waarin over deze abstracte histories, en dus over hetudcommunicatiegedrag van de processen geredeneerd wordt, beslisbaar is.
展开▼
