Lecturer: Prof. Dr. Heike Wehrheim
Tutorial: M.Sc. Jürgen König

This lecture will be organized via Koala. All material regarding this lecture can be found there. Please register in PAUL to attend this course. You will be automatically registered in Koala after your PAUL registration.

• The course will be taught in English.
• Audience: Students working towards a Master degree in Computer Science.
• The course belongs to the modules:
  • III.1.1 Model-based software development and III.1.5 Analytical Methods in Software Engineering (Master 2009)
  • III.1.1 Software Engineering 1 and III.1.4 Semantics and Verification (Master 2004).
• Credit points: 4 ECTS.

• The lecture will take place on Tuesday from 09:00-11:00 in O.1.258.
• The tutorial will take place on Tuesday from 11:00-12:00 in O.1.258, right after the lecture.

• An assignment sheet will be uploaded to Koala every week on Tuesday
• Each assignment sheet need be submitted on Koala until Sunday, one week after its upload.
• It will be discussed during the following tutorial.
• Each assignment has to be submitted in groups of 2-4 students.

To pass this course you need to fulfill 3 requirements:

• Present the solution of at least one exercise in the tutorial.
• Reach 30% of the total points of all exercise sheets.
• Pass the oral examination.

The oral examination will take place at the end of the semester. The grade of the examination will be the grade for this lecture.

In the course we will study techniques for formally verifying that a system (software or hardware) is correct, i.e. adheres to requirements describing the desired functionality. For describing requirements a particular class of logics, so called temporal logics, will be employed. Temporal logics can be used to describe properties of systems in time. For this class of logics there are algorithms for checking whether a property does or does not hold for a system. If the system under consideration has a finite state space, tools implementing these algorithms can fully automatically carry out the verification.

In the course we will take a look at two temporal logics (LTL and CTL) and their model checking algorithms. We will furthermore work with model checking tools (in particular SPIN) and verify small examples of systems (for instance distributed algorithms) in the exercises.

[1] E. Clarke, O. Grumberg, D. Peled: Model Checking, MIT Press, 1999.

[2] C. Baier, J.P. Katoen: Principles of Model Checking, MIT Press, 2008.

[3] G.J. Holzmann: The SPIN Model Checker - Primer and Reference Manual, Addison Wesley, 2004.
(see also Spin Webpage)

[4] G.J. Holzmann: The Spin Model Checker, IEEE Trans. on Software Engineering, Vol. 23, No. 5, May 1997, pp. 279-295.

[5] M.B. Dwyer, J. Hatcliff, Robby, C.S. Psreanu, W. Visser: Formal Software Analysis : Emerging Trends in Software Model Checking. Future of Software Engineering Track. Proceedings of the 2007 International Conference on Software Engineering (ICSE 2007), 2007.

[1] will be the basis of a large part of the course, [2] gives a comprehensive introduction to model checking, [3] and [4] describe the SPIN model checker and [5] gives a survey of formal software analyses.