Formal Methods

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.

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.

Lectures, self study, colloquiums and assignments. A submission of a group assignment based on the model checking tool TLC.