Correcte software, dat is het doel van drie jonge onderzoekers van het Centrum voor Wiskunde en Informatica (CWI) te Amsterdam, die binnen één maand tijd promoveren op verificatie en model checking technieken. Daarbij worden automatisch alle mogelijke toestanden gecontroleerd waarin een computersysteem zich kan bevinden. Op die manier kunnen alle fouten opgespoord worden. Dit onderzoek heeft toepassingen in veiligheidskritische software, zoals de besturing van helikopters, kernreactoren of liftsystemen.
Softwaresystemen kunnen fouten maken. Programma-onderdelen wachten bijvoorbeeld op elkaar en zorgen ervoor dat het systeem vastloopt. Fouten kunnen zeer kostbaar zijn, milieuschade opleveren en in het ergste geval mensenlevens kosten. Voor veiligheidskritische systemen zoals spoorwegbeveiligingen is het daarom belangrijk dat software foutloos is. Dit kan bereikt worden door het gebruik van wiskundige technieken, formele methoden genaamd, die fouten kunnen opsporen en kunnen vaststellen of iets echt foutloos is. Ook kan gekeken worden of de software doet wat hij moet doen.
Eén formele methode is die van verificatie door middel van enumerative model checking. Deze techniek controleert alle mogelijke toestanden van het systeem. Bij een spoorwegbeveiliging is zo'n toestand bijvoorbeeld: 'sein rood en slagboom omlaag' of 'sein rood en slagboom omhoog'. Om alle mogelijke toestanden van een complex systeem te kunnen controleren wordt eerst de software op een wiskundige manier gemodelleerd. Dit gebeurt in de muCRL-taal, die ontwikkeld is op het CWI. Vervolgens worden alle mogelijke toestanden opgesomd waarin het systeem zich kan bevinden. Deze verzameling - de toestandsruimte - kan ontzettend groot of oneindig worden: de 'state space explosion'. Natalia Ioustinova - een van de drie promovendi - onderzocht hoe miljarden toestanden in een tijdsafhankelijk systeem teruggebracht kunnen worden naar een kleiner aantal, of van oneindig naar een eindig aantal. Zij deed dit via abstracties en programmatransformaties.
Soms blijft de toestandsruimte echter te groot om op één machine gegenereerd te worden en crasht het controlesysteem. Simona Orzan, die op 25 november 2004 zal promoveren aan de Vrije Universiteit te Amsterdam, zorgde voor de distributie van berekeningen over een netwerk van computers. Zij testte dit op het Linux supercomputercluster van het CWI. Grotere problemen konden hiermee worden aangepakt in kortere tijd. Jun Pang onderzocht of de theorie van formele verificatie van gedistribueerde systemen toepasbaar is in industriële ontwikkelprocessen, via een aantal case studies. Hij keek daarbij zowel naar abstracte communicatieprotocollen als naar algoritmen, zoals die van een liftsysteem voor vrachtwagens. Er werden betere oplossingen voor problemen gevonden dan met de oude methode. Door het werk van de drie promovendi wordt het onderzoek van CWI's groep Specification and Analysis of Embedded Systems steeds breder toepasbaar.
CWI's promovendi:
- Simona Orzan, e-mail: s.m.orzan (at) tue.nl . Zij promoveert op donderdag 25 november 2004 om 10.45 uur aan de Vrije Universiteit te Amsterdam. De titel van haar proefschrift is: 'On distributed verification and verified distribution'.
- Nataliya Yustinova, e-mail: Natalia.Ioustinova (at) cwi.nl . Zij promoveerde op donderdag 4 november aan de Vrije Universiteit op het proefschrift: 'Abstractions and Static Analysis for Verifying Reactive Systems.
- Jun Pang, e-mail: pangjun (at) lix.polytechnique.fr (Engelstalig). Hij promoveerde op 26 oktober 2004 aan de Vrije Universiteit op het proefschrift: 'Formal Verification of Distributed Systems'.
Promotor van de drie promovendi is Prof.dr. Wan Fokkink, Vrij Universiteit te Amsterdam en Centrum voor Wiskunde en Informatica, e-mail wanf (at) cs.vu.nl, tel. 020 444 7735.
