Hier werden die Unterschiede zwischen zwei Versionen angezeigt.
|
lehre:sose07:formale_methoden [2009/05/04 14:18] brauer |
lehre:sose07:formale_methoden [2011/11/21 17:27] |
||
|---|---|---|---|
| Zeile 1: | Zeile 1: | ||
| - | ====== Formale Methoden für eingebettete Systeme ====== | + | |
| - | \\ | + | |
| - | === Klausurergebnisse === | + | |
| - | \\ | + | |
| - | {| | + | |
| - | |- | + | |
| - | || Matrikelnummer | + | |
| - | || Punkte | + | |
| - | || Note | + | |
| - | || Schein | + | |
| - | |- | + | |
| - | || 212360 | + | |
| - | || 14 | + | |
| - | || 5 | + | |
| - | || Nein | + | |
| - | |- | + | |
| - | || 221786 | + | |
| - | || 9,5 | + | |
| - | || 5 | + | |
| - | || Nein | + | |
| - | |- | + | |
| - | || 226568 | + | |
| - | || 23,5 | + | |
| - | || 5 | + | |
| - | || Nein | + | |
| - | |- | + | |
| - | || 234982 | + | |
| - | || 18,5 | + | |
| - | || 5 | + | |
| - | || Nein | + | |
| - | |- | + | |
| - | || 235835 | + | |
| - | || 41 | + | |
| - | || 2 | + | |
| - | || Ja | + | |
| - | |- | + | |
| - | || 244170 | + | |
| - | || 38 | + | |
| - | || 2,3 | + | |
| - | || Ja | + | |
| - | |- | + | |
| - | || 250743 | + | |
| - | || 33,5 | + | |
| - | || 3 | + | |
| - | || Ja | + | |
| - | |- | + | |
| - | || 251205 | + | |
| - | || 38,5 | + | |
| - | || 2,3 | + | |
| - | || Ja | + | |
| - | |- | + | |
| - | || 258415 | + | |
| - | || 40 | + | |
| - | || 2 | + | |
| - | || Ja | + | |
| - | |- | + | |
| - | || 267936 | + | |
| - | || 50,5 | + | |
| - | || 1 | + | |
| - | || Ja | + | |
| - | |} | + | |
| - | \\ | + | |
| - | === Inhalt === | + | |
| - | \\ | + | |
| - | Anwendung formaler Methoden in der Entwicklung eingebetteter Systeme:\\ | + | |
| - | \\ | + | |
| - | * formale Modelle, | + | |
| - | * hybride Systeme, | + | |
| - | * Verifikation, | + | |
| - | * Model Checking. | + | |
| - | \\ | + | |
| - | Die Vorlesung wird in Deutsch gehalten.\\ | + | |
| - | \\ | + | |
| - | === 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. | + | |
| - | \\ | + | |
| - | === Folien === | + | |
| - | \\ | + | |
| - | {| | + | |
| - | |- | + | |
| - | || Datum | + | |
| - | || Thema | + | |
| - | || Dokumente | + | |
| - | |- | + | |
| - | || 10.04.2007 | + | |
| - | || Einführung | + | |
| - | || [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/07sommer/formaleMethoden/1_20070410_Introduction.pdf|pdf]] | + | |
| - | |- | + | |
| - | || 17.04.2007 | + | |
| - | || Signale und Systeme | + | |
| - | || [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/05sommer/fmes/Formale_Methoden_02.pdf|pdf]] | + | |
| - | |- | + | |
| - | || 24.04.2007 | + | |
| - | || Temporale Logiken | + | |
| - | || [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/05sommer/fmes/Formale_Methoden_03.pdf|pdf1]], [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/05sommer/fmes/Formale_Methoden_04.pdf|pdf2]] | + | |
| - | |- | + | |
| - | || 15.05.2007 | + | |
| - | || CTL Model-Checking | + | |
| - | || [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/05sommer/fmes/Formale_Methoden_05_neu.pdf|pdf]] | + | |
| - | |- | + | |
| - | || 22.05.2007 | + | |
| - | || Symbolic Model-Checking | + | |
| - | || [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/06sommer/fmes_ss06/Formale_Methoden_06.pdf|pdf]] | + | |
| - | |- | + | |
| - | || 05.06. & 12.06.2007 | + | |
| - | || Timed Automata | + | |
| - | || [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/07sommer/formaleMethoden/TA07.pdf|pdf]] | + | |
| - | |- | + | |
| - | || 19.06.2007 | + | |
| - | || Hybride Systeme 1 | + | |
| - | || [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/07sommer/formaleMethoden/Formale_Methoden_08.pdf|pdf1]], [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/07sommer/formaleMethoden/9_20050630_FMES_HybSys.pdf|pdf2]] | + | |
| - | |- | + | |
| - | || 26.06.2007 | + | |
| - | || [mc]square | + | |
| - | || [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/07sommer/formaleMethoden/20070626_Vorlesung_FMES.pdf|pdf]] | + | |
| - | |- | + | |
| - | || 03.07.2007 | + | |
| - | || Hybride Systeme 2 | + | |
| - | || [[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/07sommer/formaleMethoden/10_20050707_FMES_HybSys.pdf|pdf]] | + | |
| - | |} | + | |
| - | \\ | + | |
| - | === Errata === | + | |
| - | \\ | + | |
| - | * Temporale Logiken S. 7 oben, 4. Beispiel: Die Formel cUd ist auch im letzten Knoten wahr. | + | |
| - | * CTL Model-Checking S. 3 a)-f): Die Teilformeln werden für alle Zustände in der Kripke-Struktur überprüft, nicht nur für x0. | + | |
| - | \\ | + | |
| - | === Mitschrift === | + | |
| - | \\ | + | |
| - | Mitschrift der Vorlesung erstellt von Herrn Matthias Lebok (Student). Die Mitschrift wird ohne jegliche Gewähr angeboten. Wer Fehler findet, kann diese im Forum melden ([[http://www.embedded.rwth-aachen.de/fileadmin/user_upload/Redakteure/Vorlesungen/07sommer/formaleMethoden/Formale_Methoden.pdf|pdf]]). | + | |
| - | \\ | + | |
| - | Errata: Am Ende des Semesters wird eine korrigierte Version zur Verfügung gestellt.\\ | + | |
| - | \\ | + | |
| - | === Übung === | + | |
| - | \\ | + | |
| - | * Die Übung findet donnerstags 10:00 - 11:30 statt. | + | |
| - | * Voraussichtliche Termine: | + | |
| - | * 19.04.2007 | + | |
| - | * 03.05.2007 | + | |
| - | * 24.05.2007 | + | |
| - | * 14.06.2007 (Raum 2323, Lehrstuhl für Informatik 11) | + | |
| - | * 28.06.2007 (Raum 2323, Lehrstuhl für Informatik 11) | + | |
| - | \\ | + | |
| - | === Übungsschein === | + | |
| - | \\ | + | |
| - | Um den Übungsschein zu erwerben\\ | + | |
| - | \\ | + | |
| - | * dürfen Sie maximal einen Übungstermin mit Attest entschuldigt versäumen, | + | |
| - | * müssen Sie mindestens einmal mit Ihrer Gruppe eine Lösung präsentieren | + | |
| - | * und müssen die Klausur bestehen (voraussichtlich 10.07.2007 10:00-11:00). | + | |
| - | \\ | + | |
| - | === Kontakt === | + | |
| - | \\ | + | |
| - | * Gerlind Herberich | + | |
| - | * [[:lehrstuhl:mitarbeiter:schlich|Bastian Schlich]] | + | |
| - | * Allgemeine Fragen werden im [[http://www-i11.informatik.rwth-aachen.de/smf/index.php?board=33.0|Forum]] beantwortet. | + | |