Wiskunde

model checking


Model Checking

Je hebt het vast wel eens gehad. Ben je lekker aan het werk op je computer, loopt hij ineens vast! En natuurlijk heb je het werk niet opgeslagen. Je probeert nog van alles om te redden wat er te redden valt, maar uiteindelijk moet je toch opgeven en de computer opnieuw opstarten. Je kunt dan weer helemaal opnieuw beginnen. Behalve dit zijn er nog veel meer problemen met computers. Denk bijvoorbeeld aan de belastingdienst die een paar jaar geleden ruim 700.000 mensen geen geld terug kon geven omdat de computer de aangiftes kwijt was geraakt.

Er wordt daarom veel onderzoek gedaan naar verschillende manieren om fouten in computerprogramma's te kunnen vinden, op te lossen en zelfs te voorkomen. Een van die manieren is model checking. Dit betekend letterlijk 'modelcontrole'. Het is een techniek die in de informatica is bedacht om te controleren of een computerprogramma zich gedraagt zoals wij willen. Dit doen we niet door direct een computerprogramma te controleren, maar door eerst een model van het programma te maken en dat te controleren. Het voordeel hiervan is dat de modellen vaak veel eenvoudiger zijn dan het computerprogramma, en dus gemakkelijker te controleren.

onderzoeksvragen

Model
Hoe maak je een model van een computerprogramma?

Specificatie
Maak een overzicht van het gedrag dat je van het programma verwacht.

Dagelijks leven
Op welke problemen uit je dagelijks leven zou deze methode toegpast kunnen worden?

Wiskunde
Welke wiskunde kun je gebruiken om een model te maken?