Hier werden die Unterschiede zwischen zwei Versionen angezeigt.
lehre:sose06:formale_methoden [2009/05/05 12:42] brauer angelegt |
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 | + | |
- | || Vorlesungsfolien | + | |
- | |- | + | |
- | || 2006-04-13 | + | |
- | || Zeitachsen, Signale, Systeme | + | |
- | || Manuskript (2005) | + | |
- | |- | + | |
- | || 2006-04-20 | + | |
- | || Berechnungsmodelle, Kripke-Strukturen, Temporale Logiken | + | |
- | || Manuskript (2005) | + | |
- | |- | + | |
- | || 2006-04-27 | + | |
- | || CTL/LTL | + | |
- | || Manuskript (2005) | + | |
- | |- | + | |
- | || 2006-05-04 | + | |
- | || CTL-Model-Checking 1 | + | |
- | || Manuskript (2005) | + | |
- | |- | + | |
- | || 2006-05-11 | + | |
- | || CTL-Model-Checking 2 | + | |
- | || 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 | + | |
- | || Folien | + | |
- | |- | + | |
- | || 2006-06-29 | + | |
- | || Hybride Automaten (1) | + | |
- | || Manuskript, Folien (2005) | + | |
- | |- | + | |
- | || 2006-07-06 | + | |
- | || Hybride Automaten (2) | + | |
- | || 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 | + | |
- | || 1. Übung | + | |
- | |- | + | |
- | || 2006-04-26 | + | |
- | || 2006-05-03 | + | |
- | || AH 3 | + | |
- | || 2. Übung, Beispiel | + | |
- | |- | + | |
- | || 2006-05-10 | + | |
- | || 2006-05-17 | + | |
- | || AH 3 | + | |
- | || 3. Übung | + | |
- | |- | + | |
- | || 2006-05-24 | + | |
- | || 2006-05-31 | + | |
- | || 2323 | + | |
- | || 4. Übung, Beispiel | + | |
- | |- | + | |
- | || 2006-06-21 | + | |
- | || 2006-06-28 | + | |
- | || 2323 | + | |
- | || 5. Übung (kein neues Blatt) | + | |
- | |- | + | |
- | || 2006-07-05 | + | |
- | || 2006-07-12 | + | |
- | || 2323 | + | |
- | || 6. Übung, 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]] | + |