TU Darmstadt / ULB / TUbiblio

Compositional Reasoning about Shared Futures

Din, Crystal Chang and Dovland, Johan and Owe, Olaf
Eleftherakis, George and Hinchey, Mike and Holcombe, Mike (eds.) (2012):
Compositional Reasoning about Shared Futures.
In: Software Engineering and Formal Methods, Springer Berlin Heidelberg, In: Lecture Notes in Computer Science, ISBN 978-3-642-33825-0,
DOI: 10.1007/978-3-642-33826-7_7, [Conference or Workshop Item]

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, 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: Conference or Workshop Item
Erschienen: 2012
Editors: Eleftherakis, George and Hinchey, Mike and Holcombe, Mike
Creators: Din, Crystal Chang and Dovland, Johan and Owe, Olaf
Title: Compositional Reasoning about 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, 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.

Title of Book: Software Engineering and Formal Methods
Series Name: Lecture Notes in Computer Science
Volume: 7504
Publisher: Springer Berlin Heidelberg
ISBN: 978-3-642-33825-0
Divisions: 20 Department of Computer Science > Software Engineering
20 Department of Computer Science
Date Deposited: 31 Dec 2016 10:40
DOI: 10.1007/978-3-642-33826-7_7
Identification Number: TUD-CS-2012-0365
Export:

Optionen (nur für Redakteure)

View Item View Item