Faglig innhold

Emnet undervises annet hvert år, neste gang vår 2011.
Fokus er på teori for validering og verifikasjon av nett og nettbasert tjenestefunksjonalitet spesifisert vha. kommuniserende tilstandsmaskiner, processalgebraiske formler og temporallogiske beskrivelser. Teorien omfatter validering ved modellsjekking i ikke-reduserte tilstandsrom og verifikasjon med Prosessalgebra, Temporallogikk, Omskrivingslogikk (rewriting logic) og deduksjon fra randbetingelser (Constraints) i UML.

Læringsutbytte

Å kunne validere korrekthetsegenskapene av en funksjonell modell og å kunne verifisere konsistens mellom modeller for ulike faser av systemutviklingen, f.eks. konsistens mellom spesifiserte krav og funksjonell design, eller konsistens mellom funksjonell design og implementasjonsdesign.

Læringsformer og aktiviteter

Forelesninger, selvstudium, kollokvier og øvinger.

Et gruppearbeid basert på bruk av modellsjekkeverktøyet TLC.

Obligatoriske aktiviteter

• Gruppearbeid

Anbefalte forkunnskaper

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

Forkunnskapskrav

Kjennskap til endelige og utvidete tilstandsmaskiner.

Kursmateriell

1) 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.
2) 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