Concurrency

Q1 2011, 5 ECTS

Kurset vil dække følgende emner:

Deltagerne skal ved afslutningen af kurset kunne

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 / 9780470093559

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

TidEmner, slides og opgaver
uge 34
26. aug.

Concurrency i Java og proces-modeller i FSP

Øvelser starter ugen efter!

slides (til print)

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

Opgaver

uge 35
2. sep.

Concurrency konstruktioner og egenskaber

slides (til print)

[M&K] kap. 5-7

Opgaver

uge 36
9. 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 37
16. sep.

Introduktion til model-checking & semantik for FSP

(Forelæsning ved Michael Schwartzbach)

slides (til print)
ekstra forklaring til slide 28

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

Opgaver

uge 38
23. 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 39
30. sep.

Model-checking for regulære egenskaber

(Forelæsning ved Jan Midtgaard)

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 40
7. 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 (og nogle eksempler på spørgsmål).

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.

Eksamen er 12. oktober kl. 12.30-14.30, Trøjborg, Willemoesgade 15, bygn. 2113, lok. 139. Reeksamen: lørdag 14. jan. 2012 kl. 9.00-11.00.