INF4230 – Formell modellering og analyse av kommuniserende systemer

Kort om emnet

Bruk av formelle metoder for modellering av og resonnering om kommuniserende distribuerte systemer. Det legges vekt p? h?yniv? objekt-orientert design og programmering samt verkt?ysbasert simulering/eksekvering og analyse. Ulike former for synkronisering behandles med vekt p? asynkron kommunikasjon ved meldingsutveksling. Emnet vil ta for seg konkrete ikke-trivielle eksempler som nettverksprotokoller, distribuerte databaser, sikkerhetsprotokoller og/eller Internettprogrammering.

Formalismen som benyttes bygger p? termomskrivningsteknikker. Emnet gir en innf?ring i operasjonell semantikk for abstrakte datatyper, modellering og maskinell testing/modellsjekking av kommuniserende systemer ved bruk av spr?ket og eksekveringsverkt?yet Maude, samt formell resonering om egenskaper som terminering og invarians.

Hva l?rer du?

Det overordnede m?let er ? vise hvordan formelle metoder kan benyttes til ? modellere kompliserte distribuerte systemer p? et h?yt abstraksjonsniv?, slik at man kan prototype, modellsjekke og resonnere om slike systemer i en tidlig fase i systemutviklingsprosessen. Emnet vil gi en praktisk innf?ring i utforming, programmering, kj?ring/testing og modellsjekking av distribuerte systemer, samtidig som det vil gi en teoretisk innsikt i formell resonnering om egenskaper til programmer.

Opptak og adgangsregulering

Studenter m? hvert semester s?ke og f? plass p? undervisningen og melde seg til eksamen i Studentweb.

Dersom du ikke allerede har studieplass ved UiO, kan du s?ke opptak til v?re studieprogrammer, eller s?ke om ? bli enkeltemnestudent.

Forkunnskaper

Anbefalte forkunnskaper

Emnet bygger p? INF1020 – Algoritmer og datastrukturer (nedlagt) /INF 110.

Overlappende emner

10 studiepoeng mot INF3230 – Formell modellering og analyse av kommuniserende systemer (videref?rt), 10 studiepoeng mot INF 220, 9 studiepoeng mot INF 220A og 3 studiepoeng mot IN 307.

Undervisning

3 timer forelesninger og 2 timer gruppe?velser per uke. Det kreves gjennomf?ring av obligatoriske oppgaver for ? kunne g? opp til eksamen.

Eksamen

Midtermineksamen (ca 37%). Skriftlig (3 timer) avsluttende eksamen (ca 63%). Bokstavkarakter (A - F).

Informasjon om utsatt pr?ve (kontinuasjon) finner du her: /studier/admin/eksamen/sykdom-utsatt/mn/index.html.

Mer informasjon om eksamen ved MN-fakultetet kan du lese p? fakultetets eksamenssider: http://www.mn.uio.no/studier/admin/index.html.

Annet

Det er obligatorisk oppm?te p? f?rste forelesning. Ved praktisering av 3-gangers regelen skal emnet sees i sammenheng med INF3230, INF220 og INF220A.

Tilsynssensor for emnet er: Michal Walicki

Fakta om emnet

Studiepoeng
10
Undervisning
V?r 2007
V?r 2006
V?r 2005
V?r 2004

Denne versjonen av emnet g?r for siste gang v?ren 2007. INF3230 – Formell modellering og analyse av kommuniserende systemer (videref?rt) vil videref?res.

Eksamen
Hver v?r
Undervisningsspr?k
Norsk (engelsk p? foresp?rsel)