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
This website uses cookies. By using the website, you agree with storing cookies on your computer. If you do not agree please leave the website.More information about cookies

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