Antal poäng: 4. Betygskala: TH. Valfri för: D3, E4. Kursansvarig: Univ.lektor Lennart Andersson, Lennart.Andersson@cs.lth.se, Inst f datavetenskap. Förkunskapskrav: EDA040 Realtidsprogrammering. Prestationsbedömning: Skriftlig tentamen och inlämningsuppgifter. På inlämningsuppgiften ges ej graderat betyg. Studenterna förväntas presentera lösningar till förelagda problem vid seminarier. Detta tillgodoräknas vid första ordinarie tentamenstillfälle. Övrigt: Kursen kan komma att ges på engelska. Kursen är periodiserad. Den planeras att ges VT08. Kursen kan komma att ställas in vid mindre än 15 anmälda deltagare. Hemsida: http://www.cs.lth.se/EDA160.

Mål
Kursen skall ge förmåga att formellt beskriva och analysera kommunicerande och jämlöpande processer.

Innehåll
1. CCS, Calculus of Communicating Systems.

2. Petrinät.

3. Andra formalismer, temporallogik, händelsestrukturer.

Litteratur
Andersson, L.: Lecture notes. Distribueras av institutionen.
Milner,R : Communicating and Mobile Systems: the Pi-Calculus. Cambridge University Press. ISBN: 0-521-65869-1.