Samenvatting

Gedistribueerde algoritmen en protocollen zijn van vitaal belang geworden voor de consumenten-elektronica. Gedurende de laatste jaren is er in de industrie een enorme inspanning gepleegd om verschillende protocol-families, zoals IEEE 1394 'Firewire' and HAVi, te ontwikkelen en in consumentenproducten te verwerken. Hoewel deze producten meestal geen kritieke veiligheidsaspecten kennen, kunnen de financiŽle gevolgen van fouten of slechte prestatie enorm zijn vanwege de massale productreplicatie. Dit impliceert dat de verificatie van de correctheid van zulke systemen van groot praktisch belang is. De zeer hoge complexiteit van de protocolfamilies (specificaties zijn typisch enige honderden pagina's lang) maken hun verificatie echter tot een grote uitdaging. Behalve de grote omvang is ook de analyse van tijdafhankelijke onderdelen een belangrijke bron van problemen vanwege de nogal subtiele complicaties die ze soms kunnen veroorzaken. Dit project richt zich op de ontwikkeling en integratie van methoden en gereedschappen voor de verificatie en analyse van real-time embedded systems, met een nadruk op gedistribueerde algoritmen en protocollen voor de consumentenelektronica. Het doel is om niet alleen 'harde' tijdseisen (bijv. het systeem moet altijd voor een gegeven tijdstip x doen), maar ook zogenaamde 'zachte' tijdseisen (bijv. het systeem moet over het algemeen voor een gegeven tijdstip x doen). Voor dit laatste type van eisen volgen we een stochastische benadering. Veel systemen combineren verschillende soorten van eigenschappen, met vaak puur functioneel gedrag in grote delen en een klein aantal aanvullende harde/zachte tijdseisen op een of meer specifieke plaatsen. Het heeft duidelijke voordelen de verificatiemiddelen van zulke verschillende eigenschappen in ťťn raamwerk aan te bieden, en het project richt zich derhalve op een geÔntegreerde benadering van het verificatieprobleem. In deze aanpak bestaat wordt er gestreefd naar een duidelijke theoretische en practische verbinding met de zuiver functionele analyse van systemen aan de ene kant, en met het gebied van de prestatie-analyse aan de andere kant.

Het project heeft concreet de volgende doelstellingen:

Uitbreiding van bestaande verificatiemethoden voor getimede systemen met voorzieningen voor stochastische eigenschappen.
Ontwikkeling van een software-omgeving van verificatiegereedschappen voor de analyse van getimede en stochastische systemen.
Toepassing van geavanceerde methoden en gereedschappen op case studies van represenatieve complexiteit.

Ons project bouwt direct voort op de ervaring en resultaten van twee gemeenschappelijke onderzoeksprojecten die in 1999 worden afgerond, en onze verwachtingen rechtvaardigen dat bovenstaande projectdoelstelling inderdaad realistisch zijn. Het SION project "Testing and Verification of Timed Systems (TVTS)" (KUN, UT) heeft zowel significante theoretische resultaten voortgebracht, als ook een prototype software gereedschap (SPADES), die tezamen voor een groot deel de basis voor het huidige project vormen. De geboekte resultaten (testtheorie voor getimede systemen, procesalgebra voor getimede en stochastische systemen) moeten nu gebruikt worden om werkbare verificatiemethoden voor hard en zacht getimede systemen te verkrijgen. Het SPADES gereedschap kan als beginpunt voor een serieuze toolontwikkeling dienen.

Het andere voorafgaande samenwerkingsproject (CWI, UT, (KUN en Philips Research) is "Specification, Testing and Verification of Software for Technical Applications (STVSTA)". In dit project zijn een aantal protocollen uit de IEEE 1394 en de HAVI families met succes geanalyseerd, gebruikmakend van een combinatie methoden en gereedschappen voor verificatie en testen (LOTOS, SPIN, Caesar/Aldebaran, I/O automata, PHACT,..). Het project heeft ons een aanzienlijke ervaring gegeven in de omgang met correktheidsvragen in een industriŽle context, hoewel beperkt tot alleen functionele en harde-tijdseisen. Het zou voor deze protocollen ook duidelijk van groot belang zijn de zachte-tijdseisen en prestatie-analyse te bestuderen. Om de praktische relevantie van de case studies in dit project te garanderen, zal het zeer succesvolle en productieve werkvorm van het STVSTA-project worden overgenomen. Er wordt derhalve voorzien dat een AIO in nauwe samenwerking met Philips Research de case studies zal uitvoeren. Het gaat hierbij om een vijftal verschillende toepassings-cases van ongeveer een half jaar werk elk.

Meer Informatie:

Project voorstel (volledige tekst) Publicaties
Personeel en Contactpersonen Gereedschappen
Het project op de Progress site Verwante onderwerpen
Voortgangsverslag 2000

October 1, 2002
Henrik Bohnenkamp