Den studerende skal 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
verifikationsteknikker for realtidsmodeller
evt. andre emne from modelverifikation som f.eks. partial order reduktion eller probabilistiske modeller og ræsonnementsteknikker
Kursusmodulet kan derudover inddrage andre formelle modeller.
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
Undervisningen tilrettelægges i henhold til de generelle undervisningsformer for uddannelsen jf. § 17.
Det forventes at den studerende bruger 27,5 timer per ECTS, hvilket for denne aktivitet betyder 137,5 timer.
Prøvens navn | Modellering og verifikation |
Prøveform | Skriftlig eller mundtlig |
ECTS | 5 |
Bedømmelsesform | 7-trins-skala |
Censur | Intern prøve |
Vurderingskriterier | Vurderingskriterierne er angivet i Universitetets eksamensordning |
Kontakt: Studienævn for datalogi via cs-sn@cs.aau.dk eller 9940 8854
Engelsk titel | Modelling and Verification |
Modulkode | DSNDATB612 |
Modultype | Kursus |
Varighed | 1 semester |
Semester | Forår
|
ECTS | 5 |
Undervisningssprog | Dansk og engelsk |
Tomplads | Ja |
Undervisningssted | Campus Aalborg |
Modulansvarlig |
Uddannelsesejer | Bachelor (BSc) i datalogi |
Studienævn | Studienævn for Datalogi |
Institut | Institut for Datalogi |
Fakultet | Det Teknisk Fakultet for IT og Design |