Brontekst bekijken van Introductie Informatica en Informatiekunde/deel 2. activiteiten/9. verificatie

{{III/dag
|vraag=
Hoe zeker kunnen we zijn? En helpen computers daarbij?
|brainstorm= Hoe kwam [http://www.youtube.com/watch?v=IONcgYzVFlg dit] {{III/navimgx|xsize=300|ysize=450|image=ariane5.jpg|link=http://www.youtube.com/watch?v=IONcgYzVFlg}}en kunnen we zoiets voorkomen - of, nog beter, uitsluiten?
<br>
Hoe hadden we [http://www.youtube.com/watch?v=NW3RGbQTLhE dit] {{III/navimgx|xsize=600|ysize=277|image=mifareclassic.jpg|link=http://www.youtube.com/watch?v=NW3RGbQTLhE}} kunnen voorkomen?
|verkenning=
testen, verifiëren, specificeren, modelleren, model checking, tools 
|pauzenvraag=

|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

|doelen=
* 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.

|motto=
''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.''

[[Afbeelding:RationalitySquareVerify.gif|150px|thumb|left|Verificatie en validatie]]
|rode draad=

|programma=

|taak=
[http://www.cs.ru.nl/~erikpoll/Teaching/III/dag9.html uppaal]

|materiaal=
* [http://www.cs.ru.nl/ita/rondleiding/uitleg/martijn.html carrieres (clickable map: correctness by construction])
* [http://www.cs.ru.nl/ita/rondleiding/index.html rondleiding ita]
* [http://www.cs.ru.nl/H.Wupper/informatica/billard/ballen.html billard (correctness by contruction)]

}}