vrijdag 30 januari 2009

Proefschrift: "Specification and Analysis of Internet Applications"

Harm van Beek (2005)

Tegenwoordig vinden er meer en meer activiteiten plaats via het internet. Dit betekent dat internet-applicaties steeds belangrijker worden. Omdat deze applicaties ook in omvang en complexiteit groter worden, wordt het specificeren en implementeren van zulke applicaties steeds lastiger. Er komen veel kwesties de hoek om kijken, zoals sessie-beheer en het correct implementeren van het parallel gebruik door meerdere cliënten. Onze mening is dat formele methoden kunnen helpen deze problemen aan te pakken.

In dit proefschrift wordt een nieuwe specificatietaal, DiCons, geïntroduceerd, die gebruikt kan worden voor het specificeren van een speciale groep van internet-applicaties, de zogenaamde gedistribueerde consensus applicaties. Dit zijn applicaties die door een groep van cliënten gebruikt kan worden om een gemeenschappelijk doel te bereiken. Hierbij hoeven gebruikers elkaar niet fysiek te ontmoeten en vindt alle communicatie asynchroon plaats. Voorbeelden van zulke applicaties zijn het trekken van Sinterklaaslootjes, een stemming, een veiling, maar ook het plannen van een vergadering.

We bekijken eerst de verschillen tussen op het web gebaseerde en “gewone” window-gebaseerde applicaties. Vervolgens bekijken we de verschillen en overeenkomsten tussen enkele voorbeeldapplicaties en we kijken welke risico’s het gebruik van web-applicaties met zich meebrengt. Daaruit abstraheren we concepten die voor alle applicaties in het voor ons interessante domein van belang zijn.

Met deze concepten in ons achterhoofd ontwikkelen we een op proces-algebra gebaseerde formele specificatietaal. De taal bevat naast de standaardoperatoren voor sequentiële en alternatieve compositie drie conditionele operatoren: de conditionele keuze, de conditionele herhaling en de conditionele onderbreking. We leggen uit hoe toestanden en tijd aan de taal toegevoegd worden en welke communicatie-primitieven we gebruiken voor het modelleren van communicatie via het internet tussen gebruikers en de applicatie zelf. Daarnaast voegen we de mogelijkheid voor het specifiëren van transactioneel gedrag toe. Dit doen we door eerst een formalisme in detail uit te werken dat dit transactioneel gedrag beschrijft. Dit formalisme wordt vervolgens aangepast zodat het in de DiCons specificatietaal past.

Om de toepasbaarheid van de taal aan te tonen worden enkele eigenschappen van specificaties bewezen. Daarnaast wordt een methodiek gegeven voor het testen van internet-applicaties. Deze methodiek is gebaseerd op transitiesystemen die onder andere met behulp van \dicons\ specificaties beschreven kunnen worden. Met behulp van een implementatie van het algoritme voor het testen van internet-applicaties worden enkele applicaties getest. Ook wordt uitgelegd hoe een internet-applicatie geïmplementeerd kan worden met behulp van de momenteel gangbare technieken, en hoe een specificatie omgezet kan worden in uitvoerbare programmacode. Er wordt kort ingegaan op de compiler die voor een eerste versie van DiCons geïmplementeerd is en er wordt aangegeven welke uitbreidingen nodig zijn om specificaties van de in dit proefschrift beschreven taal om te zetten in programmacode.

Download proefschrift