INF4231 – 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 ressonering 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.
Etter å tatt dette emnet skal du:
- kunne modellere parallelle og distribuerte systemer
- forstå forskjellen på asynkrone og synkrone systemer
- forstå ulike former for kommunikasjon og nettverk
- kunne definere sine egne datastrukturer og tilhørende funksjoner
- kunne lage og teste ut prototyper og modeller for ulike slags systemer
- kunne definere temporallogiske formler som uttrykker avanserte egenskaper til distribuerte systemer
- kunne bruke analyseverktøy til å undersøke hvorvidt et gitt distribuert system tilfredsstiller en slik ønsket egenskap.
- kunne benytte metodene i kurset til å resonnere formelt om korrektheten av imperative 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å INF2220 – Algoritmer og datastrukturer (videreført) /INF1020 – Algoritmer og datastrukturer (nedlagt) /INF 110.
Overlappende emner
- 10 studiepoeng overlapp mot INF3230 – 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 samarbeid 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 INF3230, INF4230, INF220 og INF220A.
Annet
Det er sterkt anbefalt å møte på første forelesning fordi det vil bli gitt viktig informasjon.