INF4230 – Formell modellering og analyse av kommuniserende systemer
Beskrivelse av emnet
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