Formelle metoder

Emnet undervises annet hvert år, neste gang vår 2026. Fokus er på teori for validering og verifikasjon av nett og nettbasert tjenestefunksjonalitet spesifisert vha. kommuniserende tilstandsmaskiner, processalgebraiske formler og temporallogiske beskrivelser. Teorien omfatter verifikasjon med prosessalgebra, temporallogikk, og deduksjon fra randbetingelser (constraints) i UML. Mht. verifikasjonsverktøy vil model checkers, theorem provers, SAT og SMT solvers bli diskutert.

A. Kunnskap:

1. En god innsikt i muligheter, metoder og utfordringer innen formal modellering, verifikasjon og utvikling av funksjonale egenskaper i informasjon- og kommunikasjons-teknologiske (IKT) systemer.
2. Dybdekunnskap på å beherske de forskjellige tekniske fremgangsmåtene å spesifisere systemer på en modular måte og å verifisere at systemene oppfyller spesielle system egenskaper.
3. Basiskunnskap om verifiseringsverktøy som theorem provers og model checkers.

B. Ferdigheter:

1. Beherske terminologi og begrepsdannelse innen området av formal spesifisering og verifikasjon.
2. Kunne spesifisere modeller for IKT systemer basert på automater, temporal logikk og protokollalgebra.
3. Beherske verifikasjon av invariante systemegenskaper.
4. Beherske enkle raffineringsbeviser at en mer detaljert oppfyller en mer abstrakt systemspesifikasjon.

C. Generell kompetanse:

1. Bedret innsyn i fordelene av formal systemutvikling sammenlignet med uformell programmering.

Forelesninger, selvstudium, kollokvier og øvinger. Et gruppearbeid basert på bruk av modellsjekkeverktøyet TLC.