Paper Info
Title
Observable behavior of distributed systems: Component reasoning for concurrent objects.
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 difficulties 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 relative completeness of this proof system are shown using a transformational approach from a sequential language with a non-deterministic assignment operator.
Year
DOI
Venue
2012
10.1016/j.jlap.2012.01.003
The Journal of Logic and Algebraic Programming
Keywords
DocType
Volume
Distributed systems,Object-orientation,Compositional reasoning,Hoare Logic,Concurrent objects
Journal
81
Issue
ISSN
Citations 
3
1567-8326
22
PageRank 
References 
Authors
0.78
17
4
Name
Order
Citations
PageRank
Crystal Chang Din1827.87
Johan Dovland21598.18
Einar Broch Johnsen3107169.56
Olaf Owe460448.17