System Verification and Testing
Informatica en informatiekunde | 5 EC | Voor dit product gelden ingangseisen
Code IM0402
Deze cursus heeft een vast startmoment. Kijk in het Jaarrooster wanneer de begeleiding is ingeroosterd.

Deze cursus heeft als onderwerp het verifiëren en testen van systemen met behulp van formele (wiskundige) methoden. Het eerste deel van de cursus gaat over het construeren van formele modellen. Hiertoe worden Kripkestructuren en timed automata behandeld. In het tweede gedeelte worden temporele logica en model checking gebruikt om deze modellen te verifiëren. Het laatste gedeelte behandelt model-based testtechnieken, die deze modellen kunnen testen. Een belangrijk aspect van deze cursus is dat hetzelfde model wordt gebruikt voor zowel verificatie als testing.

Algemeen

Inhoud

Verificatie en testen zijn twee belangrijke aspecten voor de constructie van correcte systemen. Een cruciaal instrument daarbij is het gebruik van modellen. Modellen staan centraal in deze cursus. Het eerste deel van deze cursus gaat over het opstellen van modellen in wiskundige formalismen zoals Kripkestructuren en timed automata. Over deze modellen kunnen eigenschappen worden uitgedrukt, die het correcte gedrag van het systeem specificeren. Deze eigenschappen leiden tot een formele specificatie. We behandelen temporele logica, een wiskundige taal die in staat is dergelijke eigenschappen uit te drukken in de tijd van het systeem. Bijvoorbeeld: een systeem voor verkeerscontrole van vliegtuigen moet voldoen aan de temporele eigenschap dat twee vliegtuigen nooit tegen elkaar botsen.
In het tweede gedeelte van de cursus bewijst U door model checking te gebruiken dat de modellen aan hun temporele specificaties voldoen. Model checking is heden ten dage een standaardtechniek voor het ontwerpen van hardware en wordt steeds populairder bij het ontwerpen van software. In 2007 hebben de ontwikkelaars van deze techniek de ACM Turing Award (de officieuze Nobelprijs in informatica) gekregen.
Het derde deel van de cursus gaat over het testen van systemen. In tegenstelling tot het eerste deel gaat de analyse niet over een model maar over een systeem dat op een machine kan draaien. Het testen is desalniettemin gebaseerd op een model van hetzelfde type als in het eerste deel van de cursus. Deze manier van testen heet dan ook model-based testing. Deze techniek is nieuw en wordt steeds populairder bij softwareontwikkeling door grote bedrijven.

Deze cursus geeft een introductie over de theorie achter model checking en model-based testing. In beide delen van de cursus worden deze theoretische concepten toegepast op concrete modellen en software.

Leerdoelen
Na het bestuderen van deze cursus wordt verwacht dat u:
- formele specificaties kunt schrijven met behulp van temporele logica's
- formele modellen kunt maken van softwaresystemen
- kunt herkennen in welke situaties model-checking van toepassing is
- gebruik kunt maken van een model-checker om te bewijzen dat de modellen voldoen aan hun formele specificaties
- Inzicht hebt in de basisprincipes van model-based testing
- een model-based testing tool kunt gebruiken om te testen of een implementatie overeenkomt met het specificatiemodel.

Aanmelden

Ingangseisen

Aanmelden is alleen mogelijk voor opleidingsstudenten die formeel zijn toegelaten tot de masteropleiding Computer Science of de masteropleiding Software Engineering.

Aanmelden

Aanmelden is alleen mogelijk voor studenten die formeel zijn toegelaten tot de masteropleiding.

Toelichting aanmelden

Deze cursus is reeds gestart. Aanmelden in het lopende academisch jaar is niet meer mogelijk.

Deze cursus start 4 september 2017. We adviseren u om u uiterlijk 14 augustus 2017 aan te melden, zodat u tijdig het cursusmateriaal ontvangt, toegang heeft tot de leeromgeving en (indien van toepassing) ingedeeld kunt worden in een studiegroep.

Bij deze cursus hoort zowel online als face-2-face activerende begeleiding. Deze cursus start op vastgestelde momenten, en ook tijdens de bestudering van de cursus zijn er vaste inlevermomenten van opdrachten en feedback. Deze begeleiding is erop gericht u sneller, effectiever en met een beter begrip van de stof door de cursus te helpen. U kunt vooraf aan de begeleidingsperiode in uw eigen tempo de stof alvast doornemen; het materiaal wordt één kwartiel tevoren al uitgeleverd. Aansluitend aan de begeleidingsperiode is uw eerste tentamenkans. Na de begeleidingsperiode heeft u nog twee ingeroosterde tentamenkansen. Informatie over begeleiding en tentamen vindt u op de respectievelijke tabbladen.

Voorkennis

Kennis op het niveau van een afgeronde (academische) bacheloropleiding Informatica. Specifiek: Logica en Informatica.

Begeleiding

Begeleidingsvorm

Deze cursus heeft een vast startmoment. Kijk in het Jaarrooster wanneer de cursus van start gaat en wanneer de begeleiding is ingeroosterd.

Per kwartiel worden groepen studenten gevormd. De docent organiseert extra begeleidingsactiviteiten zoals online bijeenkomsten, tentamenvoorbereiding of nabespreking van het tentamen. Tijdens de bijeenkomsten gaat de docent inhoudelijke in op de lesstof en bereidt u zich voor op het tentamen. De bijeenkomsten vinden plaats in de avonduren of op zaterdag.
De geboden begeleidingsbijeenkomsten hebben een zeer grote toegevoegde waarde en een verhoogde slagingskans.

Begeleidingsbijeenkomsten


Utrecht
Kwartiel 1 - begeleider: dhr. dr. F. Verbeek
1. za 09-09-2017 / 10.30-14.00 uur
2. do 19-10-2017 / 18.30-21.30 uur
3. do 16-11-2017 / 18.30-21.30 uur
4. za 13-01-2018 / 10.30-14.00 uur

Online bijeenkomsten
Kwartiel 1 - begeleider: dhr. dr. F. Verbeek
1. za 09-09-2017 / 10.30-14.00 uur
2. do 19-10-2017 / 18.30-21.30 uur
3. do 16-11-2017 / 18.30-21.30 uur
4. za 13-01-2018 / 10.30-14.00 uur

Docenten

Dhr. dr. F. Verbeek.

Bereikbaarheidsoverzicht

Bereikbaarheidsinformatie docenten/examinatoren

Tentamen

Tentamenvorm

Regulier schriftelijk tentamen bestaande uit open vragen (ov) en een opdracht.

Tentamentoelichting

Studenten moeten een verslag over hun projectopdracht maken. Het tentamen is een mondeling tentamen op afspraak waar de student zijn werkstuk moet verdedigen. Het werkstuk zelf telt voor 50% en de mondelinge verdediging telt voor de andere 50%. Het mondelinge tentamen is een openboektentamen.

Tentamendata

Schriftelijk tentamen: 05-02-2018, 24-04-2018, 28-08-2018.
Opdracht: volgens afspraak.

Tentamenhulpmiddelen

Een 'schoon' verklarend Nederlands woordenboek (op eigen risico)
Een schoon exemplaar van het gedrukte cursusmateriaal

Meer info

Cursusmateriaal

De cursus bestaat uit een tekstboek, een reader, een werkboek en de projectopdracht in digitale vorm in de elektronische leeromgeving. Het tekstboek 'Model Checking' is van Clarke, Grumberg en Peled. De reader bevat een aantal academische artikelen en wordt ook via de digitale leeromgeving beschikbaar gesteld.

Mediagebruik

Als student heeft u toegang tot een groot aantal online diensten die u nodig heeft tijdens uw studie. Deze zijn bereikbaar via MijnOU, uw persoonlijke online werkplek bij de Open Universiteit, Hier heeft u o.a. toegang tot onze digitale leeromgeving, tentamenroosters, en onze uitgebreide digitale bibliotheek.

Digitale leeromgeving

Als medewerker of als student (na inschrijven) kunt u via de cursussite in de digitale leeromgeving naar de discussiegroepen. Hier kunt u met medestudenten en begeleider informatie uitwisselen en discussiëren over de leerstof.