Deze website gebruikt cookies (en daarmee vergelijkbare technieken) om het bezoek voor u nog makkelijker en persoonlijker te maken. Met deze cookies kunnen wij en derde partijen uw internetgedrag binnen en buiten onze website volgen en verzamelen.
Hiermee kunnen wij en derde partijen advertenties aanpassen aan uw interesses en kunt u informatie delen via social media.
Klik op 'Ik ga akkoord' om cookies te accepteren en direct door te gaan naar de website of klik op om uw voorkeuren voor cookies te wijzigen. Bekijk onze privacyverklaring voor meer informatie.
$altText
System verification and testing
Informatica en informatiekunde | 7,5 EC | Voor dit product gelden ingangseisen
Code IM0903
Prijsindicatie € 486
Deze cursus heeft een vast startmoment. Kijk in het Jaarrooster wanneer de cursus van start gaat en wanneer de begeleiding is ingeroosterd.

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. Andere technieken van testing worden ook getoond.

Deze cursus geeft een introductie over de theorieën achter model checking en 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 testing technieken zoals model-based testing en search-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 start 27 april 2020. We adviseren om uiterlijk zondag 12 april 2020 hiervoor aan te melden zodat u tijdig het eventuele cursusmateriaal ontvangt, toegang heeft tot de leeromgeving en (indien van toepassing) ingedeeld kunt worden in een studiegroep. Bij aanmelding na 12 april 2020 kunnen we dit niet garanderen. Aanmelden is mogelijk tot en met 26 april 2020.

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 (Studiedag Informatica)
Kwartiel 4 - begeleider: dhr. dr. S. Schivo
za 02-05-2020 / ntb

Online bijeenkomsten
Kwartiel 4 - begeleider: dhr. dr. S. Schivo
1. za 16-05-2020 / 10.30-14.00 uur
2. do 28-05-2020 / 19.00-21.30 uur
3. za 13-06-2020 / 10.30-14.00 uur

Docenten

Dhr. dr. S. Schivo, dhr. dr. F. Verbeek en mw. dr. N. van Vugt-Hage.

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 schriftelijk tentamen. Het werkstuk telt voor 33 1/3% en het schriftelijke telt voor de andere 66 2/3%.

Tentamendata

Schriftelijk tentamen:.
Opdracht: volgens afspraak.

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 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.