[an error occurred while processing this directive]

Forskning ved Presis modellering og analyse (PMA)

Se også på FRIDA

Gruppen interesserer seg for grunnleggende teori innen databehandling, særlig med henblikk på formelle metoder som hjelpemidler for program- og systemutvikling. Vårt fokus er formelle språk og verktøy for spesifikasjon og analyse. Mer konkret arbeider vi med objekt-orienterte og applikative språk som understøtter parallellitet, modularitet og distribusjon; semantikk for slike språk; teori for typing; programmeringsmetodikk; forfiningskalkyler; logikk og bevissystemer; verifikasjon; og verktøy for semiautomatiske resonnementer.

Creol/Connect (Owe, Johnsen, Dovland, Torjusen, Yu, Bjørk):

Spesifikasjon, design og formell analyse av åpne, distribuerte, objekt-orienterte systemer. Rollebetingelser som uttrykker tilgjengelige tjenester og gjensidig avhengighet mellom objekter. Et hovedmål ved prosjektet er å utvikle en formell og eksekverbar modell for å resonnere om oppgraderinger og andre modifikasjoner i distribuerte systemer.

I Connect-prosjektet utvides dette rammeverket mot sømløse og trådløse systemer.

For mer informasjon, se Creol-siden og Connect-siden.

Credo (Owe, Johnsen, Dovland, Torjusen, Yu, Steffen, Kyas, Liang):

Rammeverk for modellering og analyse av programvare for dynamiske nett og rekonfigurerbare systemer. Bygger på Creol.

For mer informasjon, se den lokale Credo-siden og den offisielle Credo-siden.

Contracts for Internet Services (Schneider, Prisacariu, Owe):

Contract-Oriented Software Development for Internet Services is a Nordunet3 project. The aim of this project is to develop novel approaches to implement and reason about contracts in a service oriented architecture. The fundamental insight is that system developers lack appropriate abstraction mechanisms to work with these architectures. Therefore the goal is to design and give proof of usefulness of system modeling and programming language tools to empower SOA developers to deploy highly dynamic, negotiable and monitorable Internet services.

For mer informasjon, se prosjekt-siden.

Maude (Ølveczky, Owe, Johnsen, Schneider):

Maude er et state-of-the-art og intuitivt system for modellering og prototyping av distribuerte systemer og protokoller. I tillegg tilbyr systemet en rekke fasiliteter for testing og analyse av egenskaper ved modellen. Maude-systemet er basert på omskrivingslogikk. Vi tilbyr både et introduksjonskurs til Maude og et mer avansert kurs i omskrivingslogikk ved PMA-gruppa. Maude er en generell formalisme som har vært anvendt på en rekke systemer med ulike kommunikasjonsformer. Vi har god erfaring med bruk av Maude og omskrivingslogikk til modellering og analyse av bl.a. objekt-orienterte systemer og avanserte kommunikasjons- og sikkerhetsprotokoller.

Generell informasjon om Maude finnes på Maude-siden.

Real Time Maude er et verktøy for prototyping, testing og modell-sjekking av sanntids- og hybride systemer. Dette verktøyet er utviklet av Ølveczky og videre utvikling av verktøyet og anvendelser av dette er et aktivt forskningsområde.

Prosjekter:
  • RHYTM: High-Level Formal Modeling and Analysis of Real-Time and Hybrid Systems (NFR: frie midler, 2 stipendiater)

    Sikkerhet og sårbarhet (Owe, Johnsen, Ølveczky, Moen)

    Sikkerhet og sårbarhet av IT-systemer er et spesielt viktig tema i dagens samfunn. For å vurdere hvordan sikkerhet ivaretas i ulike typer kommunikasjonssystemer, er formelle analysemetoder helt avgjørende. I dette prosjektet ønsker vi å adressere konkrete problemer i sikkerhets- og sårbarhetsanalyse av IT-systemer og annen infrastruktur i tett samarbeid med industri og næringsliv.

    For mer informasjon, ta kontakt med Einar B. Johnsen.

    Logikk og automatisk bevis-søk (Waaler, Antonsen, Johnsen):

    Bevissystemer, logikk, bevisteori, automatisk bevis-søk

    Løpende prosjekter

    Tidligere prosjekter