| Website: | website containing additional information |
| Course code: | WIRIS |
| Credits: | 5.72 ECTS (=4 old credit points) |
| Period: | periode 5 (week 20 t/m 27, dwz 13-5-2002 t/m 5-7-2002; herkansing week 34)
|
| Participants: | up till now 15 subscriptions |
| Schedule: | Dit is een oud rooster!
|
| Contents: | De wereld wordt steeds meer afhankelijk van computertechnologie.
Het risico en de kosten van softwarefouten nemen natuurlijk ook
toe (denk er aan dat een softwarefout makkelijk een
miljarden guldens kostend ruimteschip kan opblazen).
Er zijn veel mensen die menen dat het risico en de kosten al een zorgwekkend
niveau hebben bereikt, daarom wordt er ook heel veel geinvesteerd in technologie
om de kwaliteit van software te verbeteren.
Computerondersteunde Verificatie (CV) is een opkomende techniek die veel
aandacht heeft getroken.
In dit college gaan we experimenteren met een aantal case studies
en software tools gebruiken om de correctheid van softwaresystemen
te verifieren.
We gebruiken SPIN en HOL.
SPIN is een zeer geautomatiseerde verficatietool,
en HOL is een zeer configureerbaar verificatieplatform.
Beide vertegenwoordigen de state-of-the-art van CV-technologie. |
| Literature: | HOL en SPIN manuals. Deze zijn te downloaden van uit de
website van het vak. |
| Course form: | Combinatie van hoorcollege, practicum, project, en seminarium. |
| Exam form: | Op basis van seminarium, projectbespreking, en practicum opdrachten. |
| Minimum effort to qualify for 2nd chance exam: | Om aan de aanvullende toets te mogen meedoen is ontbreken van ten hoogte 1 toetsactiviteit toegestaan. |
| Description: | Belangrijkste thema van de cursus :
- Formele modellen van gedistribueerde systemen
- Modelleren en verificatie van gedistribueerde systemen met SPIN
- Model checking algoritmen
- Semantische embedding van formele systemen in HOL
- Verificatie van wetten met HOL
HOL onderwerpen:
- Onderliggende HOL logic
- Uitbreiding van HOL logic : nieuwe constanten en nieuwe typen
- ML syntax van HOL
- Term en Theorem
- Achterwaarts bewijzen met tactic en goal
- Basis tactieken
- Conversies
- Theorem tactics en tacticals
Case studies
- Verificatie van parity checker (als introductie van programmeren van HOL)
- Embedding van sequentieel programmeer logica (HOL)
- Embedding en verificatie van compositionaliteit wetten (HOL)
- SPIN opdrachten (wordt tijdens de college nader gespecificeerd)
|
