Kurset har til formål at give deltagerne færdigheder i matematisk
baserede metoder til udvikling af pålidelige
programmelsystemer.
Læringsmål:
En studerende, der fuldt ud har opfyldt kursets mål, vil kunne:
opstille en formel specifikation ud fra en uformel
opgavebeskrivelse
anvende udvalgte specifikations-stile og -teknikker til at
konstruere modeller på et passende abstraktionsniveau
trinvis forfine en specifikation
opstille verifikationsforpligtelser (f.eks.
forfiningsbetingelser og krævede systemegenskaber)
verificere simple verifikationsforpligtelser
oversætte en specifikation til et udførbart program
anvende udvalgte værktøjer relateret til formelle metoder
forklare hvad der kan opnås ved brug af formelle metoder
kommunikere resultater på en klar og præcis måde
løse opgaver i en gruppe påtagende sig individuelt
ansvar
Kursusindhold:
Formel specifikation med udgangspunkt i et eller flere typiske
eksempler på specifikationssprog. Forskellige
specifikationsteknikker og stile til at konstruere modeller på
forskellige abstraktionsniveauer. Trinvis udvikling og
verifikation.
Implementeringsrelation(er). Anvendelse af computer-baserede
specifikations-værktøjer.