Dette emnet er nedlagt

INF4230 – Formell modellering og analyse av kommuniserende systemer

Timeplan, pensum og eksamensdato

Velg semester

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)