Modulaire statische analyse voor de zachte verificatie van contracten in gedistribueerde actor programma's (FWOTM1089)

Gedistribueerde programma’s, dewelke gevormd worden door
onafhankelijke systemen die met elkaar communiceren om een
gemeenschappelijk doel te bereiken, zijn alomtegenwoordig. Actors
voorzien een geschikt model om gedistribueerde systemen te
beschrijven en te implementeren. Jammer genoeg maken
programmeurs meer fouten in gedistribueerde programma’s dan
sequentiële programma’s. Dit komt onder andere doordat
programmeurs de moeilijkheden van gedistribueerde systemen
onderschatten. Design-by-contract blijkt een krachtig paradigma te
zijn waarmee het gewenste gedrag van een programma kan worden
beschreven, waardoor ze robuuster worden tegen fouten. Helaas
introduceert het naleven van deze contracten vaak een grote last
tijdens de uitvoer. Wij stellen een nieuwe contracten taal voor om het
gedrag van gedistribueerde actor programma’s mee te beschrijven.
Om de last bij het uitvoeren van het programma te verminderen en
om potentiële defecten op voorhand te kunnen detecteren stellen we
een zachte verificatie voor. Het doel van deze verificatie is om zoveel
mogelijk contract controles te verifiëren, en de niet geverifieerde
controles als residuen achter te laten en nog steeds bij de uitvoer te
controleren. Gedistribueerde programma’s zijn vaak moeilijker om
statisch te analyseren door het niet-determinisme van de
meervoudigheid van berichten, en gedeeltelijke falingen. We stellen
een proces modulaire analyse voor om de verificatie schaalbaar,
maar ook voldoende precies te houden

Trefwoorden:gedistribueerde programmaverificatie, ontwerp-door-contract, statische analyse

Disciplines:Computerwetenschappen