Formelevalidatie

Formelevalidatie is een benadering binnen systeem- en softwareontwikkeling die gericht is op het aantonen dat een product, proces of systeem voldoet aan zijn formele specificaties en aan het beoogde gebruik. In tegenstelling tot traditionele validatie die sterk op testen leunt, combineert formelle validatie wiskundige modellen, formele specificaties en logische bewijzen om eigenschappen zoals correctheid, veiligheid en gebrek aan deadlocks aan te tonen.

Toepassingsgebieden zijn onder meer kritieke software voor luchtvaart- en railvervoer, medische en embedded systemen, en cryptografische protocollen. Formele validatie kan naast of in combinatie met testen worden ingezet en dient vaak als aanvulling op formele verificatie, dat gericht is op bewijzen van juistheid ten opzichte van specificaties.

Technieken binnen formelle validatie omvatten formele specificatietalen (bijvoorbeeld Z, VDM, Alloy), model checking, theorem proving en abstract interpretation. Het proces begint met het vastleggen van formele vereisten en het construeren van een formeel model. Vervolgens worden properties bewezen of model-checkingresultaten geanalyseerd; waar mogelijk kan een implementatie worden verfijnd op basis van deze bewijzen, zodat de implementatie afstemt op het formele model.

Voordelen zijn onder meer een hoger niveau van vertrouwen in de correctheid en veiligheid en het vroegtijdig opsporen van ontwerpfouten. Nadelen zijn de vereiste gespecialiseerde kennis, hogere kosten en soms beperkte schaalbaarheid voor complexe systemen. Formele validatie is daarom meestal een onderdeel van een bredere kwaliteitsstrategie en wordt vaak toegepast in combinatie met traditionele testen.

Zie ook: formele verificatie, formele specificatie, model checking.