INF4231 – Formell modellering og analyse av kommuniserende systemer

Timeplan, pensum og eksamensdato

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.

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 澳门葡京手机版app下载 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.

Fakta om emnet

Studiepoeng
10
Niv?
Master
Undervisning
Hver v?r

Dette emnet vil v?ren 2017 endres til INF4232

Eksamen
Hver v?r
Undervisningsspr?k
Norsk (engelsk p? foresp?rsel)