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 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, 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: http://www.mn.uio.no/studier/admin/eksamen/utsatt-og-ny-eksamen/.
Mer informasjon om eksamen ved MN-fakultetet kan du lese på fakultetets eksamenssider: http://www.mn.uio.no/studier/admin/eksamen/.
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