Modellering og verifikation

2018/2019

Forudsætninger/Anbefalede forudsætninger for at deltage i modulet

Anbefalede faglige forudsætninger:
Modulet bygger videre på viden opnået i Syntaks og semantik samt Beregnelighed og kompleksitet.

Modulets indhold, forløb og pædagogik

Læringsmål

Viden

  • opnå viden om avancerede matematiske modeller til formel beskrivelse og verifikation af programmer, softwaresystemer og programmeringssprog med fokus på parallelle og kommunikerende systemer.

  • Specielt skal den studerende opnå viden om:

    • transitionssystemer
    • procesalgebra, f.eks. CCS
    • bisimulering
    • Hennessy-Milner logik med rekursion
    • Tarskis sætning om fikspunkter
    • modeller og ræsonnementsmetoder for realtidssystemer, f. eks. Timed CCS og tidsautomater
    • probabilistiske modeller og ræsonnementsteknikker, f. eks. probabilistiske proceskalkyler, ækvivalenser og logikker
    • verifikationsteknikker for realtidsmodeller
    • evt. andre verifikationsmetoder

Kursusmodulet kan derudover inddrage andre formelle modeller.

Færdigheder

  • kunne redegøre præcist og ved brug af fagets terminologi og notation for vigtige teorier for beskrivelse og analyse af reaktive systemer
  • kunne anvende verifikationsværktøjer, der er baseret på formelle modeller
  • kunne gøre brug af de fornødne skriftlige færdigheder i disse sammenhænge

Kompetencer

  • kunne anvende formelle modeller og hermed forbundne verifikationsværktøjer til verifikation af softwaresystemer

Undervisningsform

Undervisningen tilrettelægges i henhold til de generelle undervisningsformer for uddannelsen, jf. kapitel 3

Omfang og forventet arbejdsindsats

Det forventes at den studerende bruger 30 timer per ECTS, hvilket for denne aktivitet betyder 150 timer.

Eksamen

Prøver

Prøvens navnModellering og verifikation
Prøveform
Skriftlig eller mundtlig
ECTS5
Bedømmelsesform7-trins-skala
CensurIntern prøve
VurderingskriterierSom angivet i Fakultets vurderingskriterier
http:/​/​www.tech.aau.dk/​digitalAssets/​337/​337434_vurderingskriterier.pdf

Yderligere informationer

Kontakt: Studienævn for datalogi via cs-sn@cs.aau.dk eller 9940 8854

 

Fakta om modulet

Engelsk titelModeling and Verification
ModulkodeDSNDATFB603
ModultypeKursus
Varighed1 semester
SemesterForår
ECTS5
TompladsJa
UndervisningsstedCampus Aalborg
Modulansvarlig

Organisation

StudienævnStudienævnet for Datalogi
InstitutInstitut for Datalogi
FakultetDet Tekniske Fakultet for IT og Design