Eerste Dutch Model Checking Day door universiteit Twente

Universiteit Twente

01/05 27 januari 2001

Eerste Dutch Model Checking Day

Bugs en deadlocks zo vroeg mogelijk te lijf

Een foutje in de software kan leiden tot de spreekwoordelijke computer die regelmatig vastloopt. Maar evengoed kan een fout tot gevolg hebben dat een raket als de Ariane V uit koers raakt of de Pathfinder niet goed functioneert op Mars. Terdege testen lijkt de remedie. Maar het vinden van een fout in software die al geschreven is, of in een chip die na een paar maanden uit de fabriek komt, is erg kostbaar. Model checking is daarom sterk in opkomst: omschrijf het systeem eerst maar eens in een model, stel dit op de proef en ga dan pas implementeren. Onverwachte valkuilen worden dan eerder gevonden. Een eye-opener voor de industrie, die steeds hogere eisen ziet aan prestaties en tegelijk aan kosten. Reden voor onderzoekers van de faculteit Informatica van de Universiteit Twente om op 30 januari de eerste Dutch Model Checking Day te organiseren.

The proof of the pudding is in the eating, vertaald naar de ontwikkeling van software, betekent dat in de praktijk pas gaat blijken hoe het werkt. Dus: testen van een product dat bijna marktrijp is. Vaak wordt ook nog op die manier gewerkt. Nu laat software zich nog flexibel aanpassen, maar een fout in hardware die pas na productie aan het licht komt, is dodelijk. Testen is onontbeerlijk, maar het vinden van fouten in zon laat stadium is duur: de fout is al vroeg gemaakt, pas na testen gaat in de papieren lopen. Bij de huidige time-to-market eisen is dat niet acceptabel. En de economische kant is nog maar één aspect: vaak spelen ook factoren als veiligheid.

Verwachting
In analogie met de pudding is het beter om eerst over de ingrediënten na te denken, en bijvoorbeeld over de verwachting van degene die m gaat eten. Dat klinkt vanzelfsprekend, maar heel precies definiëren wat een systeem moet kunnen, en waartegen het bestand moet zijn, is een stap die vaak wordt verwaarloosd. De leerstoel Formele Methoden en Gereedschappen van de Universiteit Twente ontwikkelt hiervoor technieken en tools. Eigenlijk moet de ontwerper heel precies leren kijken. Wat wil je van het systeem? Wat voor factoren spelen mee? Dit eisenpakket wordt vertaald naar een model waarin tot op detail toestanden en toestandsovergangen worden beschreven.

Push button
De Twentse onderzoeksgroep heeft volgens deze methodiek bijvoorbeeld gewerkt aan de besturingssoftware voor de afsluitarmen in de Nieuwe Waterweg, aan communicatienetwerken in autos, en aan nieuwe geïntegreerde thuissystemen voor video en audio. Onderling heel verschillende systemen die op een zelfde manier kunnen worden gecheckt. Volgens onderzoeker dr.ir. Joost-Pieter Katoen is er grote vooruitgang geboekt in bijvoorbeeld het voorspellen van valkuilen, zoals mogelijke deadlocks waarin het systeem helemaal niets meer doet. Ook wordt het beter mogelijk om modellen te vereenvoudigen. Een groot voordeel van model checking is volgens Katoen het pushbutton karakter van de methode. Zonder kennis te hoeven hebben van deze methode kan de ontwerper zijn model op de proef laten stellen.

Dagprogramma
Het programma van de dag vermeldt verschillende sprekers uit de wetenschap en de industrie. Invited speaker is prof. Kim Larsen. Hij is hoogleraar aan de Universiteit van Aalborg en de UT. Dagvoorzitter is prof. Ed Brinksma, die in Twente de onderzoeksgroep leidt die zich sterk richt op model checking. Andere sprekers zijn onder meer afkomstig van Philips en het Telematica Instituut.

Noot voor de pers
Meer informatie over de Dutch Model Checking Day is te vinden op http://fmt.cs.utwente.nl/mcd2001. De onderzoekers zijn graag bereid het onderwerp in een gesprek verder toe te lichten.

dinsdag 30 januari 2001