TU Darmstadt / ULB / TUbiblio

Observable behavior of distributed systems: Component reasoning for concurrent objects

Din, Crystal Chang and Dovland, Johan and Johnsen, Einar Broch and Owe, Olaf (2012):
Observable behavior of distributed systems: Component reasoning for concurrent objects.
In: Journal of Logic and Algebraic Programming, pp. 227-256, 81, (3), DOI: 10.1016/j.jlap.2012.01.003, [Article]

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.

Item Type: Article
Erschienen: 2012
Creators: Din, Crystal Chang and Dovland, Johan and Johnsen, Einar Broch and Owe, Olaf
Title: Observable behavior of distributed systems: Component reasoning for concurrent objects
Language: German
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.

Journal or Publication Title: Journal of Logic and Algebraic Programming
Volume: 81
Number: 3
Divisions: 20 Department of Computer Science > Software Engineering
20 Department of Computer Science
Date Deposited: 31 Dec 2016 10:40
DOI: 10.1016/j.jlap.2012.01.003
Identification Number: TUD-CS-2012-0366
Export:

Optionen (nur für Redakteure)

View Item View Item