Introductie Informatica en Informatiekunde/deel 2. activiteiten/9. verificatie

9. verificatie Men heeft iets bedacht en gemaakt, alles zit goed in elkaar, op een theoretisch fundament. Maar klopt het ook? Het kan zo complex zijn dat we het niet meer overzien. Verificatie en validatie

Hoe zeker kunnen we zijn? En helpen computers daarbij? doelen: aan het eind kunnen de deelnemers uitleggen wat het verschil is tussen valideren en verifiëren; uitleggen wat het verschil is tussen testen en verifiëren; uitleggen hoe een toestandsdiagram een (bepaald aspect) van een systeem beschrijft. een eenvoudige modelbeschrijving in Uppaal begrijpen, hier zelf kleine aanpassingen in maken, en deze simuleren en model-checken met de Uppaal tool.

brainstorm

Hoe kwam dit

 

en kunnen we zoiets voorkomen - of, nog beter, uitsluiten?

Hoe hadden we dit

 

kunnen voorkomen?

verkenning

testen, verifiëren, specificeren, modelleren, model checking, tools

pauzevraag

concepten

• hoe kan men zeker zijn?
  • inzicht
  • correctness by construction (rationele ontwikkeling, waarbij elke stap gegarandeerd klopt)
  • verifiëren: bewijzen dat ontwerp voldoet aan specificatie
  • valideren: nagaan dat de specificatie zegt wat-ie moet zeggen
  • deductie (afleiden, bewijzen)
  • inductie (testen, experimeteren)
• simulatie, rapid prototyping
• proof assistants
• model checkers
• bewijsbaarheid
• model, toestandsdiagram

rode draad: cellulaire automaten

studietaak

uppaal

materiaal

• carrieres (clickable map: correctness by construction)
• rondleiding ita
• billard (correctness by contruction)

docenten

zalen