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

Recommended previous knowledge

Experience with state based languages such as SDL, UML and LOTOS.

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