TU Darmstadt / ULB / TUbiblio

Observable behavior of distributed systems: Component reasoning for concurrent objects

Din, Crystal Chang ; Dovland, Johan ; Johnsen, Einar Broch ; Owe, Olaf (2012)
Observable behavior of distributed systems: Component reasoning for concurrent objects.
In: Journal of Logic and Algebraic Programming, 81 (3)
doi: 10.1016/j.jlap.2012.01.003
Artikel, Bibliographie

Kurzbeschreibung (Abstract)

Distributed and concurrent object-oriented systems are difficult to analyze due to the complexity of their concurrency, communication, and synchronization mechanisms. Rather than performing analysis at the level of code in, e.g., Java or C++, we consider the analysis of such systems at the level of an abstract, executable modeling language. This language, based on concurrent objects communicating by asynchronous method calls, avoids some difficul-ties of mainstream object-oriented programming languages related to compositionality and aliasing. To facilitate system analysis, compositional verification systems are needed, which allow components to be analyzed independently of their environment. In this paper, a proof system for partial correctness reasoning is established based on communication histories and class invariants. A particular feature of our approach is that the alphabets of different objects are completely disjoint. Compared to related work, this allows the formulation of a much simpler Hoare-style proof system and reduces reasoning complexity by significantly simplifying formulas in terms of the number of needed quantifiers. The soundness and rel-ative completeness of this proof system are shown using a transformational approach from a sequential language with a non-deterministic assignment operator.

Typ des Eintrags: Artikel
Erschienen: 2012
Autor(en): Din, Crystal Chang ; Dovland, Johan ; Johnsen, Einar Broch ; Owe, Olaf
Art des Eintrags: Bibliographie
Titel: Observable behavior of distributed systems: Component reasoning for concurrent objects
Sprache: Deutsch
Publikationsjahr: 2012
Titel der Zeitschrift, Zeitung oder Schriftenreihe: Journal of Logic and Algebraic Programming
Jahrgang/Volume einer Zeitschrift: 81
(Heft-)Nummer: 3
DOI: 10.1016/j.jlap.2012.01.003
Kurzbeschreibung (Abstract):

Distributed and concurrent object-oriented systems are difficult to analyze due to the complexity of their concurrency, communication, and synchronization mechanisms. Rather than performing analysis at the level of code in, e.g., Java or C++, we consider the analysis of such systems at the level of an abstract, executable modeling language. This language, based on concurrent objects communicating by asynchronous method calls, avoids some difficul-ties of mainstream object-oriented programming languages related to compositionality and aliasing. To facilitate system analysis, compositional verification systems are needed, which allow components to be analyzed independently of their environment. In this paper, a proof system for partial correctness reasoning is established based on communication histories and class invariants. A particular feature of our approach is that the alphabets of different objects are completely disjoint. Compared to related work, this allows the formulation of a much simpler Hoare-style proof system and reduces reasoning complexity by significantly simplifying formulas in terms of the number of needed quantifiers. The soundness and rel-ative completeness of this proof system are shown using a transformational approach from a sequential language with a non-deterministic assignment operator.

ID-Nummer: TUD-CS-2012-0366
Fachbereich(e)/-gebiet(e): 20 Fachbereich Informatik > Software Engineering
20 Fachbereich Informatik
Hinterlegungsdatum: 31 Dez 2016 10:40
Letzte Änderung: 16 Mai 2018 12:06
PPN:
Export:
Suche nach Titel in: TUfind oder in Google
Frage zum Eintrag Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen