INF5130 – Utvalgte emner i omskrivningslogikk
Beskrivelse av emnet
Timeplan, pensum og eksamensdato
Kort om emnet
Emnet er en fortsettelse av INF3230 / INF4231 og tar for seg grunnleggende teori rundt omskrivningslogikk som Knuth-Bendix-komplettering, refleksjon og metaprogrammering, samt eksempler på avanserte anvendelser av omskrivningslogikk til modellering og analyse av systemer i verktøyet Maude. Aktuelle systemer å modellere kan være sikkerhets- og nettverksprotokoller, sanntidssystemer, mobile systemer og biokjemiske prosesser.
Hva lærer du?
Etter å ha tatt INF5130
- har du bedre kompetanse på formell modellering og analyse av
distribuerte systemer på et høyt abstraksjonsnivå, og spesielt
kunnskap om omskrivingslogikk-baserte verktøy,
- vet du hva meta-programmering er, og du forstår begrepene
refleksjon og metanivåberegning innen omskrivningslogikk;
spesielt kan du definere ad hoc strategier for gjennomføring og
analyse av Maude moduler ved hjelp av
meta-programmeringsmulighetene i Maude,
- har du god kjennskap av state-of-the-art anvendelser av
omskrivningslogikk innen bestemte domener, som for eksempel
biokjemiske prosesser, sanntidsdatasystemer og mobile prosesser,
- kan du spesifisere og analysere systemkrav ved bruk av temporal
logikk og modellsjekking, og særlig ved hjelp av Maudes
modellsjekker for lineær tid,
- kjenner du avanserte omskriving-logikk-baserte analyseteknikker
for distribuerte systemer som innsnevring og domenetilpassede
strategispråk,
- har du en bedre innsikt i hvordan å lese og forstå vitenskapelige artikler,
- har du bedre trening i vitenskapelige presentasjoner.
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å INF3230 – Formell modellering og analyse av kommuniserende systemer (videreført) /INF220
Overlappende emner
10 studiepoeng overlapp mot INF9130 – Utvalgte emner i omskrivningslogikk (videreført)
Undervisning
To til tre timer undervisning per uke (forelesning eller gruppeøvelse). Det kreves innlevering av obligatoriske oppgaver. Les mer om krav til innlevering av oppgaver, gruppearbeid og lovlig samarbeid under retningslinjer for obligatoriske oppgaver.
Eksamen
Studenten skal holde en muntlig presentasjon som teller 1/3 av den endelige karakteren. En muntlig eksamen teller 2/3. Dersom mange studenter følger emnet, kan eksamen bli skriftlig. De obligatoriske oppgavene må være bestått for å kunne gå opp til eksamen.
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.
Annet
Det er sterkt anbefalt å møte på første forelesning fordi det vil bli gitt viktig informasjon.