Concurrency (Semantik) (Q1) ( efterår 2008 - 5 ECTS )
Rammer for udbud
-
Uddannelsessprog:
engelsk (eller dansk)
-
Niveau:
Bachelorkursus
-
Semester/kvarter:
Q1 i /
-
Timer per uge:
6
-
Deltagerbegrænsning:
Ingen
-
Undervisningssted:
Århus
-
Hovedområde:
Det Naturvidenskabelige Fakultet
-
Udbud ID:
8421
Formål
Deltagerne vil efter kurset have indsigt i modelbaseret design, specifikation og verifikation af concurrent systemer og praktisk erfaring med thread programmering i Java og modelverifikationsværktøjer.
Obligatorisk program
Ugentlige afleveringsopgaver
Indhold
Concurrency-mekanismer i Java, korrekthedsegenskaber (safety og liveness), modelbaseret design af concurrent programmer, endelige tilstandsmodeller, temporal-logik (LTL), verifikation med Büchi-automater.
Læringsmål
Deltagerne skal ved afslutningen af kurset kunne:
-
beskrive
og
anvende
concurrency mekanismer i Java.
-
konstruere
modeller af concurrent systemer.
-
formulere
korrekthedsegenskaber.
-
beskrive
algoritmer for modelverifikation.
-
relatere
resultater af modelverifikation til egenskaber ved Java-programmer.
Faglige forudsætninger
dProgSprog, dRegAut, dBerLog
Underviser
Anders Møller
Undervisnings- og arbejdsform
Forelæsninger (3t/uge), holdøvelser (3t/uge)
Litteratur
Concurrency, State Models & Java Programming, Magee and Kramer, Wiley, 2006, ISBN 0470093560
Kursushjemmeside
http://www.daimi.au.dk/dConc
Skemaplacering (forelæsninger)
Blokpar F, fredag 11-14
Udbyder
Datalogisk Institut
Tilmelding til undervisning
https://mit.au.dk/da/index.cfm
Studieordning og bedømmelse
-
Skriftlig, bedømt efter 7-skala med intern censur
-
Skriftlig, bedømt efter 7-skala med intern censur
-
Skriftlig, bedømt efter 7-skala med intern censur
-
Skriftlig, bedømt efter 7-skala med intern censur
-
Skriftlig, bedømt efter 7-skala med intern censur
-
Skriftlig, bedømt efter 7-skala med intern censur
Skriftlig eksamen (2 timer)
7-skala, intern censur