Über das Buch

Zum Inhalt

Der Entwurf und die Verifikation verteilter Systeme stellen den Entwicklungsingenieur immer noch vor große Probleme. Das komplexe parallele Verhalten solcher Systeme entzieht sich wegen der Nicht-Determiniertheit der zeitliche Abläufe der menschlichen Vorstellungskraft. Der korrekte Entwurf bzw. die Verifikation des Entwurfes lassen sich deshalb nur auf der Grundlage formaler, mathematischer Methoden lösen.

Grundlage jeder formalen Entwurfsmethode ist zunächst eine Modellbildung für das Verhalten verteilter Systeme. Als Grundlage der Untersuchung dienen daher ereignisbasierte Modelle parallelen Verhaltens.

Ereignisbasierte Modelle sind eine neuere und inzwischen gut untersuchte Theorie zur Modellierung des parallelen Verhaltens verteilter Systeme.

Die bestehende Theorie ereignisbasierter Modelle wird in dieser Arbeit ergänzt um die Begriffe der Spezifikation und der Implementierung. Diese Begriffe erhalten dabei eine exakte mathematische Festlegung.

Untersucht wird dann, welche Eigenschaften einer Spezifikation beweisbar auch in der Implementierung gelten. Die gefundenen Aussagen bilden die Grundlage für einen mathematisch korrekten Entwurf oder eine a posteriori Verifikation von verteilten Systemen.

Es ist ein Anliegen des Buches eine Brücke zwischen Theorie und Praxis zu schlagen. Die Anwendung der Resultate wird an Entwurfsbeispielen aus der Praxis, z.B. Teilen des ISDN-Protokolls, aufgezeigt.

Viele ausführliche Erläuterungen und eine gründliche Motivation der theoretische Konzepte anhand von kleinen Fallbeispielen und mit Hilfe von anschaulichen Graphiken machen den Text leicht lesbar und vereinfachen das Verständnis der zugrunde liegenden Theorie.

Alle wichtigen mathematischen Grundlagen sind aus der Spezialliteratur zusammengetragen und in einfacher und einheitlicher Form präsentiert. Das Buch ist dadurch inhaltlich in sich vollständig und eignet sich wegen der didaktisch gelungenen Präsentation der…

Schlagworte

Flussereignisstruktur, Konfigurationsstruktur, Sprache, Abstraktionsoperator, Korrektheitskriterium, Implementierung, Verifikation, Informatik