TK8112 - Sanntidsteori

Om emnet

Undervises ikke studieåret 2017/2018

Faglig innhold

CSP som prosessalgebra. Prosesskomposisjon; hendelser, alfabeter,
sekvenser, alfabetisert parallell og fletting. Terminering, sporing,
feiling og divergens. CSP-prosesser som
transisjonssystemer/tilstandsmaskiner. Analyse av spor. Algebraiske
regler for CSP. Grader av abstraksjon. Modellering av diskret tid ved
klokketikk. Modellering av programmer og sanntidssystemer i CSP.
Påvisning av sanntidsegenskaper ved hjelp av FDR.

Læringsutbytte

Kandidaten skal kunne:
A) Kunnskap: 1) 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.) 2) God forståelse av divergens i CSP. (CSP hiding, renaming og hvordan hiding og renaming virker inn på divergens.) 3) God forståelse av traces, failures og refinement. 4) 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. 5) Kjenskap til den generelle bufferprosessen, og hvordan denne kan brukes til å sjekke korrekthet i kommunikasjonsprotokoller. B) Ferdigheter: 1) Kunne skrive modeller i maskinlesbar CSP for bruk med FSR2. 2) Kunne bruke FDR2 til å sjekke egenskaper i systemer definert med CSP. C) Generell kompetanse 1) Innføring i en prosessalgebra 2) Bruk av abstrakt matematikk

Læringsformer og aktiviteter

Selvstudium, Kolokvier, Øvinger.

Obligatoriske aktiviteter

  • Øvinger

Spesielle vilkår

Vurderingsmelding krever godkjent undervisningsmelding samme semester. Obligatorisk aktivitet fra tidligere semester kan godkjennes av instituttet.

Kursmateriell

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

Eksamensinfo

  • * Skriftlig eksamen plasseres på rom 3 dager før eksamensdato.
Hvis mer enn ett rom er oppgitt, finner du ditt rom på Studentweb.