Faglig innhold

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.

Læringsutbytte

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.

Læringsformer og aktiviteter

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

Obligatoriske aktiviteter

• Gruppearbeid

Mer om vurdering

Karakterregel er bestått/ikke bestått, hvor en fastsatt poenggrense 70/100 poeng (70%) gir kandidaten karakter bestått.

Ved gjentak trenger godkjente obligatoriske aktiviteter ikke å gjentas.

Anbefalte forkunnskaper

Erfaring med tilstandsbaserte språk som SDL, UML og LOTOS.

Forkunnskapskrav

Kjennskap til endelige og utvidete tilstandsmaskiner.

Kursmateriell

Generelle artikler:

• E. Brinksma: What is the Method of Formal Methods, FORTE 91, Sydney November 1991.
• B. Pehrson: Protocol Verification for OSI, Computer Systems and ISDN Systems no. 18, 1989-1990.
• L. Lamport: The Temporal Logic of Actions, ACM Transactions of Programming Languages and Systems 16, 3 (May 1994) 872-923
• P. Herrmann, H. Krumm: A Framework for Modeling Transfer Protocols. In Computer Networks, 34(2000)2, 317-337.

Modellsjekkerne SPIN og TLC:

• G.J. Holzmann: SPIN Model Checker, The: Primer and Reference Manual. ISBN: 0-321-22862-6, Publisher: Addison Wesley Professional, 2004. http://www.aw-bc.com/catalog/academic/product/0,4096,0321228626-PRE,00.html
• Y. Yuan, P. Manolios, L. Lamport: Model checking TLA+ Specifications, CHARME'99, London, Springer 1999. 3) Prosessalgebra: R. Milner: Communication and Concurrency, Prentice Hall 1989, ISBN 0-13-115007-3 PBK.

Studiepoengreduksjon