null System verification and testing

System verification and testing

  • Informatica
  • IM0903
  • 7,5 EC
  • Vanaf € 576
  • Voor dit product gelden ingangseisen
Deze cursus heeft een vast startmoment. Kijk in het Jaarrooster wanneer de cursus van start gaat en wanneer de begeleiding is ingeroosterd.

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 bewijs je 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. Daarnaast zullen we een aanpak tot het testen van bestaande software bestuderen, die het efficiënt maakt om bugs te vinden, ook wanneer er geen expliciet model van het systeem van tevoren werd gemaakt.

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

Leerdoelen
Na afronding van deze cursus kun je:
- formele modellen maken van softwaresystemen,
- formele specificaties schrijven met behulp van temporele logica's,
- basisprincipes van equivalence tussen modellen begrijpen,
- herkennen in welke situaties model checking van toepassing is,
- gebruikmaken van een model checker om te bewijzen dat de modellen voldoen aan hun formele specificaties,
- de basisprincipes van testing technieken, zoals model-based testing en scriptless testing, benoemen en uitleggen,
- een model-based testing tool gebruiken om te testen of een implementatie overeenkomt met het specificatiemodel,
- een scriptless testing aanpak toepassen aan het testen van een bestaande software.

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 28 april 2025. We adviseren om uiterlijk zondag 13 april 2025 hiervoor aan te melden zodat je tijdig het eventuele cursusmateriaal ontvangt, toegang hebt tot de leeromgeving en (indien van toepassing) ingedeeld kunt worden in een studiegroep. Bij aanmelding na 13 april 2025 kunnen we dit niet garanderen. Aanmelden is mogelijk tot en met 27 april 2025.


Bij deze cursus hoort een aantal online bijeenkomsten voor 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 je sneller, effectiever en met een beter begrip van de stof door de cursus te helpen. Je kunt vooraf aan de begeleidingsperiode in je eigen tempo de stof alvast doornemen; het materiaal wordt één kwartiel tevoren al uitgeleverd. Aansluitend aan de begeleidingsperiode is je eerste tentamenkans. Na de begeleidingsperiode heb je nog twee ingeroosterde tentamenkansen.

Voorkennis

Kennis op het niveau van een afgeronde (academische) bacheloropleiding Informatica. Specifiek: Logica en Informatica. Bekendheid met de concepten uit Software Testen is nuttig maar niet vereist.

Begeleidingsvorm

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

De docent organiseert extra begeleidingsactiviteiten zoals online bijeenkomsten en tentamenvoorbereiding. Tijdens de bijeenkomsten gaat de docent inhoudelijk in op de lesstof en bereid je je voor op het tentamen. De bijeenkomsten vinden plaats in de avonduren of op zaterdag.
De geboden begeleidingsbijeenkomsten zijn niet formeel verplicht, maar hebben een zeer grote toegevoegde waarde en een verhoogde slagingskans.

Begeleidingsbijeenkomsten


Studiedag Informatica en Informatiekunde Utrecht, onder voorbehoud
Kwartiel 4 - begeleider: dhr.dr. S. Schivo
- za 03-05-2025/ tijd wordt nader bekend gemaakt
Tijdig aanmelden via http://www.ou.nl/studiedag-inf-ink

Online-bijeenkomsten
Kwartiel 4 - begeleider: dhr.dr. S. Schivo
1. ma 28-04-2025 / 19.00-20.30 uur
2. vr 16-05-2025 / 19.00-20.45 uur
3. za 17-05-2025 / 14.00-15.00 uur
4. di 27-05-2025 / 20.00-21.00 uur
5. wo 28-05-2025 / 20.00-21.00 uur
6. wo 11-06-2025 / 19.00-20.30 uur
7. wo 18-06-2025 / 19.00-20.30 uur
8. wo 25-06-2025/ 19.00-20.30 uur

Tentamenvorm

Digitaal groepstentamen met open vragen en een opdracht.

Tentamentoelichting

U dient zelf tijdig aan te melden voor een tentamen.

Studenten moeten een verslag over hun projectopdracht maken. Het tentamen is een digitaal groepstentamen. Het werkstuk telt voor 33% en het tentamen telt voor de andere 67%.

Tentamendata

Digitaal groepstentamen: 06-02-2025 14:00, 08-07-2025 19:00.
Opdracht: volgens afspraak.

Tentamenhulpmiddelen

'Schoon' tekstboek 'Model checking' (E. Clarke, O. Grumberg etc.)
'Schoon' werkboek 'System Verification and Testing' (S. Schivo etc.)
Het online woordenboek
Het online woordenboek t.b.v. ANS

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' (2e editie) is van Clarke, Grumberg, Kroening, Peled en Veith. De reader bevat een aantal academische artikelen en wordt ook via de online leeromgeving beschikbaar gesteld.

Mediagebruik

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

Digitale leeromgeving

Als student kun je, na inschrijving, via de cursussite in de online leeromgeving naar de discussiegroepen. Hier kun je met medestudenten en begeleiders informatie uitwisselen en discussiëren over de leerstof.