Course content

The course is taught every second year, next time spring 2026. 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.

Compulsory assignments

• Group Work

Further on evaluation

The grading rule is passed/failed. The minimum passing grade is 70/100 points (70%).

If a student wants to retake the course, approved compulsory activities do not have to be repeated.

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

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.

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