Unterschiede

Hier werden die Unterschiede zwischen zwei Versionen angezeigt.

Link zu dieser Vergleichsansicht

lehre:sose06:formale_methoden [2009/05/05 12:47]
brauer 		lehre:sose06:formale_methoden [2011/11/21 17:27]
Zeile 1: Zeile 1:
-====== 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]] ​+