course-details-portlet

TM8103 - Formal Methods

About

Examination arrangement

Examination arrangement: Oral examination
Grade: Letters

Evaluation Weighting Duration Grade deviation Examination aids
Oral examination 100/100

Course content

The course is taught every second year, next time spring 2011. Topics are: Focus is on theory for specification, validation and verification of network and network based service functionality specified by communicating state machines, protocol algebraic formulas, and temporal logic descriptions. The theory covers validation by model checking in non-reduced state space, and verification by process algebra, temporal logic, rewriting logic and reasoning on UML constraints.

Learning outcome

To be able to validate the correctness properties of a functional model and also to verify the consistency between models related to the various phases of the functionality life cycle, e.g. the consistency between required properties and functional design, or the consistency between functional design and implementation design.

Learning methods and activities

Lectures, self study, colloquiums and assignments.

A submission of a group assignment based on the model checking tool TLC.

Compulsory assignments

  • Group Work

Required previous knowledge

Knowledge of Finite and Extended State Machines.

Course materials

1) General papers:
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) The model checkers SPIN and 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) Process Algebra:
R. Milner: Communication and Concurrency,
Prentice Hall 1989, ISBN 0-13-115007-3 PBK.

Credit reductions

Course code Reduction From To
DIE5938 7.5
More on the course

No

Facts

Version: 1
Credits:  7.5 SP
Study level: Doctoral degree level

Coursework

Term no.: 1
Teaching semester:  SPRING 2011

Language of instruction: English

-

Subject area(s)
  • Program/system-utvikling
  • Telematics
Contact information
Course coordinator:

Department with academic responsibility
Department of Information Security and Communication Technology

Examination

Examination arrangement: Oral examination

Term Status code Evaluation Weighting Examination aids Date Time Examination system Room *
Autumn ORD Oral examination 100/100
Room Building Number of candidates
Spring ORD Oral examination 100/100 2011-05-27
Room Building Number of candidates
  • * The location (room) for a written examination is published 3 days before examination date. If more than one room is listed, you will find your room at Studentweb.
Examination

For more information regarding registration for examination and examination procedures, see "Innsida - Exams"

More on examinations at NTNU