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
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 datamatbaserede specifikations-værktøjer.
