De Radboud Universiteit Nijmegen heeft formele softwareverificatie toegepast in een aantal praktijkstudies. Hier beschrijven Marko van Eekelen en Sjaak Smetsers er twee: de Maeslantkering en de ook in veel grote industriële systemen gebruikte Qt-toolkit. De resultaten zijn verrassend.
Onze maatschappij is in grote mate afhankelijk van software. Kleine softwarehaperingen hebben vaak hooguit enige frustratie van de gebruiker tot gevolg. Dit verandert echter zodra we te maken hebben met applicaties waarbij grote financiële belangen spelen of de veiligheid van personen in het geding komt. Kenmerkend bij deze zogeheten safety-critical of industry-critical systemen is dat één enkele softwarefout desastreuze gevolgen kan hebben: gigantische financiële schade of zelfs verlies van mensenlevens.
Daarom gelden er hoge eisen voor de kwaliteit en veiligheid van deze systemen. Zo bestaat er een keur aan ontwikkelstandaarden en -technieken die moeten garanderen dat volgens de aangegeven richtlijnen gebouwde applicaties vrij zijn van softwarefouten. Niet zelden stellen ze eisen aan het ontwikkelproces, waarbij we elke stap zorgvuldig dienen te monitoren. De standaarden voor de diverse industriële sectoren vertonen onderling ook grote verschillen. Toch bestaat er consensus over de noodzaak om tijdens de ontwikkeling van safety-critical software formele methoden te gebruiken, waarmee de correctheid van zowel ontwerp als uiteindelijke realisatie van een (deel)systeem wiskundig is aan te tonen.
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.
