Ifi forskning:  Presis modellering og analyse (PMA) English

Personer  |  Forskning  |  Undervisning  |  Masteroppgaver

Ledige masteroppgaver ved PMA

Noen oppgaver er av teoretisk art, noen er av mer praktisk rettet og noen er litt av begge deler. Vi har her gruppert oppgavene innen aktuelle temaer/prosjekter. Med mindre noe annet er skrevet, vil oppgavene gis som såkalte "lange" oppgaver.

Kortoppgaver kan gis ved forespørsel.

Hvis du er interessert i en oppgave, kan du henvende deg til en aktuell veileder.

Vi er alltid interesserte i å knytte flinke studenter til PMA gruppen. Under følger en beskrivelse av noen
mulige masteroppgaver, men vi diskuterer gjerne andre forslag. Ta kontakt med oss så tar vi et møte.

Nye Oppgavene

Creol/Connect/Credo-prosjektene

Creol-prosjektet går ut på å utvikle et rammeverk som er egnet for modellering av objekt-orienterte og distribuerte systemer. I tråd med basale objekt-orienterte prinsipper ønsker vi la objektene svare til parallelle prosesser og la objekter snakke sammen ved hjelp av metode-kall. En distribuert setting krever da at man finner en hensiktsmessig form for asynkron kommunikasjon, der et objekt kan sette i gang flere kall og så plukke opp svarene (fra metodekallene) på en mest mulig fleksibel måte.

Et høy-nivå språk (Creol) sammen med abstrakt maskin, interpret, kompilator og analyseverktøy er under utvikling, implementert i Maude etter byggekloss-prinsippet. Det lyses ut flere oppgaver, som spenner fra utvikling og implementasjon av byggeklosser i Maude-rammeverket, eksperimentering med Maude-rammeverket, utvidelser av språket i ulike retninger og teori.

Creol-prosjektets hjemmeside finner du her: heim.ifi.uio.no/~creol.

Personer: Einar Broch Johnsen, Olaf Owe, Bjarte M. Østvold, Johan Dovland, Ingrid C. Yu, Arild Torjussen.

Lange masteroppgaver: Generelt

Det er mulighet for lange masteroppgaver i forbindelse med Creol. En slik oppgave kan være rent teoretisk eller den kan se på praktiske aspekter ved f.eks. typeanalyse eller kjøretidsystemet. Oppgavene kan være basert på Maude hvis ønskelig. Noen forslag til slike oppgaver er gitt under, men andre problemstillinger er mulig. Kom gjerne innom for en prat om mulig oppgave!

Kontaktpersoner: Einar Broch Johnsen, Olaf Owe

System for analyse av klasse-invarianter

I en distribuert og dynamisk omgivelse kan det være viktig å angi krav til omgivelsene og å ha garantier for at objekter har visse egenskaper. I Creol er vi derfor interessert i å gjøre formelle analyse av tilstanden og oppførselen til objekter. Klasse-deklarasjoner i Creol inkluderer angivelse av krav til omgivelsene, og garantier i form av såkalte klasse-invarianter. Invarianter kan gjøres til gjenstand for formell analyse av egenskaper.

Vi ønsker å implementere en analysator for klasse-invarianter og mer generelt, for tilstandspredikater ved hjelp av Hoare-logikk. Hoare-logikk er et formelt system for å beskrive hvordan en systemtilstand endres av programsetninger.

Oppgaven går ut på å finne en hensiktsmessig struktur for underliggende programvare (implementert i Maude) for en slik analysator, samt implementasjon av analyse for basale setninger. Man skal også diskutere hvordan forenkling av utsagn (tilstandspredikater) best kan innpasses.

Relevante kurs:
INF3230 - Formell modellering og analyse av kommuniserende systemer
INF3140 - Modeller for parallellitet
INF3170 - Logikk og analysemetoder

Programmeringsspråk: Maude.

Veiledere: Einar Broch Johnsen, Johan Dovland

Eksperimentering med case-studier i Creol

Oppgaven går ut på først å utarbeide et utvalg case-studier i Creol, med tanke på å bygge opp et eksempel-bibliotek. Case-studier som dekker prinsipielle aspekter og problemstillinger ved distribuerte systemer vil bli valgt.

Man skal eksperimentere med eksekvering av case-studiene ved hjelp av Creol-rammeverket og den abstrakt maskinen. Spesielt skal man se på effektivitet ved bruk av ulike forutsetninger om underliggende meldingsutveksling (bl.a. kø-ordninger), og dessuten på program-kompleksitet og riktighet.

Studiene skal lede til en diskusjon omkring egnetheten av Creol, og evt. forslag til utvidelser/forbedringer av språket.

Relevante kurs:
INF3230 - Formell modellering og analyse av kommuniserende systemer
INF3140 - Modeller for parallellitet
Evt. operativsystemkurs

Veileder: Einar Broch Johnsen, Arild Torjussen

Modellering av Hikernet-protokollen i Creol

HikerNet er et store-and-forward meldingssystem beregnet for områder uten vanlig datakommunikasjon. Transport av meldinger skjer ved at man bærer små enheter (f.eks. mobiltelefoner) med seg. Disse enhetene har mulighet for dataoverføring over korte avstander (f.eks. bluetooth), der meldingene blir utvekslet med peer-to-peer metoder i et ad-hoc nettverk. Oppgaven går ut på først å modellere de underliggende prinsippene av HikerNet i Creol, for så å gjennomføre en simulering av visse aspekter av HikerNet. Dette er en case-study som dekker prinsipielle aspekter og problemstillinger ved distribuerte systemer.

Man skal eksperimentere med eksekvering av case-studiene ved hjelp av Creol-rammeverket og den abstrakt maskinen ved å bruke HikerNet som eksempel. Spesielt skal man se på effektivitet ved bruk av ulike forutsetninger om underliggende meldingsutveksling, og dessuten på program-kompleksitet og riktighet.

Studiene skal lede til en diskusjon omkring egnetheten av Creol, og evt. forslag til utvidelser/forbedringer av språket. Samtidig skal simuleringsresultatene være egnet til å gi idéer i hvilken retning HikerNet skal videreutvikles.

Relevante kurs:
INF3230 - Formell modellering og analyse av kommuniserende systemer
INF3140 - Modeller for parallellitet
INF3090 - Datakommunikasjon
evtl. INF 5090 - Advanced Topics in Distributed Computing

Ekstern Veileder: Wolfgang Leister, Norsk Regnesentral

Intern Veileder: Olav Owe, Einar Broch Johnsen

Korte masteroppgaver:

Korte masteroppgaver kan tilbys. Disse involverer programmering/implementasjon i Maude, eller eksperimentering.

Relevante kurs:
INF3230 - Formell modellering og analyse av kommuniserende systemer
INF3140 - Modeller for parallellitet

Kontaktperson: Einar Broch Johnsen, Olaf Owe

Spesifikasjon og analyse i Maude

Maude er et fleksibelt høynivå språk og verktøy for spesifikasjon og analyse. Maude har blitt anvendt på en lang rekke forskjellige systemer, fra sikkerhetsprotokoller, programanalyse, hybride og sanntidssystemer til biologiske prosesser. Det er mulighet for både lange og korte oppgaver relatert til Maude. Aktuelle oppgaver kan gå ut på alt fra å utvikle deler av verktøyet til å anvende det på et konkret problem.

Webside: Maude

Relevante kurs:
INF3230 - Formell modellering og analyse av kommuniserende systemer
INF3140 - Modeller for parallellitet
INF3170 - Logikk og analysemetoder
INF5130 - Utvalgte emner i omskrivningslogikk
INF5140 - Kravspesifikasjon og verifikasjon av parallelle systemer

Kontaktpersoner: Peter Ölveczky, Einar Broch Johnsen, Olaf Owe.

Lange masteroppgaver:

Tilfeldige eksekveringer i Maude

Maude tilbyr kommandoene rew og frew for å eksekvere spesifikasjoner, og search for å lete gjennom alle mulige eksekveringer. Mange ganger vil antallet mulige eksekveringer være temmelig stort, f.eks. i NSPK protokollen eller i modeller av distribuerte systemer med mye ikke-determinisme. Da kan det være attraktivt med en strategi (kommando) for å kunne kjøre en serie med ulike testkjøringer. Dette er ikke mulig vha. rew og frew, disse vil gi samme resultat hver gang de anvendes på en spesifikasjon.

Oppgaven går ut på å utvikle og implementere en hensiktsmessig strategi for tilfeldig eksekvering i Maude, og utvide systemet med en tilhørende kommando random-rew[n] init for å utføre en serie på n ulike eksekveringer fra samme initialtilstand init.

Relevante kurs:
INF3230 - Formell modellering og analyse av kommuniserende systemer
INF3170 - Logikk og analysemetoder
INF5130 - Utvalgte emner i omskrivningslogikk

Programmeringsspråk: Maude.

Veileder: Einar Broch Johnsen, Arild Torjussen

Real-Time Maude: Generelt

Real-Time Maude er en utvidelse av Maude språket og systemet som tar for seg sanntidsmodellering. Det er mulighet for lange masteroppgaver basert på Real-Time Maude.

denne siden finner du noen forslag til både korte og lange oppgaver innen utvikling og bruk av verktøyet Real-Time Maude. (Se også nedenfor.)

Webside: Real-Time Maude

Veileder: Peter Ölveczky

Korte masteroppgaver:

Det er mulighet for kort masteroppgave knyttet til Maude eller Real-Time Maude.

Kontaktpersoner: Peter Ölveczky, Einar Broch Johnsen, Olaf Owe

Utvikling og bruk av Real-Time Maude

Real-Time Maude er en utvidelse av Maude til modellering og eksekvering/analyse av sanntids datasystemer. Real-Time Maude utvikles av Ølveczky og Meseguer.

Det tilbys oppgaver både til å videreutvikle verktøyet teoretisk og praktisk, og til å bruke verktøyet på interessante systemer som avanserte kommunikasjonsprotokoller, trådløse sensornettverk, tidsavhengige sikkerhetsprotokoller, etc.

Det tilbys både lange og korte oppgaver, bland annet en interessant oppgave sammen med Pål Halvorsen fra Nettverk og distribuerte systemer-gruppen omkring bruk av Real-Time Maude for å modellere og teste ut ulike idéer for å oppnå effektiv lokal rekonfigurering for interaktive multimedia applikasjoner.

Her er en liste av noen mulige korte og lange masteroppgaver som tilbys innen utvikling og bruk av Real-Time Maude.

Relevante kurs:
INF3230/4230 - Formell modellering og eksekvering av kommuniserende systemer

Kontaktperson: Peter Ölveczky

Logikk og automatisk bevissøk

Logikk er et sentralt verktøy i teoretisk databehandling og mange anvendelser krever spesialtilpassede kalkyler. I automatisk bevissøk studerer man spesielt teknikker som egner seg for maskinell behandling av søkerommet til et gitt problem. Bevissøk har vært et teoretisk fagområde, men blir nå stadig oftere integrert i store datasystemer.

Oppgavene forutsetter evne og interesse til å arbeide med teoretiske problemstillinger, samt være innstilt på å inngå i samarbeid. Oppgaven vil naturlig utføres i nært samarbeid med veilederne og andre masterstudenter ved PMA-gruppen.

Relevante kurs:
INF3170 - Logikk og analysemetoder
INF3200 - Algoritmer og effektivitet

Kontaktpersoner: Arild Waaler, Einar Broch Johnsen, Roger Antonsen, Olaf Owe, Anders Moen, Christian Mahesh Hansen.

Forfiningskalkylen i Isabelle

Forfiningskalkylen (Refinement Calculus) er et matematisk spesifikasjonsspråk for å utvikle programmer stegvis. Isabelle er en moderne teorembeviser utviklet i programmeringsspråket ML. Oppgaven går ut på å utvikle støtte i Isabelle for programutvikling i forfiningskalkylen. Dette gjøres ved å representere forfiningskalkylen som en teori i Isabelles høyere-ordens logikk. Oppgaven forutsetter en interesse for logikk og funksjonell programmering.

Relevante kurs:
INF4110 - Programmeringsspråk
INF4170 - Logikk og analysemetoder
INF4230 - Formell modellering og analyse av kommuniserende systemer
INF4140 - Modeller for parallellitet

Referanser:

  1. Isabelle
  2. Refinement Calculus

Veileder: Einar Broch Johnsen

TAcS-prosjektet

TAcS(Tableaux with Accelerated Search)-prosjektet tar sikte på å utvikle teknikker for logikker med stort potensiale innenfor databehandling. TAcS er et ambisiøst prosjekt som tar for seg nye teknikker for bevissøk og implementasjon av disse. Hvert år arrangeres et "verdensmesterskap" i logiske søkemotorer (The CADE ATP System Competition - http://www.cs.miami.edu/~tptp/CASC/) og et naturlig mål er å hevde seg her. Allerede er det fire personer som jobber fulltid med prosjektet sammen med internasjonale samarbeidspartnere. Vi tilbyr et stimulerende og engasjert miljø med tett oppfølging av masterstudentene. Ta kontakt.

Relevante kurs:
INF3170 - Logikk og analysemetoder
INF3200 - Algoritmer og effektivitet
INF5170 - Masterseminar i logikk

Kontaktpersoner: Arild Waaler, Christian Mahesh Hansen, Roger Antonsen, Espen Lian.

Sikkerhet og sårbarhet

Sikkerhetsmodellering og analyse i Maude: Generelt

Oppgavene går ut på å utvikle abstraksjoner av konkrete systemer, protokoller og sikkerhetsscenarier som tillater høy-nivå analyse vha. Maude. Det er mulighet for oppgaver i samarbeid med industri og næringsliv. En slik oppgave er konkretisert under.

Kontaktpersoner: Einar Broch Johnsen, Peter Ölveczky, Olaf Owe

Ende-til-ende kryptering vs. delvis kryptering i Web-baserte informasjonsregistre

En del av informasjonen som utveksles og lagres i forbindelse med innrapportering til det offentlige er sensitiv. I denne sammenhengen ønsker vi å få en sammenligning av sikkerheten i en modell med ende-til-ende kryptering, der data både kommuniseres og lagres kryptert, og en modell med kryptering kun i kommunikasjonsleddene. Hovedfokus bør legges på overgangen mellom kryptert / ikke-kryptert informasjonsutveksling.
Dette er et forslag til oppgave utarbeidet i samarbeid med Brønnøysundregistrene (ved Jeanine Lilleng), og knytter seg til problemstillinger innen Altinn-systemet, som bl.a. brukes til innlevering av selvangivelse over nettet.
Bakgrunnsstoff: Line Borgunds masteroppgave ved IFI fra April 05.
Kan passe for to studenter.

Veiledere: Einar Broch Johnsen, Olaf Owe, Jeanine Lilleng (Brønnøysundregistrene).

Mønstre for policybasert kontroll av offentlig nøkkel infrastruktur

En PKI (Public Key Infrastructure) er en infrastruktur for sikkerhet basert på elektroniske signaturer, kryptering og sertifikater. Overordna krav til sikkerhet og sikkerhetsløsninger uttrykkes ofte i form av policyer. Disse kravene kan med fordel dokumenteres som mønstre (patterns). Oppgaven går ut på å lage (1) metodikk for spesifikasjon av slike mønstre, og (2) verktøy for kontroll/evaluering av PKI-løsninger med utgangspunkt i slike mønstre.

Forkunnskap: Kunnskap om PKI vil være nyttig.

Bakgrunnslitteratur:

  1. Norges Offentlige Utredninger 2001: 10. Uten penn og blekk.
  2. Erich Gamma, Richard Helm, Ralf Johnson, and John Vlissides. Design patterns: Elements of reusable object-oriented software. Addison Wesley, 1994.

Veileder: Ketil Stølen

Utarbeidelse av formell semantikk for et språk for grafisk trusselmodellering

Ved SINTEF har det blitt utviklet et grafisk språk for modellering av trussel scenarier. Språket har blitt definert som en UML-profil og baserer seg på UML-usecase diagrammer. Språket er ment å understøtte kommunikasjon mellom ulike personer involvert i en sikkerhetsanalyse. Språket skal kunne forstås av folk uten teknisk kompetanse. Språket har en veldefinert syntaks og er ment å ha en intuitiv, lett forstålig semantikk. I mange sammenhenger er det imidlertid ønskelig med en mer presis og formell semantikk, ikke minst i forbindelse med automatisk analyse av spesifikasjoner. Oppgaven går ut på å utarbeide en slik formell semantikk.

Forkunnskap: Bakgrunn i predikatlogikk er en forutsetning. Bakgrunn i UML vil være nyttig.

Bakgrunnslitteratur:

  1. Teknisk beskrivelse av UML profil
  2. Eksempel på presis semantikk for UML diagrammer

Veileder: Ketil Stølen

Casebasert evaluering av STAIRS

STAIRS er en metode for stegvis utvikling av UML interaksjoner (f.eks. sekvensdiagrammer). STAIRS er praktisk rettet, men basert på prinsipper fra formelle metoder. En interaksjon spesifiserer en mengde positive og/eller negative oppførsler. STAIRS beskriver tre basissteg i systemutviklingen: supplering (oppførsler det tidligere ikke er sagt noe om, beskrives som enten positive eller negative), innsnevring (reduserer mengden positive oppførsler) og detaljering (introduserer mer detaljerte beskrivelser). Oppgaven går ut på å evaluere nåværende versjon av STAIRS, primært ved å gjennomføre et større case. STAIRS er under stadig utvikling, og resultatene i oppgaven vil være viktige i det videre arbeidet.

Forkunnskap: Fordel med bakgrunn i UML og noe predikatlogikk. Bør ta/ha tatt INF5150 (tidligere INF-UIT).

Bakgrunnslitteratur:

  1. Teknisk beskrivelse av STAIRS

Veileder: Ketil Stølen

Integrasjon av UML-verktøy i CORAS-verktøyet

Ved SINTEF har det blitt utviklet et open source Java-basert verktøy for modell-basert risikoanalyse basert på UML (CORAS-verktøyet). Samvirke med eksterne verktøy som UML CASE-verktøy er for øyeblikket basert på dataintegrasjon ved hjelp av utveksling av filer i XML-format, f.eks. XMI for UML. Neste versjon av CORAS-verktøyet er under utvikling, og vi ønsker nå en direkte integrasjon med ett eller flere UML-verktøy som støtter modellering med CORAS UML-profilen. Oppgaven går ut på å (1) vurdere metoder for integrasjon med forskjellige UML-verktøy og (2) implementere integrasjon med et utvalgt UML-verktøy.

Forkunnskap:Bakgrunn i Java-utvikling er en forutsetning, fordel med kjennskap til J2EE, XML og UML/XMI.

Bakgrunnslitteratur:

  1. CORAS plattformen
  2. CORAS UML profil

Veileder: Ketil Stølen

Formelle Metoder

Minneanalyse av Java smartkort i Maude

Programmerbare smartkort er små personlige kort med en mikroprosessor som er i stand til å manipulere konfidensielle data. Applikasjoner for msartkort er vanligvis skrevet i et høy-nivå Java-aktig språk. Kompilert kan slike applikasjoner eksekveres på Java Card Virtual Machine (JCVM) som er en forenklet versjon av Java Virtual Machine (JVM). Minne er en begrenset ressurs på smartkort, derfor er det viktig å kunne garantere at en applikasjon ikke krever mer minne en tilgjengelig på smartkortet. Det finnes en implementasjon av JVM i Maude. Din oppgave blir å tilpasse denne til JCVM og deretter å utvikle en minneanalysator for bytekode i Maude som gjør det mulig å statisk avgjøre hva som er maksimalt minneforbruk for en gitt applikasjon.

Relevante kurs:
INF3230 - Formell modellering og analyse av kommuniserende systemer
INF3170 - Logikk og analysemetoder
INF5130 - Utvalgte emner i omskrivningslogikk
INF5110 - Kompilatorteknikk

Veiledere: Gerardo Schneider, Einar Broch Johnsen

Utarbeidelse av kompletthetsbegrep for antagelse-garanti kalkyler

Antagelse-garanti kalkyler har blitt utviklet for å muliggjøre modulær resonering om distribuerte systemer. Som en konsekvens av Gødels ufullstendighetsteorem er slike kalkyler ufullstendige i det generelle tilfellet. Begrepet "relativ fullstendighet" (relative completeness) har blitt foreslått som et alternativ. Dette begrepet er imidlertid for svakt for antagelse-garanti kalkyler. Oppgaven går ut på å definere og motivere et mer egnet fullstendighetsbegrep.

Forkunnskap: Bakgrunn i predikatlogikk og formell bevisførsel er en forutsetning.

Bakgrunnslitteratur:

  1. Assumption/commitment rules for dataflow networks - with an emphasis on completeness. In Proc. 6th European Symposium on Programming (ESOP'96), LNCS 1058, pages 356-372, Springer, 1996.

Veileder: Ketil Stølen

Utarbeidelse av beviskalkyle for FOCUS-metoden

FOCUS er en formell metode inspirert av funksjonell programmering for spesifikasjon og utvikling av distribuerte systemer. Metoden er basert på en enkel og presis matematisk semantikk. FOCUS tilbyr et antall ulike spesifikasjonsstiler samt karakteriseringer av hva det betyr for en spesifikasjon å raffinere eller implementere en annen spesifikasjon. Oppgaven går ut på å utarbeide en beviskalkyle for FOCUS-metoden

Forkunnskap: Bakgrunn i predikatlogikk er en forutsetning.

Bakgrunnslitteratur:

  1. Kortfattet oversikt over FOCUS-metoden
  2. FOCUS-boka

Veileder: Ketil Stølen

Klassifisering av teknikker for modulær bevisførsel med mytiske variable

Mytiske variable har lenge blitt brukt for å øke beviskraften til beviskalkyler for distribuerte systemer. Oppgaven består i å klassifisere og relatere ulike teknikker for bevisførsel med mytiske variable. Teknikker for modulær resonering med mytiske variable skal vektlegges.

Forkunnskap: Bakgrunn i predikatlogikk og formell bevisførsel er en forutsetning.

Bakgrunnslitteratur:

  1. A method for the development of totally correct shared-state parallel programs. In Proc. 2nd International Conference on Concurrency Theory (CONCUR'91), LNCS 527, pages 510-525, Springer, 1991.

Veileder: Ketil Stølen

MAL: