De meeste ingenieurs houden mathematische methodes liefst op grote afstand, omdat die hun waarde nog niet voldoende hebben bewezen. Het afgelopen decennium is er echter spectaculaire vooruitgang geboekt op het gebied van formele technieken. In dit artikel geeft Frits Vaandrager van de Radboud Universiteit Nijmegen een overzicht van de belangrijke ontwikkelingen en gaat hij in op de vraag welke methodes geschikt zijn voor welke problemen.
Gerard Berry, chief scientist van het Franse bedrijf Esterel Technologies, heeft voorgesteld de term ’formele verificatie‘ te vervangen door ’automatische bugdetectie‘. Hij wil hiermee benadrukken dat het (vooralsnog) niet haalbaar is om realistische IT-applicaties volledig correct te bewijzen met behulp van wiskunde. In theorie kan het wel, maar het kost gewoon te veel tijd en geld. Formele methodes moeten daarom tot doel hebben om ontwerpers te helpen zoveel mogelijk fouten zo vroeg mogelijk te vinden. Het blijkt dat formele technieken hier buitengewoon goed in zijn.
Waar ingenieurs traditioneel vooral gebruikmaken van continue wiskunde (analyse, differentiaalvergelijkingen), vergt het ontwerpen van betrouwbare computersystemen een meer discrete stijl van mathematisch redeneren. Het gedrag van computers modelleren we typisch in termen van eindige automaten met toestanden en discrete overgangen daartussen. Voor het beschrijven van en redeneren over automaten gebruiken we vaak (mathematische, formele) logica.
This article is exclusively available to premium members of Bits&Chips. Already a premium member? Please log in. Not yet a premium member? Become one for just €20 for the first year and enjoy all the benefits.
