Computers rukken steeds verder op. Vliegtuigen, treinen en auto's zitten vol met electronica. Soms gaat het mis: dan komt een vliegtuig in een duikvlucht omdat de computer de macht overneemt, of stopt een auto midden op de snelweg vanwege een software bug. Hoe kunnen we dit soort fouten voorkomen? Om ervoor te zorgen dat software bugs al tijdens het ontwerp worden gevonden (en niet pas wanneer bijvoorbeeld het vliegtuig al in de lucht is) maken bedrijven steeds vaker gebruik van modellen. Deze modellen bestaan uit diagrammen en tekst waarmee op een hoog niveau van abstractie wordt beschreven hoe cruciale onderdelen van een computersysteem zich gedragen. Vervolgens gebruikt men slimme software om aan die modellen te rekenen: men probeert fouten op te sporen of te bewijzen dat er geen fouten zijn.
Binnen de informatica wordt modelleren steeds belangrijker. Er is sprake van een duidelijke trend waarbij modellen het voornaamste product van systeemontwikkeling worden, denk bijvoorbeeld aan de opkomst van de Unified Modeling Language (UML). Modellen kunnen worden gebruikt voor overleg met klanten en belanghebbenden, voor het analyseren van het ontwerp, voor het genereren van code en voor het testen van de uiteindelijke implementatie.Tijdens deze cursus werk je met het softwarepakket Uppaal, een zogenaamde model checker waarmee je zelf modellen kunt maken en laten doorrekenen. Je gebruikt Uppaal om een aantal systemen te modelleren en analyseren. Zo ga je op zoek naar fouten in het ontwerp van een geldautomaat, een blikjesautomaat, en een spoorwegovergang, en probeer je deze fouten te repareren. Ook leer je hoe je een model checker kunt gebruiken voor het oplossen van puzzels en denkspellen zoals "De wolf, de geit en de kool" en "Rush hour". Er zijn ook een paar meer geavanceerde facultatieve onderwerpen zoals algoritmen voor mutual exclusion, gedistribueerde algoritmen voor het kiezen van een leider in een ring, en het alternerend bit protocol (een vereenvoudigde versie van een algoritme dat gebruikt wordt binnen het internet). Doel van de cursus is dat je leert werken met een model checker, in het bijzonder aanpassingen kunt maken aan bestaande modellen, zelf eenvoudige modellen kunt construeren, en gewenste eigenschappen kunt formuleren en uitrekenen met behulp van een model checker.
Laatste aanpassing gemaakt op 17/08/2012 door Frits Vaandrager.