INF4232 – Logikk for systemanalyse
Beskrivelse av emnet
Kort om emnet
Emnet har to hovedmål:
1. Vise hvordan logiske metoder kan brukes til å modellere og resonnere om datatyper og distribuerte systemer.
2. Gi en høynivå innføring i distribuerte systemer.
Emnet introduserer ulike klasser av distribuerte distribuerte systemer, som transport-protokoller, database-protokoller, klassiske distribuerte algoritmer og sikkerhetsprotokoller. Ulike kommunikasjonsformer og litt feilhåndtering. Modellering og analyse av slike distribuerte systemer, og en innføring i ulike klasser av kravspesifikasjoner til distribuerte systemer. Formalisering av kravspesifikasjoner og analyse av hvorvidt et system tilfredsstiller en gitt kravspesifikasjon.
Likhetslogikk og omskrivingslogikk, og det assosierte analyseverktøyet Maude, brukes til å spesifisere og analysere systemene, i tillegg til matematiske resonnementer om egenskaper som terminering og invarians.
Hva lærer du?
Etter å ha fullført dette emnet:
- kjenner du til noen klassiske distribuerte systemer/algoritmer
- har du en forståelse for utfordringene knyttet til design av distribuerte systemer
- kan du modellere distribuerte systemer, som distribuerte algoritmer, nettverksprotokoller og sikkerhetsprotokoller, på et høyt abstraksjonsnivå
- kan du lage og teste ut prototyper/modeller for slike systemer
- kan du resonnere matematisk om egenskaper til systemer, som f. eks. terminering og korrekthet
- forstår du ulike former for kommunikasjon og nettverk
- kjenner du til sentrale klasser av krav som kan stilles til et distribuert system
- kan du formalisere kravspesifikasjoner og kan sjekke hvorvidt et gitt system tilfredsstiller sin kravspesifikasjon
Opptak og adgangsregulering
Studenter må hvert semester søke og få plass på undervisningen og melde seg til eksamen i Studentweb.
Studenter tatt opp til andre masterprogrammer kan, etter søknad, få adgang til emnet hvis dette er klarert med eget program.
Dersom du ikke allerede har studieplass ved UiO, kan du søke om opptak til våre studieprogrammer, eller søke om å bli enkeltemnestudent.
Overlappende emner
- 10 studiepoeng overlapp mot INF3232 – Logikk for systemanalyse (videreført)
- 9 studiepoeng overlapp mot INF4231 – Formell modellering og analyse av kommuniserende systemer (videreført)
- 9 studiepoeng overlapp mot INF4230 – Formell modellering og analyse av kommuniserende systemer (nedlagt)
- 9 studiepoeng overlapp mot INF3230 – Formell modellering og analyse av kommuniserende systemer (videreført)
- 9 studiepoeng overlapp mot IN220
- 9 studiepoeng overlapp mot IN220A
- 3 studiepoeng overlapp mot IN307
Undervisning
2 timer forelesninger og 2 timer gruppeøvelser per uke. Det er 3 obligatoriske øverler i emnet. Les mer om krav til innlevering av oppgaver, gruppearbeid og lovlig samarbeid under retningslinjer for obligatoriske oppgaver.
Eksamen
4 timers skriftlig digital eksamen. Obligatoriske øvelser må være godkjente før eksamen.
Hjelpemidler
Alle trykte og skrevne hjelpemidler er tillatt
Eksamensspråk
Du kan besvare eksamen på norsk, svensk, dansk eller engelsk.
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.
Som eksamensforsøk i dette emnet teller også forsøk i følgende tilsvarende emner: INF3232/3230/4231/4230
Tilrettelagt eksamen
Søknadskjema, krav og frist for tilrettelagt eksamen.