Formal Methods for Embedded Software

News

| 2007-07-24

===== Exam Results =====

| Matr. No. | Points | Grade | Certificate
| 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 =====

  • Gerlind Herberich

RWTH Aachen University - Chair of Computer Science 11 - Ahornstr. 55 - 52074 Aachen - Germany