INF9130 – 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 INF9130
- 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
Ph.d.-kandidater ved UiO s?ker plass p? undervisningen og melder seg til eksamen i Studentweb.
Hvis emnet har begrenset kapasitet, vil ph.d.-kandidater som har emnet i sin utdanningsplan ved UiO bli prioritert. Noen nasjonale forskerskoler kan ha egne regler for rangering av s?kere til emner med begrenset kapasitet.
Ph.d.-kandidater som har opptak ved andre utdanningsinstitusjoner m? innen angitt frist s?ke om hospitantplass.
Forkunnskaper
Anbefalte forkunnskaper
Emnet bygger p? INF3230 – Formell modellering og analyse av kommuniserende systemer (videref?rt) /INF4231 – Formell modellering og analyse av kommuniserende systemer (videref?rt)INF220
Overlappende emner
10 studiepoeng overlapp mot INF5130 – 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 亚博娱乐官网_亚博pt手机客户端登录 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 best?tt/ikke best?tt. 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.