1 Ziel der Vorlesung
Das korrekte Funktionieren von Systemen sollte eine Selbstverständlichkeit sein. Jedoch wird der Qualität und Funktionssicherheit von Systemen oft zu wenig Beachtung geschenkt und allzuoft versucht Qualität nur durch Testen zu erzeugen. Die Vorlesung möchte alternative Wege aufzeigen und ein Bewußtsein für Qualität und Funktionssicherheit von Systemen schaffen.
Qualität und Funktionssicherheit können unter anderem erreicht werden durch formale Modellierung, (formale) Verifikation, Prozeßnormen und Entwicklungsnormen. Eine Einführung in diese Themen steht im Mittelpunkt der Vorlesung. Der parallele Besuch der Vorlesung „Verteilte Systeme: Algorithmen“ wird empfohlen.
2 Übung
Eine separate Übung ist nicht vorgesehen. Im Rahmen der Vorlesung werden jedoch zahlreiche Beispiele gemeinsam erarbeitet und ggf. als Übungsaufgaben angeboten.
3 Gliederung
Die Gliederung ist als vorläufig zu betrachten, deswegen ohne Numerierung.
- Nebenläufige, verteilte, kooperierende Systeme
- Grundbegriffe
- Wesentliche Eigenschaften vernetzter Systeme
- Ein einführendes Beispiel: Das „Alternating-Bit“-Protokoll
- Definition „Qualität“
- Definition „Sicherheit“
- Nutzungs- und Realisierungssicht
- Vor- und Nachbedingungen
- Schwächste Vorbedingungen
- Zustandssicht: Systeme als Zustandsmaschinen
- Zustandsübergangssysteme
- Logische Modellierung von Zustandsmaschinen
- Zustandsmaschinen mit Eingabe und Ausgabe
- Objekte als Zustandsmaschinen
- Nebenläufigkeit und Parallelität
- Parallele Progamme mit gemeinsamen Variablen
- Schnittstellensicht: Funktionale Beschreibung von Systemkomponenten
- Syntaktische Schnittstellen: Kanäle und gemeinsame Variablen
- Ströme
- Stromverarbeitende Funktionen
- Objekte als stromverarbeitende Funktionen
- Spezifikation von Strömen
- Spezifikation stromverarbeitender Funktionen
- Systeme mit benannten Kanälen
- Prädikative Spezifikation von Kommunikationsanweisungen
- Von Zustandsmodellen zu stromverarbeitenden Funktionen
- Schnittstellen für Zustandsmaschinen
- Struktur- und Verteilungssicht
- Datenflußnetze
- Kommunikationsnetze
- Kompositionsformen
- Parallele Komposition von zuweisungsorientierten interaktiven Programmen
- Parallele Komposition von Programmen mit gemeinsamen Variablen
- Ablaufsicht: Prozesse als Abläufe verteilter Systeme
- Nebenläufige Prozesse
- Sequentielle Prozesse als Ströme
- Abläufe als Zustandsfolgen und temporale Logik
- Koordination, gegenseitiger Ausschluß
- Zusammenhang zwischen stromverarbeitenden Funktionen und Abläufen
- Abläufe verteilter kommunizierender Systeme
- Temporale Logik
- Qualität als Forderung
- Entwicklungsprozeßmodelle am Beispiel V-Modell XT
- Entwicklungsstandards am Beispiel MISRA
- Reifegradmodelle am Beispiel CMMI
- Sicherheitsnormen am Beispiel IEC 61508
Erhebliche Teile der Vorlesung entstammen der Vorlesung „Modellierung verteilter Systeme“, Prof. Dr. Dr. h.c. Manfred Broy, TU München, SS 2004.
Literatur
[1] Broy, Manfred: Informatik: eine grundlegendeEinführung, Band Teil2. Systemstrukturen und theoretische Informatik. Springer Verlag, Berlin, Heidelberg, 2. Auflage, 1998.
[2] Harel, David: Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3):231–274, June 1987.
[3] Hoare, C. A. R.: Communicating Sequential Processes. Prentice-Hall International, 1986, ISBN 0131532898.
[4] Hopcroft, J. E. and J. D. Ullman: Introduction to automata theory, languages andcomputation. Addison-Wesley, 3nd edition, 1994.
[5] Broy, Manfred: Service-oriented systems engineering: Specification and design ofservices and layered architectures. In Working Material International Summer SchoolMarktoberdorf, 2004.
[6] Hoare, Tony: Process algebra: A unifying approach. In Working MaterialInternational Summer School Marktoberdorf, 2004.
[7] Pnueli, Amir: Keys in formal verification: Abstractions for progress. In WorkingMaterial International Summer School Marktoberdorf, 2004.
[8] Dijkstra, Edsger Wybe: A Discipline of Programming. Prentice Hall PTR, 1997.
[9] Gries, David: The Science of Programming (Monographs in Computer Science). Springer, 1989.
[10] Apt, Krzysztof R. and Ernst Rudiger Olderog: Verification of Sequential andConcurrent Programs. Graduate Texts in Computer Science. Springer, 2nd edition, 1997.
[11] Nissim, Francez: Program Verification (International Computer Science Series). Addison-Wesley, 1992.
[12] Manna, Zohar and Amir Pnueli: Temporal Verification of Reactive Systems :Safety. Springer, 1995.
[13] Manna, Zohar: Mathematical Theory of Computation. McGraw-Hill, 1974.
[14] Denert, Ernst: Software Engineering. Springer-Verlag, 1991.
[15] Comité Européen de Normalisation Electrotechnique (CENELEC), Brüssel: IEC 61508:Funktionale Sicherheit sicherheitsbezogener elektrischer/elektronischer/programmierbarerelektronischer Systeme, 1998.
[16] Capability Maturity Model Integrated web page. http://www.sei.cmu.edu/cmmi
[17] The Motor Industry Software Reliability Association, Nuneaton, Warwickshire: DevelopmentGuidelines For Vehicle Based Software, 2001, ISBN 0 9524156 0 7.
[18] Projekt WEIT: V-Modell XT, Juni 2005. Version 1.01.
Die Literaturliste ist vorläufig und nicht abschließend.
Schreibe einen Kommentar