course-details-portlet

TM8103 - Formelle metoder

Om emnet

Vurderingsordning

Vurderingsordning: Muntlig eksamen
Karakter: Bokstavkarakterer

Vurdering Vekting Varighet Delkarakter Hjelpemidler
Muntlig 100/100

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

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

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

Termin nr.: 1
Undervises:  VÅR 2011

Undervisningsspråk: Engelsk

-

Fagområde(r)
  • Program/system-utvikling
  • Telematikk
Kontaktinformasjon
Emneansvarlig/koordinator:

Ansvarlig enhet
Institutt for informasjonssikkerhet og kommunikasjonsteknologi

Eksamensinfo

Vurderingsordning: Muntlig eksamen

Termin Statuskode Vurdering Vekting Hjelpemidler Dato Tid Eksamens- system Rom *
Høst ORD Muntlig 100/100
Rom Bygning Antall kandidater
Vår ORD Muntlig 100/100 27.05.2011
Rom Bygning Antall kandidater
  • * 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