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?

      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?