Hier werden die Unterschiede zwischen zwei Versionen angezeigt.
| Beide Seiten der vorigen Revision Vorhergehende Überarbeitung Nächste Überarbeitung | Vorhergehende Überarbeitung | ||
|
lehre:sose06:formale_methoden [2009/05/05 12:47] brauer |
lehre:sose06:formale_methoden [2011/11/21 17:27] (aktuell) |
||
|---|---|---|---|
| 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 68: | Zeile 68: | ||
| || {{:lehre:sose06:10_20050707_fmes_hybsys.pdf|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 119: | Zeile 119: | ||
| || {{:lehre:sose06:fmes_uebung05.pdf|6. Übung}}, {{:lehre:sose06:beispiel1.zip|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]] | ||