Dette emnet er erstattet av INF3232 - Logikk for systemanalyse.

INF3230 - Formell modellering og analyse av kommuniserende systemer

Timeplan, pensum og eksamensdato

Velg semester

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

Overlappende emner

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 INF4230, INF220 og INF220A.

Annet

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

Fakta om emnet

Studiepoeng

10

Nivå

Bachelor

Undervisning

Hver vår

Dette emnet vil våren 2017 endres til INF3232

Eksamen

Hver vår

Undervisningsspråk

Norsk (engelsk på forespørsel)