« Architecten en Engine… | Home | High Availability clu… »

VVSS Symposium : Verificatie en Validatie van software

Afgelopen vrijdag 23 maart ben ik naar het VVSS symposium geweest. VVSS staat voor Verification and Validation of Software Systems.

Het symposium werd voor de derde keer gehouden bij de Technische Universiteit Eindhoven en werd georganiseerd door LaQuSo, het Laboratory for Quality Software, dat een samenwerkingsverband is tussen de universiteiten van Eindhoven en Nijmegen.

Het symposium had 2 keynotes en maar liefst 30 presentaties in 5 parallel tracks. Ik heb in totaal 8 presentaties kunnen bijwonen. Er waren zo'n 300 aanwezigen.

Voordat ik in ga op de inhoud moet ik zeggen dat het met weer enorm opviel wat een verschil in kwaliteit er was tussen de presentaties. In mijn artikel over presentatietechnieken heb ik al eens aandacht besteed aan meest voorkomende fouten tijdens presentaties, en ik heb vrijdag alle fouten weer voorbij zien komen. Ook viel me de belabberde kwaliteit op van de Engelse taal, aangezien alle presentaties in het Engels waren. Slechts enkele presentaties waren een genot om naar te kijken (onafhankelijk van de inhoud).

Ik zal me daarom beperken tot een bespreking van de goede zaken die me zijn bijgebleven.

Professor dr. Wil van der Aalst had een enorm boeiende keynote over het gebruik van logbestanden voor het opstellen van procesdiagrammen.

Als systemen worden ontworpen, worden vaak procesdiagrammen gemaakt (hier zijn verschillende notatietechnieken voor beschikbaar, zoals Petrinets of BPEL). Als het systeem is ontworpen en het draait, is het nuttig om na te gaan hoe het proces in de praktijk gaat.

Vrijwel alle moderne systemen genereren een enorme hoeveelheid logging. Niet alleen IT systemen, maar ook bijvoorbeeld medische systemen. De TU/e heeft software ontwikkeld om vanuit logbestanden automatisch procesdiagrammen te maken, zonder dat die software het proces kent. Ook kan de software aangeven op welke plaatsen in het proces de meeste vertraging optreedt. De techniek wordt process-mining genoemd.

Opvallend hierbij was dat het proces in de praktijk, zoals dat uit de logbestanden blijkt, zeer afwijkt van het originele (gedocumenteerde) proces. Het blijkt dus een goede manier te zijn om en architectuur achteraf te verifiëren in de praktijk.

Er werden aan aantal aansprekende voorbeelden getoond uit de praktijk, waaronder een testtraject en een procesflow in een ziekenhuis.

Compuware toonde een product (Vantage) dat performance-informatie geeft over in-productie zijnde .Net of Java (web)applicaties. In productie worden metingen verricht die aantonen waar eventuele bottlenecks in het systeem zitten.

Er werd ook een tool getoond (Dev Partner) waarmee tijdens het programmeren al kon worden aangegeven waar performance problemen zich zouden kunnen voordoen als het systeem live zou gaan.

Hans Baaten van Atos Origin hield een goede presentatie over de ATOS methode Requirements Definitions Center. Deze methode is gebaseerd op het Unified Process (RUP) en is dus iteratief van aard. Een belangrijk kenmerk van de methode is dat al tijdens het opstellen van requirements een software architect, een systeem analist, een requirements engineer en een tester betrokken zijn.

De methode levert overigens geen tools, het maakt gebruik van standaard tools van bijvoorbeeld IBM, Compuware of Borland.

Een mooi voorbeeld van een hele goede spreker was Erik Poll van de Radboud Universiteit Nijmegen. Hij had een presentatie over het formeel verifiëren van een SSH implementatie voor mobiele telefoons (klinkt saai, maar het was erg boeiend).

Het blijkt dat SSH een protocol is dat op zich erg sterk is, maar dat de implementatie van het protocol in een applicatie dermate moeilijk is, dat er security kwetsbaarheden ontstaan bij het gebruik van SSH.

De specificatie van SSH bestaat uit een tekst document (diverse RFC's) van ongeveer 100 pagina's. De beschrijving zit vol met ingewikkelde constructies. De universiteit heeft daarom getracht om de specificatie formeel te beschrijven in state-diagrams. Dit bleek heel moeilijk te zijn, maar het is gelukt. Met dit formele model kon men controleren of de implementatie van SSH in een mobiele telefoon (geschreven in Java) klopte.

Het zal u niet verbazen dat men diverse fouten in de implementatie gevonden heeft.

De laatste keynote was door Professor dr. David Parnas van de Universiteit van Limerick in Ierland. Hij heeft 40 jaar van zijn leven gewijd aan het verbeteren van softwaredocumentatie.

Zijn belangrijkste boodschap was dat het beschrijven van software moet worden aangepakt als de technische diagrammen in de traditionele "engineering" (weg- en waterbouw, gebouwen, elektrische diagrammen, etc). Het kenmerk van deze diagrammen is dat ze allemaal zijn gebaseerd op een behoorlijke hoeveelheid wiskunde.

Professor Parnas heeft in de loop der tijd een methode ontwikkeld om software te beschrijven in wiskundige termen, en om die (ingewikkelde) notatie om te zetten naar een tabelstructuur, die door vele mensen makkelijk is te lezen en die aantoonbaar correct is. Zijn methode is onder andere toegepast in software voor vliegtuigen en kerncentrales.

Al met al was het een nuttige en interessante dag, ondanks een aantal (zeer) slechte presentaties en een schamele lunch.

En... Wat vindt u ervan? Klik hier om uw mening te geven: