Formele methoden voor software engineering

Samenvatting

Vaknaam	Formele Methoden voor Software Engineering II
Vakcode	213520
Studiebelasting	5.0 EC

Omschrijving

Dit vak behandelt het gebruik van wiskundige technieken en bijbehorende software-gereeedschappen voor de modellering en analyse van softwaresystemen. Aan de orde komen:

1. Het modelleren van gedistribueerde systemen m.b.v. procesalgebra, ondersteund door het gereedschap LTSA en de analyse van deze modellen d.m.v. simulatie- en model-checkingtechnieken. De onderliggende theorie is gebaseerd op transitiesystemen en bisimulatie.

2. Het specificeren van de correctheid van objectgeoriënteerde (Java-)programma's met behulp van pre- en postcondities in JML, en het analyseren van de correctheid van Java programma's m.b.v. ESC (Extended Static Checking). De onderliggende theorie is gebaseerd op Hoare-logica.

Voorkenniseis

• enige ervaring met wiskundige basisconcepten als verzamelingen, relaties, functies, en predikatenlogica
• inzicht in en basale ervaring met het ontwerpen van softwaresystemen
• ervaring met het programmeren in Java (Programmeren 1 en 2).

Leerdoelen

Na afloop van het vak kan de student:

• de principes transitiesystemen en Hoare-logica uitleggen;
• eenvoudige gedistribueerde systemen specificeren met de procesalgebra FSP, en analyseren met het tool LTSA;
• Java-programma's annoteren met JML-specificaties, en de geannoteerde programma's analyseren met ESC/Java
• beargumenteren wat het belang is van formele specificatie en analyse voor software engineering

Onderwijs

Dit vak wordt gegeven in 10 hoorcolleges, 10 werkcolleges en 4 practicumdagdelen.

Beoordeling

Het vak wordt afgesloten met een schriftelijk tentamen. Daarnaast zijn er een aantal huiswerkopgaven waar punten mee gehaald kunnen worden.

Studiemateriaal

Bij dit vak wordt uitsluitend gebruik gemaakt van Teletop voor het beschikbaar stellen van studiemateriaal.

Docent

De docent en contactpersoon van dit vak is Dr.ir. R.. Langerak.

Links

• VIST
• Oude tentamens