====== Formale Methoden für eingebettete Systeme ======

=== Inhalt ===

Anwendung formaler Methoden in der Entwicklung eingebetteter Systeme:\\
\\
  * formale Modelle,
  * hybride Systeme,
  * Verifikation,
  * Model Checking.
\\
Die Vorlesung wird in Deutsch gehalten.

=== Vorlesung ===

Die Vorlesung findet donnerstags von 10:00 - 11:30 im AH 1 statt.

=== Dokumente ===

{|
|-
|| **Termin**	
|| **Thema**
|| **Dokumente**
|-
|| 2006-04-06
|| Einführung
|| {{:lehre:sose06:1_20060406_introduction.pdf|Vorlesungsfolien}}
|-
|| 2006-04-13
|| Zeitachsen, Signale, Systeme
|| {{:lehre:sose06:formale_methoden_02.pdf|Manuskript (2005)}}
|-
|| 2006-04-20
|| Berechnungsmodelle, Kripke-Strukturen, Temporale Logiken
|| {{:lehre:sose06:formale_methoden_03.pdf|Manuskript (2005)}}
|-
|| 2006-04-27
|| CTL/LTL
|| {{:lehre:sose06:formale_methoden_04.pdf|Manuskript (2005)}}
|-
|| 2006-05-04
|| CTL-Model-Checking 1
|| {{:lehre:sose06:formale_methoden_05.pdf|Manuskript (2005)}}
|-
|| 2006-05-11
|| CTL-Model-Checking 2
|| {{:lehre:sose06:formale_methoden_06.pdf|Manuskript (2005)}}
|-
|| 2006-05-17
|| SPS-Beispiel
||
|-
|| 2006-06-01
|| Vortrag Applying Model Checking to Real Software for Embedded Systems
|| 
|-
|| 2006-06-22
|| Vortrag Modelchecking von Echtzeitautomaten mit UPPAAL
|| {{:lehre:sose06:formale_methoden_07.pdf|Folien}}
|-
|| 2006-06-29
|| Hybride Automaten (1)
|| {{:lehre:sose06:formale_methoden_08.pdf|Manuskript}}, {{:lehre:sose06:9_20050630_fmes_hybsys.pdf|Folien (2005)}}
|-
|| 2006-07-06
|| Hybride Automaten (2)
|| {{:lehre:sose06:10_20050707_fmes_hybsys.pdf|Folien (2005)}}
|}

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

=== Übung ===

Die Übung findet für jede Gruppe jeweils alle vierzehn Tage mittwochs 15:15 - 16:45 im AH 3 statt. Die voraussichtlichen Termine sind unten aufgeführt. Die Übungen werden zum Teil thematisch aufeinander aufbauen. Aus diesem Grund ist es sinnvoll, an allen Übungsterminen aktiv teilzunehmen.

=== Übungstermine und -blätter ===

{|
|-
|| **A-Termin**
|| **B-Termin**
|| **Ort**
|| **Übung**
|-
|| 2006-04-12
|| 2006-04-19
|| AH 3
|| {{:lehre:sose06:fmes_uebung01.pdf|1. Übung}}
|-
|| 2006-04-26
|| 2006-05-03
|| AH 3
|| {{:lehre:sose06:fmes_uebung02.pdf|2. Übung}}, {{:lehre:sose06:fmes_uebung02_beispiel.pdf|Beispiel}}
|-
|| 2006-05-10
|| 2006-05-17
|| AH 3
|| {{:lehre:sose06:fmes_uebung03.pdf|3. Übung}}
|-
|| 2006-05-24
|| 2006-05-31
|| 2323
|| {{:lehre:sose06:fmes_uebung04.pdf|4. Übung}}, {{:lehre:sose06:fmes_uebung04_beispiel.pdf|Beispiel}}
|-
|| 2006-06-21
|| 2006-06-28
|| 2323
|| 5. Übung (kein neues Blatt)
|-
|| 2006-07-05
|| 2006-07-12
|| 2323	
|| {{:lehre:sose06:fmes_uebung05.pdf|6. Übung}}, {{:lehre:sose06:beispiel1.zip|Beispiel}}
|}

=== Übungsschein ===

Um einen Übungschein zu erlangen, müssen Sie \\
\\
  * an mindestens 5 Übungsterminen anwesend sein,
  * mindestens einmal mit Ihrer Gruppe eine Lösung präsentieren und
  * die Klausur am 2006-07-13 bestehen.

=== Software ===

  * In der Übung wird der Model-Checker SMV verwendet.
    * [[http://www-cad.eecs.berkeley.edu/~kenmcmil/psdoc.html|SMV Dokumentation]]
    * [[http://www-cad.eecs.berkeley.edu/%7Ekenmcmil/smv/|Download von Cadence SMV]]
  * In der letzten Übung werden wir mit [[http://www.uppaal.com/|UPPAAL]] arbeiten.

=== Termine ===

{|
|-
|| **Termin**
|| **Thema**
|| **Ort**
|-
|| 2006-04-06
|| 1. Vorlesung
|| AH 1
|-
|| 2006-04-12
|| 1. Übung, Gruppe A
|| AH 3
|-
|| 2006-04-19
|| 1. Übung, Gruppe B
|| AH 3
|-
|| 2006-07-13
|| Klausur
||
|}

=== Kontakt ===

  * [[:lehrstuhl:mitarbeiter:palczynski|Jacob Palczynski]]