Cyber-Physical Systems I - Discrete Models
Model checking is a technique for the automatic verification of hardware or software systems. Given such a system and a specification of its intended behaviour, a model checker finds out whether the system satisfies the specification. Model checking has made enormous progress since its invention in the 1980s; today it is possible to verify entire CPU designs, and so all major microprocessor companies use and develop tools for this purpose. Software verification is more challenging than hardware verification and an active research topic (pursued at the chair for Software Engineering, for instance!). Recent years have seen interesting progress in this area as well. The industry has already started using these techniques to check, e.g., safety-critical embedded systems, and software libraries; yet, many research challenges, both theoretical and practical, lie ahead of us.
| Course type | Lecture |
|---|---|
| Instructors | Prof. Dr. Andreas Podelski, Sergio Feo-Arenis, Alexander Nutz |
| Lecture | Tuesday 16:00 - 18:00 Bldg. 101 SR 01-016 Thursday 16:00 - 17:00 Bldg. 101 SR 01-016 |
| Exercise | Schedule will be adapted during the semester. |
| First session | October 23rd, 2012 |
| Language of instruction | English |
| Credits | 6 |
| Exams | Oral exam |
| Course catalog | click here |
Description
The course provides an introduction to the topic, covering how to model systems, how to express properties about them in temporal logic, and algorithms for checking whether they hold. We will introduce some well-known model-checking tools.
The lecture will cover the following topics:
- Transition Systems
- Linear Time Properties
- Regular Properties
- Temporal Logics
- ... (Under Construction)
News
- (2012-12-20) Exercise sheet 6 is online now.
- (2012-11-27) The submission deadline for exercise sheet 4 has been moved by two days to December 6th (the old date in the pdf is obsolete)
- (2012-11-22) A new version of exercise sheet 3 is online, now with an alternative exercise.
- (2012-11-13) The slides for the new chapter "Linear-Time Properties" are online.
- (2012-11-08) The handout version of the slides from October 23rd is online.
- (2012-11-08) The second exercise sheet is up, it will be discussed on Thursday, November 15th
- (2012-11-07) The first (short) exercise session wil take place tomorrow, Thursday, November 8th.
- (2012-10-31) The first exercise sheet is up, the date of the discussion will be announced shortly.
- The first session will take place during the week between the 22nd and the 26th of October.
Exercises
At the beginning of each week, we will hand out an exercise sheet with exercises on material that you will acquire in that week. I.e., the lectures of each week will cover the material that you need in order to be able to solve the exercise sheet that you received at the beginning of the week. In each new week, we start with the exercise group to discuss the exercises which you have worked on during the preceding week.
Exercise Submission Scheme
- You will have one week to hand in the solutions of the exercises, i.e., the time from Tuesday of one week until the Tuesday of the following week. There will be a designated lockbox which we will empty at a set time. You can also hand in the solutions at the beginning of the Tuesday lecture, or you can bring them to one of the instructors or the secretaries.
- We would like that you hand in a signed sheet with the solutions of every exercise sheet. You can hand in whatever you have been able to do, possibly nothing if you were sick. In case you have been sick, you just mark this on your signed solution sheet. This helps us to know that you are still on the ball.
- We will alternate three lectures (of two hours) with one exercise group (of two hours). We will schedule the alternation on demand. In the exercise group, we will discuss the exercises which you have worked on during the preceding weeks and/or those for which you have just handed in the solutions.
Final examination (oral exam)
There will be no formal admission criteria for the final exam. We will correct your solutions but we will not grade them. There will be no 50% rule or such. We would like that you hand in a signed sheet with the solutions of every exercise sheet. As said above, you can hand in whatever you have been able to do, possibly nothing if you were sick. In case you have been sick, you just mark this on your signed solution sheet. This helps us to know that you are still on the ball.Resources
Slides
- Tuesday, October 23rd. [PDF] [PDF Handout]
- Tuesday, November 13th. Linear-Time Properties. [PDF] [PDF-Handout]
- Tuesday, November 27th. Regular Properties. [PDF] [PDF-Handout]
- Tuesday, January 8th, 2013. Linear Temporal Logic. [PDF]
Exercise sheets
- Exercise Sheet 1 (Transition Systems) [PDF]
- Exercise Sheet 2 (Synchronized Systems) [PDF]
- Exercise Sheet 3 (Trace Inclusion, Safety Properties & Invariants) [PDF]
- Exercise Sheet 4 (Invariants) [PDF] (submission till December 6th, not 4th as written in the pdf)
- Exercise Sheet 5 (Infinite words) [PDF]
- Exercise Sheet 6 (Büchi Automata) [PDF]
- Exercise Sheet 7 (LT Properties) [PDF]
- Exercise Sheet 8 (Regular Properties) [PDF]
- Exercise Sheet 9 (LTL) [PDF]
- Exercise Sheet 10 (LTL - Part 2) [PDF]
Literature
The lecture will follow very closely the famous textbook "Principles of Model Checking" by Christel Baier and Joost-Pieter Katoen (MIT Press). It is worth buying the book but a copy will be available in the library.