| | 212360
===== Content =====
Application of formal methods in embedded systems development:
formal models,
hybrids systems,
verification,
model checking.
The lecture will be held in German.
===== Literature =====
D. Peled: Software Reliability Methods. Springer, 2001.
E. Clarke, O. Grumberg, D. Peled: Modelchecking. MIT Press, 2001.
B. Berard, M. Bidoit, A. Finkel: Systems and Software Verification. Springer, 2001
W. Ehrenberger: Software-Verifikation. Hanser, 2002.
===== Slides =====
2007-04-10: Introduction ( PDF) 2007-04-17: Signals and Systems ( PDF) 2007-04-24: Temporal Logics ( PDF1 + PDF2) 2007-05-15: CTL Model-Checking ( PDF) 2007-05-22: Symbolic Model-Checking ( PDF) 2007-06-05 & 2007-06-12: Timed Automata ( PDF) 2007-06-19: Hybrid Systems ( PDF1 + PDF2) 2007-06-26: [mc]square
2007-07-03: Hybrid Systems 2 ( PDF)
Errata:
Temporal Logics see 7 above, 4th example: the formula cUd is true in the last node as well.
CTL Model-Checking see 3 a)-f): the partial formulas are checked in the Kripke structure for all states not merely for x0.
===== Lecture Notes =====
Mr. Matthias Lebok (student) has provided his lecture notes as a pdf file which is available for download (no responsibility is taken for the correctness of it). Please report any mistakes you may find in the forum. (pdf)
Errata: We will provide a revised version at the end of the semester.
===== Exercise =====
The exercise will take place Thursdays from 10:00am to 11:30am.
=== Estimated Dates: ===
2007-04-19
2007-05-03
2007-05-24
2007-06-14 (room 2323, Chair of Computer Science 11)
2007-06-28 (room 2323, Chair of Computer Science 11)
=== Übungsschein ===
In order to achieve the Übungsschein
you may be absent for max. one exercise session with attestation,
you must present a solution with your group at least one time
and you must pass the exam (estimatedly on 2007-07-10 10:00am-11:00am).
===== Contact =====
-
Questions of general interest will be answered in the forum
|