course-details-portlet

TM8103 - Formelle metoder

Om emnet

Undervises ikke studieåret 2024/2025

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.

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

Emnekode Reduksjon Fra Til
DIE5938 7.5
Flere sider om emnet

Ingen

Fakta om emnet

Versjon: 1
Studiepoeng:  7.5 SP
Studienivå: Doktorgrads nivå

Undervisning

Ingen

Undervisningsspråk: Engelsk

Sted: Trondheim

Fagområde(r)
  • Program/system-utvikling
  • Telematikk

Eksamensinfo

  • * Skriftlig eksamen plasseres på rom 3 dager før eksamensdato. Hvis mer enn ett rom er oppgitt, finner du ditt rom på Studentweb.
Eksamensinfo

For mer info om oppmelding til og gjennomføring av eksamen, se "Innsida - Eksamen"

Mer om eksamen ved NTNU