Concurrency (Datalogi)

Q1 2009, 5 ECTS

Kurset vil dække følgende emner:

Deltagerne skal ved afslutningen af kurset kunne

Kurset er forbeholdt studerende på datalogi. De første uger af kurset er fælles med Concurrency (IT / Teknisk IT). Kursets sidste del bygger på dRegAut og dBerLog.

Forelæser

Anders Møller <amoeller@cs.au.dk>

Materiale

Kurset tager udgangspunkt i følgende bog:

[M&K] Jeff Magee og Jeff Kramer
Concurrency: State Models & Java Programming
2. udgave, Wiley, 2006
ISBN: 0470093560 / 0470093552

Desuden anvendes de første kapitler af denne:

[B&K] Christel Baier og Joost-Pieter Katoen
Principles of Model Checking
MIT Press, 2008
ISBN: 0-262-02649-X

Begge bøger kan købes i Stakbogladen Naturfag.

Kursusplan

Forelæsninger er fredage 11-14 i IT Huset, Store Aud. (Første forelæsning er flyttet til Søauditoriet, Aud. 4.) Øvelser er i den efterfølgende uge. Holdlister og instruktorer kan findes her.

TidEmner, slides og opgaver
uge 35
28. aug.

Concurrency i Java og proces-modeller i FSP

(Forelæsning i Søauditoriet, Aud. 4)

slides (til print)

[M&K] kap. 1-4
FSP Quick Reference
java.lang.Thread

Opgaver

uge 36
4. sep.

Concurrency konstruktioner og egenskaber

slides (til print)

[M&K] kap. 5-7

Opgaver

uge 37
11. sep.

Model-baseret design og verifikation

slides (til print)

[M&K] kap. 8+13 (samt dele af kap. 9-10)
Java memory model

Opgaver

uge 38
18. sep.

Introduktion til model-checking & semantik for FSP

slides (til print)
ekstra forklaring til slide 28

Forelæsningen forudsætter kendskab til basal matematisk notation om mængder, tupler og relationer.

Dele af [B&K] kap. 1-2 (spring gerne over afsnit 2.2.4, 2.2.6 og 2.3)

Opgaver

uge 39
25. sep.

Logiske specifikationer og temporal-logik (LTL)

slides (til print)

[M&K] kap. 14, [B&K] kap. 3 (ikke afsnit 3.3.1, 3.3.3 og 3.5.2-3) og afsnit 5.1 (ikke afsnit 5.1.4-5)

Opgaver

uge 40
2. okt.

Model-checking for regulære egenskaber

Inden forelæsningen, repetér definitionerne af nondeterministisk endelig automat (NFA) og sproget for en NFA fra Regularitet & Automater.

slides (til print)

[B&K] kap. 4 (ikke afsnit 4.3.4), afsnit 3.3.1

Opgaver

uge 41
9. okt.

Model-checking for LTL med Büchi-automater

slides (til print)

[B&K] afsnit 5.2 (kun s.270-278), desuden anbefales afsnit 4.3.4

Information til instruktorer.

Eksamen

Skriftlig eksamen (2 timer, uden bøger, noter, etc.). Se forsiden af eksamenssættet.

Alle afleveringsopgaver skal være godkendt før man kan komme til eksamen. Hvis du har fået godkendt afleveringsopgaverne et tidligere år, så kontakt forelæseren.

Pensum er kapitlerne angivet i kursusplanen samt forelæsnings-slides og opgaver.

Tid og sted: 14. okt. 2009 kl. 9.00-11.00, Trøjborg, Willemoesgade 15
Reeksamen: 19. jan. 2010 kl. 9.00-11.00, IT Huset Lille Aud.