===== 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 =====

• Gerlind Herberich

• Dr.rer.nat. Bastian Schlich
• Questions of general interest will be answered in the forum