TM8103 - Formal Methods

About

Examination arrangement

Examination arrangement: Oral examination
Grade: Passed/Failed

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

Course content

The course is taught every second year, next time spring 2019.

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 verification by process algebra, temporal logic, rewriting logic and reasoning on UML constraints. With respect to verification tools, model checkers, theorem provers, SAT and SMT solvers will be discussed.

Learning outcome

A. Knowledge: 1) A good understanding of the opportunities, methods and challenges in formal-based modeling, verification and development of functional properties in information and communication technology (ICT) systems. 2) In depth knowledge of the different techniques to specify ICT systems in a modular way and to verify that the models keep certain system properties. 3) Basic knowledge of verification tools like theorem proving and model checking. B. Skills: 1) Manage the terminology and theoretical concepts in the area of formal specification and verification. 2) Be able to specify models of ICT systems based on automata, temporal logic and protocol algebras. 3) Master verification proofs of invariant system properties. 4) Master simple refinement proofs that a more detailed system specification implements a more coarse-grained one. C. General competence: 1) Improved insight into the advantages of a formal-based system design in comparison to non formal programming.

Learning methods and activities

Lectures, self study, colloquiums and assignments.

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

The grading rule is pass/fail. The minimum passing grade is 70/100 points (70%).

Compulsory assignments

  • Group Work

Further on evaluation

If the course is failed, only the oral exam has to be repeated.

Specific conditions

Exam registration requires that class registration is approved in the same semester. Compulsory activities from previous semester may be approved by the department.

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

Timetable

Detailed timetable

Examination

Examination arrangement: Oral examination

Term Statuskode Evaluation form Weighting Examination aids Date Time Room *
Autumn ORD Oral examination 100/100
Spring ORD Oral examination 100/100
  • * 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.