Achtergrond

Formele modelverificatie van stormvloedkering tot treinvolgsysteem

Franc Buve is consultant bij Logica Technical Software Engineering in Eindhoven. Hij heeft ruim twintig jaar ervaring als ontwikkelaar, architect en projectmanager van technische projecten op het gebied van veiligheidskritieke toepassingen, telecom en embedded software.

Leestijd: 8 minuten

Gegarandeerd foutvrije software binnen tijd en budget, wie wil dat niet? Dat is de belofte die formele modelverificatie ons doet. Toch past de industrie deze tak van sport nog maar weinig toe, deels uit onbekendheid, deels uit angst voor de complexiteit van formele methodes. Aan de hand van drie praktijkvoorbeelden laat Franc Buve van Logica zien dat formele modelverificatie wel degelijk met succes in commerciële projecten toepasbaar is.

Modelverificatie is een onderdeel van modelgedreven ontwikkeling. Dit is een ruim begrip: de een vindt het maken van rudimentaire UML-diagrammen in een tekenpakket al modelgedreven ontwikkeling, een ander wenst daar pas van te spreken als uit de modellen automatisch grote delen programmacode zijn te genereren. Zelf beschouw ik als de essentie van modelgedreven ontwikkelen het gebruik van een specificatietaal of notatie om het systeem of delen daarvan te beschrijven op een manier die het mogelijk maakt het gedrag te voorspellen. Een dergelijk beschrijving noemen we een model en het controleren ervan op gewenst gedrag heet modelverificatie.

Afhankelijk van de gekozen notatie zijn er verschillende hulpmiddelen, of modelcheckers, waarmee we de verificatie geautomatiseerd kunnen uitvoeren. Dit varieert van eenvoudige consistentiecontroles, bijvoorbeeld of de uitstroom van de ene module wel klopt met de instroom van de andere, tot simulatie van modelgedrag, waarbij we kunnen zien of het ontwerp inderdaad doet wat we voor ogen hadden. Het summum van modelverificatie is een wiskundig bewijs van correctheid. Hiervoor zijn speciale specificatietalen nodig. Dit is het speelveld van de formele methodes.

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 and enjoy all the benefits.

Login

Related content