• Studier
• Emner
• Matematikk og naturvitenskap
• Informatikk
  • INF3230

INF3230 - 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.

Målet med kurset er at studentene skal:

• 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 prototyper for ulike slags systemer
• kunne teste ut prototyper og modeller

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

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 /INF1020 - Algoritmer og datastrukturer /INF 110.

Overlapping

10 studiepoeng mot INF4230 - 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. Les mer om krav til innlevering av oppgaver, gruppearbeid og lovlig samarbeid under retningslinjer for obligatoriske oppgaver.

Vurdering og eksamen

Skriftlig (4 timer) avsluttende eksamen. Alle obligatoriske oppgaver må være bestått for å kunne gå opp til eksamen. Generell informasjon om eksamen.

Hjelpemidler

Alle trykte og skrevne hjelpemidler tillatt.

Sensur

Emnet bruker gradert bokstavkarakterskala fra A til F, der A er beste karakter og F er stryk. Les mer om karakterskalaen .

Tilsynssensor for emnet er Michal Walicki.

Emnet har en tilsynssensor som vurderer den helhetlige faglige kvaliteten på emnet, inkludert vurderingsordningene.

Adgang til utsatt eller ny eksamen/vurdering

Dette emnet tilbyr ikke ny eksamen i begynnelsen av påfølgende semester til kandidater som stryker eller trekker seg under ordinær eksamen. For generelle opplysninger om ny og utsatt eksamen, se http://www.mn.uio.no/studier/admin/eksamen/utsatt-og-ny-eksamen/index.html

Trekk fra eksamen og antall eksamensforsøk

Ved praktisering av 3-gangers regelen skal emnet sees i sammenheng med INF4230, INF220 og INF220A.

En student kan fremstille seg til eksamen i dette emnet inntil tre ganger. Studenten anses å ha fremstilt seg til eksamen dersom hun/han ikke har trukket eksamensmeldingen sin i StudentWeb innen en gitt frist.

Annet

Det er sterkt anbefalt å møte på første forelesning fordi det vil bli gitt viktig informasjon.

Kontakt oss