====== Formal Methods for Embedded Software ======
~~NOTOC~~
===== News =====

{|
|-
|| 2007-07-24 	
|| The exam results are online. You can pick up your certificates at our secretariat in about 14 days. Exam inspection will be on 2007-08-06 in room 2320 from 2:00pm - 3:00pm.
|-
|| 2007-05-31 	
|| The upcoming exercise sessions will take place in room 2323 at our chair.
|- 
|| 2007-05-11 	
|| We have added a list with corrections considering the slides.
|- 
|| 2007-05-09 	
|| The next exercise session will take place on 2007-05-24 in room 2323 at our chair. We will discuss the final tasks of the last exercise (bring along your exercise sheet!) and will give an introduction to Uppaal.
|- 
|| 2007-05-03 	
|| There is a thread in the forum concerning task 1 of the second sheet (fairness in LTL/CTL). Additionally, the notes of the last two lectures are online. Please report errors in the forum.
|-
|| 2007-04-23 	
|| Lecture notes of a student are online.
|-
|| 2007-04-10 	
|| The exercise sessions will start from 2007-04-19 on every two weeks and take 90 minutes.
|- 
|| 2007-03-12 	
|| The lecture and exercise session will not take place in the week of 2007-04-02. They will start a week later.
|}

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

{|
|-
|| **Matr. No.**
|| **Points**
|| **Grade**
|| **Certificate**
|-
|| 212360 	
|| 14 	
|| 5 	
|| No
|-
|| 221786 	
|| 9,5 	
|| 5 	
|| No
|-
|| 226568 	
|| 23,5 	
|| 5 	
|| No
|-
|| 234982 	
|| 18,5 	
|| 5 	
|| No
|- 
|| 235835 	
|| 41 	
|| 2 	
|| Yes
|-
|| 244170 	
|| 38 	
|| 2,3 	
|| Yes
|-
|| 250743 	
|| 33,5 	
|| 3 	
|| Yes
|-
|| 251205 	
|| 38,5 	
|| 2,3 
|| Yes
|-
|| 258415 	
|| 40 	
|| 2 	
|| Yes
|-
|| 267936 	
|| 50,5 
|| 1 	
|| Yes
|}

===== 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 ({{:lehre:sose07:fm_intro.pdf|PDF}})
  * 2007-04-17: Signals and Systems ({{:lehre:sose07:fm_signals.pdf|PDF}})
  * 2007-04-24: Temporal Logics ({{:lehre:sose07:fm_temporal1.pdf|PDF1}} + {{:lehre:sose07:fm_temporal2.pdf|PDF2}})
  * 2007-05-15: CTL Model-Checking ({{:lehre:sose07:fm_ctl.pdf|PDF}})
  * 2007-05-22: Symbolic Model-Checking ({{:lehre:sose07:fm_symbolic.pdf|PDF}})
  * 2007-06-05 & 2007-06-12: Timed Automata ({{:lehre:sose07:fm_timed.pdf|PDF}})
  * 2007-06-19: Hybrid Systems ({{:lehre:sose07:fm_hyb.pdf|PDF1}} + {{:lehre:sose07:fm_hybsys.pdf|PDF2}})
  * 2007-06-26: [mc]square
  * 2007-07-03: Hybrid Systems 2 ({{:lehre:sose07:fm_hybsys2.pdf|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. ({{:lehre:sose07:fm.pdf|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

  * [[:en:lehrstuhl:mitarbeiter:schlich]]
  * Questions of general interest will be answered in the [[http://www-i11.informatik.rwth-aachen.de/smf/index.php?board=33.0|forum]]

~~NOTOC~~