Faglig innhold

Kjernen i dette faget er et kræsjkurs i CSP - Communicating Sequential Processes. Dette illustrerer en gren av teoretisk/matematisk underlag under datavitenskap og gir en god forståelse for grunnlaget for formell verifikasjon av programvare og design i tillegg til modellering av parallelle systemer og 'refinement' konseptet.

I tillegg gjennomføres et relevant prosjekt hvor synergi med kandidatens forskning tilstrebes.

Læringsutbytte

Kunnskap:

• Inngående kjennskap til CSP som modelleringsspråk. (CSP's syntaks, hendelser og prosesser. Fundamentale operatorer: prefiksing, rekursjon, mu-rekursjon, alternativer Paralleloperatorer, alfabetisert, flettet og synkronisert. Kanaler og piping i CSP. Sekvenser, terminering, SKIP vs STOP.)
• God forståelse av divergens i CSP. (CSP hiding, renaming og hvordan hiding og renaming virker inn på divergens.)
• God forståelse av traces, failures og refinement.
• God forståelse av CSP's definisjon av ulike typer refinement og hvordan refinement kan brukes til å sjekke om en prosess følger en spesifikasjon.
• Kjennskap til den generelle bufferprosessen, og hvordan denne kan brukes til å sjekke korrekthet i kommunikasjonsprotokoller.

Ferdigheter:

• Kunne skrive modeller i maskinlesbar CSP for bruk med FDR3.
• Kunne bruke FDR3 til å sjekke egenskaper i systemer definert med CSP.

Generell kompetanse

• Innføring i en prosessalgebra
• Bedre kjennskap til det teoretiske fundamentet under datavitenskap.
• Bruk av abstrakt matematikk

Læringsformer og aktiviteter

Forelesninger og prosjekt.

Obligatoriske aktiviteter

• Øvinger

Anbefalte forkunnskaper

Det er en fordel med kunnskaper tilsvarende TTK4145 Sanntidsprogrammering.

Kursmateriell

A.W. Roscoe: The Theory and Practice of Concurrency. Annen pensumlitteratur og støttelitteratur oppgis ved semesterstart.