Program refinement in UNITY-like environments

Abstract

Een parallel of gedistribueerd systeem is een systeem waarin meer met elkaar verbonden computers samenwerken. Iedereen komt tegenwoordig, bewust of onbewust, steeds vaker met gedistribueerde systemen in aanraking. Een van de bekendste is wel de geldautomaat waarmee men (bijna) altijd en (bijna) overal ter wereld geld van een bankrekening kan halen. Computers in gedistribueerde systemen moeten met elkaar kunnen communiceren. Dit kan via het telefoonnet, via speciale berglass kabels of zelfs via de satelliet. De infrastructuur voor telecommunicatie en ook de technieken om computers met elkaar te laten communiceren worden beter. Hierdoor wordt het mogelijk grotere en complexere gedistribueerde systemen te bouwen. We zullen steeds afhankelijker worden van deze gedistribueerde systemen en het wordt daarom belangrijker dat deze systemen correct werken. In het menselijk lichaam, en zeker in het menselijk brein, spelen zich een groot aantal parallelle processen af en we schijnen weinig moeite te hebben om deze te controle- ren en beheersen. Het nadenken over gedistribueerde systemen kost ons daarentegen veel moeite, juist omdat in deze systemen meerdere dingen tegelijk gebeuren die elkaar op subtiele wijze be?nvloeden. Opdrachtgevers kunnen hun wensen vaak niet duidelijk verwoorden en door de complexiteit van de meeste gedistribueerde systemen is het vaak moeilijk te bepalen of het uiteindelijke systeem aan de wensen voldoet. Formele, wiskun- dige methoden kunnen hier behulpzaam zijn. Ze kunnen gebruikt worden om systemen duidelijk te speciceren en ze geven middelen om te bewijzen dat een systeem aan zijn specicatie voldoet. Verder kunnen ze een beter inzicht geven in wat een specicatie precies inhoudt en wat er zich mogelijk in een speciek gedistribueerd systeem afspeelt. Dit proefschrift presenteert een wiskundige methode die het ontwerpen en bouwen van gedistribueerde systemen ondersteunt. Bijzonder aan deze methode is dat zij een compositioneel ontwerpproces mogelijk maakt; dit wil zeggen dat onderdelen in het sys- teem onafhankelijk beschreven en gebouwd kunnen worden, waarbij de correctheid van het gehele systeem behouden blijft. Dit kan de ontwikkeling van complexe systemen aanzienlijk vereenvoudigen. We gaan hierbij uit van een bestaand formalisme: UNITY. Het UNITY formalisme is ge?ntroduceerd door Chandy en Misra [CM88] en het is een relatief eenvoudig formalisme voor het ontwerpen van parallelle en gedistribueerde 165?166 Samenvatting systemen. Het bestaat uit twee delen: een programmeertaal en een programma logica. De programmeertaal is beperkt en wordt gebruikt om gedistribueerde systeem te modelleren zonder daarbij allerlei details van een specieke netwerkarchitectuur in ogenschouw te nemen. In de logica kunnen (temporele) eigenschappen worden uitgedrukt en is daarom geschikt om programma's te speciceren en om over programma's te redeneren. Het ontwerpen van een gedistribueerd systeem in UNITY begint met het geven van een specicatie: dit is een verzameling van temporele eigenschappen waaraan het te bouwen systeem moet voldoen. Deze specicatie dient als contract tussen de opdracht- gever en de ontwerper; zij is zo algemeen mogelijk en abstraheert van allerlei details. De ontwerper van het systeem zal vervolgens de specicatie in een aantal stappen ver- jnen waarbij problemen van algoritmische aard worden opgelost. Als een specicatie voldoende uitgekristalliseerd is wordt er een UNITY programma ontwikkeld en bewijst men dat het programma aan de specicatie voldoet. Dit programma moet worden afge- beeld op de specieke netwerkarchitectuur waarvoor men het systeem ontwikkelt. Deze stap is niet formeel: in het UNITY formalisme kan men de correctheid van deze stap niet wiskundig bewijzen. Daarom moet de afbeelding zo eenvoudig mogelijk zijn. Vaak heeft het UNITY programma echter niet de juiste vorm voor een eenvoudige afbeelding. Dan zou het handig zijn als het programma getransformeerd kon worden naar een geschiktere vorm, waarbij de correctheid van het programma natuurlijk weer behouden moet blijven. Dit wordt programmaverjning genoemd en het wordt door het UNITY formalisme niet ondersteund. In dit proefschrift bekijken we hoe programmaverjning aan het UNITY formalisme kan worden toegevoegd. We geven hiervoor verschillende mogelijkheden aan de hand van semantische modellen van UNITY programma's. Deze modellen resulteren in verschillende noties van programmaverjning. Twee van deze noties zijn compositio- neel; dat wil zeggen dat delen van een programma afzonderlijk verjnd kunnen worden zonder dat de correctheid van het hele systeem daarbij in het geding komt. We zullen laten zien dat de compositionele noties in een bepaald opzicht de beste compositionele noties van verjning zijn die we in het UNITY formalisme kunnen bereiken. In dit proefschrift introduceren we tevens het ImpUNITY formalisme, een uitbrei- ding van UNITY. Programma's in UNITY hebben weinig structuur en ook de manier waarop ze kunnen worden samengesteld is beperkt. In het ImpUNITY formalisme is het mogelijk meer structuur aan programma's te geven en ook de manier om programma's samen te stellen is uitgebreider. Zo is het mogelijk om de interferentie van een omge- ving te beperken en een deel van de toestandsruimte voor de omgeving af te schermen. Tevens biedt ImpUNITY een nieuwe manier van communicatie: componenten kunnen met elkaar communiceren via een zogenaamd procedure mechanisme. Deze uitbreidin- gen vergroten de mogelijkheden voor het compositioneel ontwerpen van programma's en kunnen de afbeeldingen van programma's naar verschillende netwerkarchitecturen ver- eenvoudigen. De uitbreidingen worden ook doorgevoerd in de ImpUNITY logica en de?Samenvatting 167 notie van programmaverjning. Net als ImpUNITY programma's ondersteunt de logica een compositionele manier van redeneren en de logica gebruikt worden om componen- ten afzonderlijk te speciceren. ImpUNITYondersteunt een compositionele notie van programmaverjning en een uitgebreide set van programma transformatieregels. In een tweetal case studies laten we zien hoe het ImpUNITY formalisme gebruikt kan worden bij het oplossen van praktische problemen.?168 Samenvatting