Unterschiede

Hier werden die Unterschiede zwischen zwei Versionen angezeigt.

Link zu dieser Vergleichsansicht

Nächste Überarbeitung 		Vorhergehende Überarbeitung
lehre:sose06:formale_methoden [2009/05/05 12:42]
brauer angelegt 		lehre:sose06:formale_methoden [2009/06/08 17:48]
brauer
Zeile 1: Zeile 1:
 ====== Formale Methoden für eingebettete Systeme ====== ====== Formale Methoden für eingebettete Systeme ======
-\\+
 === Inhalt === === Inhalt ===
-\\+
 Anwendung formaler Methoden in der Entwicklung eingebetteter Systeme:\\ Anwendung formaler Methoden in der Entwicklung eingebetteter Systeme:\\
 \\ \\
Zeile 10: Zeile 10:
   * Model Checking.   * Model Checking.
 \\ \\
-Die Vorlesung wird in Deutsch gehalten.\\ +Die Vorlesung wird in Deutsch gehalten. 
-\\+
 === Vorlesung === === Vorlesung ===
-\\ + 
-Die Vorlesung findet donnerstags von 10:00 - 11:30 im AH 1 statt.\\ +Die Vorlesung findet donnerstags von 10:00 - 11:30 im AH 1 statt. 
-\\+
 === Dokumente === === Dokumente ===
-\\+
 {| {|
 |- |-
Zeile 26: Zeile 26:
 || 2006-04-06 || 2006-04-06
 || Einführung || Einführung
-|| Vorlesungsfolien+|| {{:​lehre:​sose06:​1_20060406_introduction.pdf|Vorlesungsfolien}}
 |- |-
 || 2006-04-13 || 2006-04-13
 || Zeitachsen, Signale, Systeme || Zeitachsen, Signale, Systeme
-|| Manuskript (2005)+|| {{:​lehre:​sose06:​formale_methoden_02.pdf|Manuskript (2005)}}
 |- |-
 || 2006-04-20 || 2006-04-20
 || Berechnungsmodelle,​ Kripke-Strukturen,​ Temporale Logiken || Berechnungsmodelle,​ Kripke-Strukturen,​ Temporale Logiken
-|| Manuskript (2005)+|| {{:​lehre:​sose06:​formale_methoden_03.pdf|Manuskript (2005)}}
 |- |-
 || 2006-04-27 || 2006-04-27
 || CTL/LTL || CTL/LTL
-|| Manuskript (2005)+|| {{:​lehre:​sose06:​formale_methoden_04.pdf|Manuskript (2005)}}
 |- |-
 || 2006-05-04 || 2006-05-04
 || CTL-Model-Checking 1 || CTL-Model-Checking 1
-|| Manuskript (2005)+|| {{:​lehre:​sose06:​formale_methoden_05.pdf|Manuskript (2005)}}
 |- |-
 || 2006-05-11 || 2006-05-11
 || CTL-Model-Checking 2 || CTL-Model-Checking 2
-|| Manuskript (2005)+|| {{:​lehre:​sose06:​formale_methoden_06.pdf|Manuskript (2005)}}
 |- |-
 || 2006-05-17 || 2006-05-17
Zeile 58: Zeile 58:
 || 2006-06-22 || 2006-06-22
 || Vortrag Modelchecking von Echtzeitautomaten mit UPPAAL || Vortrag Modelchecking von Echtzeitautomaten mit UPPAAL
-|| Folien+|| {{:​lehre:​sose06:​formale_methoden_07.pdf|Folien}}
 |- |-
 || 2006-06-29 || 2006-06-29
 || Hybride Automaten (1) || Hybride Automaten (1)
-|| Manuskript, Folien (2005)+|| {{:​lehre:​sose06:​formale_methoden_08.pdf|Manuskript}}, {{:​lehre:​sose06:​9_20050630_fmes_hybsys.pdf|Folien (2005)}}
 |- |-
 || 2006-07-06 || 2006-07-06
 || Hybride Automaten (2) || Hybride Automaten (2)
-|| Folien (2005)+|| {{:​lehre:​sose06:​10_20050707_fmes_hybsys.pdf|Folien (2005)}}
 |} |}
-\\+
 === Literatur === === Literatur ===
-\\+
   * D. Peled: Software Reliability Methods. Springer, 2001.   * D. Peled: Software Reliability Methods. Springer, 2001.
   * E. Clarke, O. Grumberg, D. Peled: Modelchecking. MIT Press, 2001.   * E. Clarke, O. Grumberg, D. Peled: Modelchecking. MIT Press, 2001.
   * B. Berard, M. Bidoit, A. Finkel: Systems and Software Verification. Springer, 2001   * B. Berard, M. Bidoit, A. Finkel: Systems and Software Verification. Springer, 2001
   * W. Ehrenberger:​ Software-Verifikation. Hanser, 2002.   * W. Ehrenberger:​ Software-Verifikation. Hanser, 2002.
-\\+
 === Übung === === Ü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. ​\\ +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 === === Übungstermine und -blätter ===
-\\+
 {| {|
 |- |-
Zeile 92: Zeile 92:
 || 2006-04-19 || 2006-04-19
 || AH 3 || AH 3
-|| 1. Übung+|| {{:​lehre:​sose06:​fmes_uebung01.pdf|1. Übung}}
 |- |-
 || 2006-04-26 || 2006-04-26
 || 2006-05-03 || 2006-05-03
 || AH 3 || AH 3
-|| 2. Übung, Beispiel+|| {{:​lehre:​sose06:​fmes_uebung02.pdf|2. Übung}}, {{:​lehre:​sose06:​fmes_uebung02_beispiel.pdf|Beispiel}}
 |- |-
 || 2006-05-10 || 2006-05-10
 || 2006-05-17 || 2006-05-17
 || AH 3 || AH 3
-|| 3. Übung+|| {{:​lehre:​sose06:​fmes_uebung03.pdf|3. Übung}}
 |- |-
 || 2006-05-24 || 2006-05-24
 || 2006-05-31 || 2006-05-31
 || 2323 || 2323
-|| 4. Übung, Beispiel+|| {{:​lehre:​sose06:​fmes_uebung04.pdf|4. Übung}}, {{:​lehre:​sose06:​fmes_uebung04_beispiel.pdf|Beispiel}}
 |- |-
 || 2006-06-21 || 2006-06-21
Zeile 117: Zeile 117:
 || 2006-07-12 || 2006-07-12
 || 2323  || 2323
-|| 6. Übung, Beispiel+|| {{:​lehre:​sose06:​fmes_uebung05.pdf|6. Übung}}, {{:​lehre:​sose06:​beispiel1.zip|Beispiel}}
 |} |}
-\\+
 === Übungsschein === === Übungsschein ===
-\\+
 Um einen Übungschein zu erlangen, müssen Sie \\ Um einen Übungschein zu erlangen, müssen Sie \\
 \\ \\
Zeile 127: Zeile 127:
   * mindestens einmal mit Ihrer Gruppe eine Lösung präsentieren und   * mindestens einmal mit Ihrer Gruppe eine Lösung präsentieren und
   * die Klausur am 2006-07-13 bestehen.   * die Klausur am 2006-07-13 bestehen.
-\\+
 === Software === === Software ===
-\\+
   * In der Übung wird der Model-Checker SMV verwendet.   * 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/​~kenmcmil/​psdoc.html|SMV Dokumentation]]
     * [[http://​www-cad.eecs.berkeley.edu/​%7Ekenmcmil/​smv/​|Download von Cadence SMV]]     * [[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.   * In der letzten Übung werden wir mit [[http://​www.uppaal.com/​|UPPAAL]] arbeiten.
-\\+
 === Termine === === Termine ===
-\\+
 {| {|
 |- |-
Zeile 159: Zeile 159:
 || ||
 |} |}
-\\+
 === Kontakt === === Kontakt ===
-\\+
   * [[:​lehrstuhl:​mitarbeiter:​palczynski|Jacob Palczynski]] ​   * [[:​lehrstuhl:​mitarbeiter:​palczynski|Jacob Palczynski]] ​