TU Darmstadt / ULB / TUprints

Modular Verification of a Modular Specification: Behavioral Types as Program Logics

Kamburjan, Eduard (2020)
Modular Verification of a Modular Specification: Behavioral Types as Program Logics.
Technische Universität Darmstadt
doi: 10.25534/tuprints-00011664
Ph.D. Thesis, Primary publication

[img]
Preview
Text
Kamburjan.pdf
Copyright Information: CC BY-NC-ND 4.0 International - Creative Commons, Attribution NonCommercial, NoDerivs.

Download (945kB) | Preview
Item Type: Ph.D. Thesis
Type of entry: Primary publication
Title: Modular Verification of a Modular Specification: Behavioral Types as Program Logics
Language: English
Referees: Hähnle, Prof. Dr. Reiner ; de Boer, Prof. Dr. Frank
Date: 2020
Place of Publication: Darmstadt
Date of oral examination: 31 March 2020
DOI: 10.25534/tuprints-00011664
Abstract:

Verification of distributed systems is a challenging problem, especially if the distributed system allows entities to interact in multiple ways. The complexity of the task is mirrored in the complexity of the verification system. The design of such verification systems itself is a challenge on the theoretical level. The main engineering tool to handle complex systems is modularization. While modularity in the target system is exploited by verification systems, it is rarely applied to their theory. This thesis is a study of modularity in deductive verification with program logics and the main tool we introduce is the Behavioral Program Logic (BPL). As concurrency model we use Active Objects, because, for one, they allow multiple ways for entities to interact, for another, because their strong encapsulation enables modularization on the semantic level. Modularity is applied on multiple layers:

• We present a modular, new Locally Abstract, Globally Concrete semantics for Active Objects, that allows us to sharply distinguish between local and global behavior.

• We introduce a modular specification principle with object invariants, asynchronous method contracts, Effect Types and Session Types. Each of these specifications itself is modular and describes the behavior of an encapsulated entity. E.g., object invariants describe single objects, method contracts describe single methods, Session Types describe single methods in a protocol context.

• We design a modular verification system with BPL. BPL allows one to design one logic per verification aspect, such as presence of object invariants, as well as interfacing with external static analyses, such as pointer analyses. BPL enables us not only the simple design of new program logics, it also allows reuse on the rule level: The calculi of all aspects are composed before being applied. For composition, we give a mostly automatic soundness argument for the composed rule. BPL has structural similarities with behavioral types, which simplify calculus design — the most prominent is that the calculus modifies program and specification in one step, after syntactically matching them. This is uncommon in other dynamic logics.

The lack of modularity in verification of distributed systems and the need for a more structural approach in the design of program logics are identified as shortcomings of state-of-the-art approaches by applying existing tools to the FormbaR model of railway operations, the biggest verification study with Active Objects to date. This thesis concludes with a discussion that exemplifies how our approach can express and verify properties that were not possible before.

Alternative Abstract:
Alternative AbstractLanguage

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.

German
URN: urn:nbn:de:tuda-tuprints-116645
Classification DDC: 000 Generalities, computers, information > 004 Computer science
500 Science and mathematics > 510 Mathematics
Divisions: 20 Department of Computer Science > Software Engineering
Date Deposited: 26 May 2020 12:28
Last Modified: 09 Jul 2020 06:31
URI: https://tuprints.ulb.tu-darmstadt.de/id/eprint/11664
PPN: 465156568
Export:
Actions (login required)
View Item View Item