INF3230 – Formell modellering og analyse av kommuniserende systemer
Beskrivelse av emnet
Timeplan, pensum og eksamensdato
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?
Etter ? ha fullf?rt dette emnet skal du:
- kunne modellere distribuerte systemer p? et h?yt abstraksjonsniv?
- kunne resonnere matematisk om egenskaper til systemer, som f. eks. terminering og korrekthet
- forst? ulike former for kommunikasjon og nettverk
- kunne definere dine egne datastrukturer og tilh?rende funksjoner
- kunne lage og teste ut prototyper og modeller for ulike slags systemer
- kunne modellere og eksekvere bl. a. nettverksprotokoller og sikkerhetsprotokoller
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
Obligatoriske forkunnskaper
I tillegg til generell studiekompetanse eller realkompetanse m? du dekke spesielle opptakskrav:
- Matematikk R1 eller Matematikk (S1+S2)
De spesielle opptakskravene kan ogs? dekkes med fag fra videreg?ende oppl?ring f?r Kunnskapsl?ftet, eller p? andre m?ter. Les mer om spesielle opptakskrav.
Anbefalte forkunnskaper
Emnet bygger p? INF2220 – Algoritmer og datastrukturer (videref?rt) /INF1020 – Algoritmer og datastrukturer (nedlagt) /INF 110.
Overlappende emner
- 10 studiepoeng overlapp mot INF4231 – Formell modellering og analyse av kommuniserende systemer (videref?rt)
- 10 studiepoeng overlapp mot INF4230 – Formell modellering og analyse av kommuniserende systemer (nedlagt)
- 10 studiepoeng overlapp mot INF220
- 9 studiepoeng overlapp mot INF220A
- 3 studiepoeng overlapp mot IN307
- 9 studiepoeng overlapp mot INF3232 – Logikk for systemanalyse (videref?rt)
- 9 studiepoeng overlapp mot INF4232 – Logikk for systemanalyse (videref?rt)
Undervisning
3 timer forelesninger og 2 timer gruppe?velser per uke. Det kreves gjennomf?ring av obligatoriske oppgaver. Les mer om krav til innlevering av oppgaver, gruppearbeid og lovlig 澳门葡京手机版app下载 under retningslinjer for obligatoriske oppgaver.
Eksamen
Skriftlig (4 timer) avsluttende eksamen. Alle obligatoriske oppgaver m? v?re best?tt for ? kunne g? opp til eksamen.
Hjelpemidler
Alle trykte og skrevne hjelpemidler tillatt.
Karakterskala
Emnet bruker karakterskala fra A til F, der A er beste karakter og F er stryk. Les mer om karakterskalaen.
Begrunnelse og klage
Adgang til ny eller utsatt eksamen
Studenter som dokumenterer gyldig frav?r fra ordin?r eksamen, kan ta utsatt eksamen i starten av neste semester.
Det tilbys ikke ny eksamen til studenter som har trukket seg under ordin?r eksamen, eller som ikke har best?tt.
Trekk fra eksamen
Det er mulig ? ta eksamen i emnet inntil tre ganger. Dersom du trekker deg fra eksamen etter fristen eller under eksamen, bruker du et eksamensfors?k.
Ved praktisering av 3-gangers regelen skal emnet sees i sammenheng med INF4230, INF220 og INF220A.
Annet
Det er sterkt anbefalt ? m?te p? f?rste forelesning fordi det vil bli gitt viktig informasjon.