Formal Methods

SaToSS home

• Theoretical Computer Science 1
• Distributed Systems
• Formal Methods
• Game Theory
• Information Security Basics
• Introduction to IT Security
• Network Security
• Security Protocols
• Security Modeling

Moodle

Please consult the FSTC moodle pages for dynamic information concerning this course.

Instructors

• Alloy: Prof. Dr. Pierre Kelsen
• Process Algebras: Prof. Dr. Sjouke Mauw
• Protocol Verification: Dr. Jun Pang

Content

Information on the course Formal Methods is kept here. In this course, we will study a collection of techniques that are essential in the construction of large and highly relibale systems. The course will focus on the principles and applications of the following formal methods:

• Alloy - a declarative modeling language based on first-order logic, for expressing complex structural constraints and behavior. The Alloy Analyzer is a constraint solver that provides fully automatic simulation and checking. The motivation for the Alloy project was to bring to Z-style specifications (Z being another formal language) the kind of automation offered by model checkers.
• Process Algebras - Process Algebra is a formal description technique for complex computer systems, especially those involving communicating, concurrently executing components. It is a subject that touches many topic areas of computer science and discrete math.
• Protocol Verification - a specification language based on process algebra extended with abstract data types is used to describe communicating systems. Interesting properties about the systems are expressed as temporal logic formulas. Model checking is employed as a method to formally verify whether the model defined by the system satisfies the properties.

We have chosen these methods because they are based on complementary approaches for formal reasoning about systems. The course is tool-oriented in the sense that automatic tool support will be an essential part of the teaching units whenever possible. In this sense the lecture provides a more hands-on approach to theoretical concepts compared to courses in the first semester. Many examples and real-life case studies drawn from a variety of domains such as computer security, communicative systems and software engineering will be presented.

Objectives

The student should gain experience in the formal methods presented in this course. More generally the student will be encouraged to think deeply about systems they will develop and to apply automated tools based on mathematical theories to their analysis and design.

Reading material

• Wan Fokkink, Modelling Distributed Systems, Texts in Theoretical Computer Science, An EATCS Series, Springer-Verlag, 2007
• Luca Aceto, Anna Ingolfsdottir, Kim Guldstrand Larsen, Jiri Srba, Reactive Systems: Modelling, Specification and Verification, Cambridge University Press, 2007
• Manual and more information on the µCRL toolset
• Manual page on the regular alternation-free µ-calculus

Evaluation

The final grade will be computed as follows: assignments will be weighted 30% (10% for each topic) and the final exam will be weighted 70%. Details about the assignment policy should be announced by each lecturer.