====== Formale Methoden für eingebettete Systeme ======
\\
=== Klausurergebnisse ===
\\
{|
|-
|| Matrikelnummer 	
|| Punkte 	
|| Note 	
|| Schein
|-
|| 212360 	
|| 14 	
|| 5 	
|| Nein 
|-
|| 221786 	
|| 9,5 
|| 5 	
|| Nein 
|-
|| 226568 	
|| 23,5 	
|| 5 	
|| Nein 
|-
|| 234982 	
|| 18,5 	
|| 5 	
|| Nein 
|-
|| 235835 	
|| 41 	
|| 2 	
|| Ja 
|-
|| 244170 	
|| 38 	
|| 2,3 	
|| Ja
|-
|| 250743 	
|| 33,5 	
|| 3 	
|| Ja 
|-
|| 251205 	
|| 38,5 	
|| 2,3 	
|| Ja 
|-
|| 258415 	
|| 40 	
|| 2 	
|| Ja 
|-
|| 267936 	
|| 50,5 	
|| 1 	
|| Ja
|} 
\\
=== Inhalt ===
\\
Anwendung formaler Methoden in der Entwicklung eingebetteter Systeme:\\
\\
  * formale Modelle,
  * hybride Systeme,
  * Verifikation,
  * Model Checking.
\\
Die Vorlesung wird in Deutsch gehalten.\\
\\
=== Literatur ===
\\
  * 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.
\\
=== Folien ===
\\
{|
|-
|| Datum
|| Thema
|| Dokumente
|-
|| 10.04.2007
|| Einführung
|| [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/07sommer/formaleMethoden/1_20070410_Introduction.pdf|pdf]]
|-
|| 17.04.2007
|| Signale und Systeme
|| [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/05sommer/fmes/Formale_Methoden_02.pdf|pdf]]
|-
|| 24.04.2007
|| Temporale Logiken
|| [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/05sommer/fmes/Formale_Methoden_03.pdf|pdf1]], [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/05sommer/fmes/Formale_Methoden_04.pdf|pdf2]]
|-
|| 15.05.2007
|| CTL Model-Checking
|| [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/05sommer/fmes/Formale_Methoden_05_neu.pdf|pdf]]
|-
|| 22.05.2007
|| Symbolic Model-Checking
|| [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/06sommer/fmes_ss06/Formale_Methoden_06.pdf|pdf]]
|-
|| 05.06. & 12.06.2007
|| Timed Automata
|| [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/07sommer/formaleMethoden/TA07.pdf|pdf]]
|-
|| 19.06.2007
|| Hybride Systeme 1
|| [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/07sommer/formaleMethoden/Formale_Methoden_08.pdf|pdf1]], [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/07sommer/formaleMethoden/9_20050630_FMES_HybSys.pdf|pdf2]]
|-
|| 26.06.2007
|| [mc]square
|| [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/07sommer/formaleMethoden/20070626_Vorlesung_FMES.pdf|pdf]]
|-
|| 03.07.2007
|| Hybride Systeme 2
|| [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/07sommer/formaleMethoden/10_20050707_FMES_HybSys.pdf|pdf]]
|}
\\
=== Errata ===
\\
  * Temporale Logiken S. 7 oben, 4. Beispiel: Die Formel cUd ist auch im letzten Knoten wahr.
  * CTL Model-Checking S. 3 a)-f): Die Teilformeln werden für alle Zustände in der Kripke-Struktur überprüft, nicht nur für x0.
\\
=== Mitschrift ===
\\
Mitschrift der Vorlesung erstellt von Herrn Matthias Lebok (Student). Die Mitschrift wird ohne jegliche Gewähr angeboten. Wer Fehler findet, kann diese im Forum melden ([[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/07sommer/formaleMethoden/Formale_Methoden.pdf|pdf]]).
\\
Errata: Am Ende des Semesters wird eine korrigierte Version zur Verfügung gestellt.\\
\\
=== Übung ===
\\
  * Die Übung findet donnerstags 10:00 - 11:30 statt.
  * Voraussichtliche Termine:
    * 19.04.2007
    * 03.05.2007
    * 24.05.2007
    * 14.06.2007 (Raum 2323, Lehrstuhl für Informatik 11)
    * 28.06.2007 (Raum 2323, Lehrstuhl für Informatik 11)
\\
=== Übungsschein ===
\\
Um den Übungsschein zu erwerben\\
\\
  * dürfen Sie maximal einen Übungstermin mit Attest entschuldigt versäumen,
  * müssen Sie mindestens einmal mit Ihrer Gruppe eine Lösung präsentieren
  * und müssen die Klausur bestehen (voraussichtlich 10.07.2007 10:00-11:00).
\\
=== Kontakt ===
\\
  * Gerlind Herberich
  * [[:lehrstuhl:mitarbeiter:schlich|Bastian Schlich]]
  * Allgemeine Fragen werden im [[http://www-i11.informatik.rwth-aachen.de/smf/index.php?board=33.0|Forum]] beantwortet.