TU Darmstadt / ULB / TUbiblio

Compositional reasoning about active objects with shared futures

Din, Crystal Chang and Owe, Olaf (2014):
Compositional reasoning about active objects with shared futures.
In: Formal Aspects of Computing, pp. 1-22, (Distributed systems; Obje), DOI: 10.1007/s00165-014-0322-y, [Article]

Abstract

Distributed and concurrent object-oriented systems are difficult to analyze due to the complexity of their concurrency, communication, and synchronization mechanisms. The future mechanism extends the traditional method call communication model by facilitating sharing of references to futures. By assigning method call result values to futures, third party objects may pick up these values. This may reduce the time spent waiting for replies in a distributed environment. However, futures add a level of complexity to program analysis, as the program semantics becomes more involved. This paper presents a model for asynchronously communicating objects, where return values from method calls are handled by futures. The model facilitates invariant specifications over the locally visible communication history of each object. Compositional reasoning is supported and proved sound, as each object may be specified and verified independently of its environment. A kernel object-oriented language with futures inspired by the ABS modeling language is considered. A compositional proof system for this language is presented, formulated within dynamic logic.

Item Type: Article
Erschienen: 2014
Creators: Din, Crystal Chang and Owe, Olaf
Title: Compositional reasoning about active objects with shared futures
Language: ["languages_typename_1" not defined]
Abstract:

Distributed and concurrent object-oriented systems are difficult to analyze due to the complexity of their concurrency, communication, and synchronization mechanisms. The future mechanism extends the traditional method call communication model by facilitating sharing of references to futures. By assigning method call result values to futures, third party objects may pick up these values. This may reduce the time spent waiting for replies in a distributed environment. However, futures add a level of complexity to program analysis, as the program semantics becomes more involved. This paper presents a model for asynchronously communicating objects, where return values from method calls are handled by futures. The model facilitates invariant specifications over the locally visible communication history of each object. Compositional reasoning is supported and proved sound, as each object may be specified and verified independently of its environment. A kernel object-oriented language with futures inspired by the ABS modeling language is considered. A compositional proof system for this language is presented, formulated within dynamic logic.

Journal or Publication Title: Formal Aspects of Computing
Number: Distributed systems; Obje
Uncontrolled Keywords: Distributed systems, Object orientation, Concurrent objects, Asynchronous communication, Shared futures, Operational semantics, Communication history, Compositional reasoning, Dynamic logic
Divisions: 20 Department of Computer Science > Software Engineering
20 Department of Computer Science
Date Deposited: 31 Dec 2016 10:40
DOI: 10.1007/s00165-014-0322-y
Identification Number: TUD-CS-2014-1006
Export:

Optionen (nur für Redakteure)

View Item View Item