Hier werden die Unterschiede zwischen zwei Versionen angezeigt.
|
lehre:sose06:formale_methoden [2009/06/08 17:48] 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]] | ||