System verification and testing

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.