Verifikation verteilter Systeme birgt viele Herausforderungen, insbesondere wenn das verteilte System mehrere Möglichkeiten der Interaktion zwischen Entitäten ermöglicht. Die Komplexität dieser Aufgabe spiegelt sich in der Komplexität des Verifikationssystems wider; der Entwurf solcher Verifikationssysteme ist selbst ein nicht minder herausforderndes Problem aus theoretischer Sicht. Das Hauptwerkzeug des Ingenieurwesens zum Entwurf komplexer Systeme ist Modularisierung. Modularität im Zielsystem wird von Verifikationssystemen zwar ausgenutzt, die Theorie der Verifikation ist aber selten selbst modular. Diese Dissertation ist eine Studie über Modularität in deduktiver Verifikation mit Programmlogiken. Der Hauptbeitrag zu diesem Zwecke ist die Behavioral Program Logic (BPL). Als Nebenläufigkeitsmodell verwenden wir Active Objects, die auf der einen Seite mehrere Möglichkeiten der Interaktion zwischen Entitäten zulässt und auf der anderen Seite durch ihre strikte Kapselung bereits auf Semantikebene Modularität ermöglichen. Modularität wird auf mehreren Ebenen benutzt:

• Wir entwerfen eine modulare, neue Locally Abstract, Globally Concrete Semantik für Active Ob- jects, welche lokales Verhalten von globalem Verhalten abkapselt.

• Wir entwerfen ein modulares Spezifikationsprinzip mit Objektinvarianten, asynchronen Methodverträgen, Effect Types und Session Types. Jede dieser Spezifikationen ist selbst modular und beschreibt das Verhalten einer abgekapselten Entität. Beispielsweise beschreiben Objektinvarianten einzelne Objekte, Methodverträge einzelne Methoden und Session Types einzelne Methoden im Kontext eines Protokolls.

• Wir entwerfen ein modulares Verifikationssystem mit BPL. BPL erlaubt es eine Programmlogik pro Verifikationsaspekt, zum Beispiel Objektinvarianten, zu entwerfen. BPL ermöglicht auch die Interaktion mit externen, statischen Analysen, z.B., Zeigeranalysen. BPL ermöglicht nicht nur den einfachen Entwurf neuer Programmlogiken, sondert erlaubt es Teile von Regeln wiederzuverwenden: die Kalküle aller Aspekte werden vor ihrer Anwendung zusammengesetzt. Basierend auf den Teilregeln konstruieren wir ein Korrektheitsargument für die zusammengesetzte Regel. BPL hat strukturelle Ähnlichkeiten zu Behavioral Types, was den Entwurf von Kalkülen erleichtern. Im Gegensatz zu anderen Dynamischen Logiken werden Programm und Spezifikation in einem Schritt manipuliert und syntaktisch verglichen.

Der Mangel an Modularität in Verifikationssystemen für verteile Systeme und die Notwendigkeit eines sturkturierteren Ansatzes im Entwurf von Programmlogiken sind als Defizite existierender Ansätze durch die Anwendung dieser Ansätze auf das FormbaR Modell für Eisenbahnbetrieb, der momentan größten Verifikationsstudie mit Active Objects, ermittelt worden. Diese Thesis schließt mit einer Diskussion die exemplarisch zeigt, dass BPL Eigenschaften spezifizieren und verifizieren kann, die über die Möglichkeiten bisheriger Ansätze hinausgehen.