Het schrijven van een programma is vaak veel gemakkelijker dan te bewijzen datudeen programma doet wat het moet doen. Daarbij wordt onze samenleving steedsudafhankelijker van computers; men denke daarbij aan complexe programmatuuruddie de verkeersleiding van treinen of vliegtuigen regelt, die de administratie van deudeectenhandel bijhoudt of die besluit of de stormvloedkering al dan niet neergelatenudmoet worden.udOm de kwaliteit van programmatuur te kunnen garanderen, wordt ze uitgebreidudgetest. Dit wordt meestal gedaan met de probeer-en-faal methode, waarbij een pro-udgramma op testinvoer wordt losgelaten en er vervolgens wordt gekeken of het aan deudverwachtingen van de programmeur en klant voldoet. Deze manier van testen elimi-udneert helaas niet alle fouten. We horen dan ook vaak mensen over bugs in programma'sudpraten. Softwarefabrikanten komen regelmatig met nieuwe versies van hun produktenuddie de bugs van de vorige versie niet meer bevatten. Dat klopt vaak wel, maar helaas isudhet eerder regel dan uitzondering dat de nieuwere versie nieuwe bugs bevat. Kortom,udbugs lijken als een soort onvermijdbare erfenis in programma's voor te komen. Voorudeen programma zoals een tekstverwerking kunnen we best wel met een bug of tweeudleven, maar van een studenten-administratiesyteem verwachten we toch dat het pro-udgramma niet onbedoeld met de cijfers van de studenten omgaat. We verwachten ook,udom een paar andere voorbeelden te noemen, dat onze prive brieven die elektronischudvia het Internet worden verzonden niet per ongeluk aan het verkeerde adres wordenudafgeleverd, of dat een elektronisch besturingsysteem van een vliegtuig niet plotselingudweigert. Met de genoemde probeer-en-faal testmethode kunnen wij slechts constaterenuddat tijdens een test alles goed ging. Helaas is het veelal onmogelijk alle toestandenudwaarin een computersysteem zich kan bevinden na gaan met een test. Dat zou veeludte veel tijd kosten of is soms zelfs theoretisch nietuitvoerbaar, nog daargelaten of hetudcommercieel acceptabel zou zijn.udEen andere methode die tot een betere softwarekwaliteit kan leiden is de volledigudformele aanpak; hierbij is een programmeur verplicht om een wiskundig bewijs vanudde correctheid van zijn programma te leveren. Meestal wordt een programma hierbijudontworpen tegelijkertijd met het construeren van een bewijs dat het programma aanudde specicatie voldoet. Er wordt gebruik gemaakt van een speciaal soort wiskundeud(vaak programma-logica genoemd) voor het redeneren over eigenschappen van een pro-udgramma. Met deze methode kan men bewijzen dat een programma qua ontwerp fout-udloos is, zonder dat men het programma zelf hoeft te testen. Dit betekent nog niet datudin de praktijk het geproduceerde programma echt foutloos zal zijn, want het ontwerpudis maar een van de vele stadia |alhoewel een van de belangrijkste| in het producerenudvan software. Wel kunnen wij zeggen dat het resultaat betrouwbaarder zal zijn.udNet zoals dat wij fouten kunnen maken bij het schrijven van een programma, kun-udnen wij helaas ook fouten maken bij het geven van een bewijs. Een gecompliceerd?Page 236udprogramma vraagt meestaal ook een gecompliceerd bewijs. De kans om fouten teudmaken zal toenemen, en het is niet onwaarschijnlijk dat een denkfout die gemaaktudwordt bij het ontwerpen van een programma ook gemaakt wordt bij het construerenudvan een correctheidsbewijs voor dat programma.udParallel met het ontwikkelen van formele methoden, is ook de technologie om bewi-udjzen te kunnen veri?eren met de computer ge?evolueerd. Deze technologie noemen weudmechanisch vericatie en het computerprogramma die dat doet noemen we (niet echtudpassend) een stellingbewijzer. Een stellingbewijzer wordt gebaseerd op een handvoludaxiomas en bewijsregels. De consistentie en zinvolheid van deze axiomas en bewijs-udregels zijn veelal al uitgebreid bestudeerd en er bestaat consensus over hun consis-udtentie. Het bewijs van een nieuwe stelling kan alleen worden geconstrueerd door hetudherhaaldelijk toepassing van de bewijsregels, uitgaande van de axiomas. De juistheidudvan deze nieuwe stellingen wordt dus afgedwongen door de manier waarop ze wor-udden gebouwd. In veel stellingbewijzers kan men ook nieuwe bewijsregels denieren inudtermen van reeds bestaande (primitieve) bewijsregels. Deze nieuwe stellingen en bewi-udjstactieken zijn vaak krachtiger dan de ingebouwde en kunnen dus leiden tot kortereuden meer inzichtelijke bewijzen.udIn dit proefschrift wordt speciaal aandacht besteed aan zogenaamde gedistribueerdeudprogramma's. Een gedistribueerd programma is een programma dat bestaat uit samen-udwerkende componenten |elke component heeft meestal een eigen processor. Zulke pro-udgramma's worden heel veel gebruikt, bijvoorbeeld in het Internet waarbij computersuduit de hele wereld in een groot elektronisch netwerk worden verbonden. Boodschappenudvan de ene computer moeten, via tussen-computers, worden verstuurd naar de bestem-udmingscomputer. Op elk van deze tussen-computers draait een component van eenudrouteringsprogramma. Deze routeringsprogramma's hebben kennis van (een gedeelte)udvan de structuur van het netwerk. Omdat het netwerk voortdurend van vorm veran-uddert (er kunnen verbindingen bijkomen of wegvallen, en er kunnen tussen-computersudaangezet en uitgezet worden) moeten deze computers het netwerk zelf gebruiken omudsamen uit te vinden hoe de globale structuur is. Zo'n routeringsprogramma is eenudvoorbeeld van een gedistribueerd programma.udOmdat het vaak om veel componenten gaat die over, tussen, met en door elkaarudwerken, is het redeneren over een gedistribueerd programma moeilijk. In dit proefschriftudbestuderen we de programma-logica UNITY die speciaal ontworpen is omte redenerenudover eigenschappen van gedistribueerde programma's [CM88]. UNITY is klein en sim-udpel, en daarom aantrekkelijk. Toch is programma's ontwerpen met UNITY, in onzeudervaring, vaak erg lastig. Er ontbreekt een systematische ontwerpmethodologie, enudsommige ontwerptechnieken bleken niet ondersteund te (kunnen) worden. We hebbenuddus UNITY uitgebreid, vooral om technieken rond het opsplitsen van programma inudparallel werkende componenten beter te ondersteunen. Er worden voorbeelden gegevenudom te laten zien hoe we de specicatie van een probleem kunnen vereenvoudigen doorudeen geschikte opsplitsing te kiezen.udWe besteden daarbij vooral aandacht aan zogenaamde zelf-stabiliserende, gedis-udtribueerde programma's. Een zelf-stabiliserend programma is een programma dat hetudsysteem weer in een gewenste toestand kan brengen als het daar, door een externe?Page 237udverstoring, uit geraakt is. Ook als er tijdens dit herstellen weer nieuwe verstoringenudoptreden is dat geen probleem voor dergelijke systemen. We hebben UNITY uitge-udbreid met een reeks van stellingen om over zulke programma's te kunen redeneren. Weudbehandelen een groot voorbeeld, het zogenaamde Eerlijk en Herhaaldelijk Toepassingud(EHT) programma. Het EHT programma is een gedistribueerd programma dat eenudbepaalde klasse van problemen zelf-stabiliserend kan oplossen (uitrekenen).udDit boek is uniek omdat het niet alleen over formele methoden of over het bewi-udjzen van een of ander moeilijk programma gaat, maar omdat vrijwel alle resultatenudmechanisch geverieerd zijn met een stellingbewijzer! Onze ervaring met mechanischudvericatie wordt ook in dit boek beschreven. Mensen die ook met mechanisch veri-udcatie van gedistribueerde programma's willen beginnen zullen veel onderwerpen in ditudboek interessant vinden.udTot slot willen we benadrukken dat het beoefenen van formele methoden vereist datudprogrammeurs een goed ontwikkelde wiskundige handvaardigheid hebben. Het eectiefudopereren met een stellingbewijzer is tot nu toe, helaas, slechts voorbehouden aan eenudhandjevol specialisten. Het is begrijpelijk dat de industrie twijfelt aan de economischudwaarde van formele methoden. Toch zullen mensen vroeg of laat, naar mate wij steedsudafhankelijker worden van computers, ontdekken hoe kwetsbaar ze zijn als er foutenudin computers optreden. In de toekomst zullen mensen dus gedwongen zijn om naarudstellingbewijzers te kijken. Investeren in de technologie van mechanisch vericatie enudin het opleiden van 'formele' programmeurs, is daarom, naar onze mening, geen wegudgegooide moeite.?
展开▼
