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 lp VT2 jämna år. 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.