Din, Crystal Chang ; Dovland, Johan ; Owe, Olaf
Hrsg.: Eleftherakis, George ; Hinchey, Mike ; Holcombe, Mike (2012)
Compositional Reasoning about Shared Futures.
doi: 10.1007/978-3-642-33826-7_7
Konferenzveröffentlichung, Bibliographie
Kurzbeschreibung (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.
| Typ des Eintrags: | Konferenzveröffentlichung |
|---|---|
| Erschienen: | 2012 |
| Herausgeber: | Eleftherakis, George ; Hinchey, Mike ; Holcombe, Mike |
| Autor(en): | Din, Crystal Chang ; Dovland, Johan ; Owe, Olaf |
| Art des Eintrags: | Bibliographie |
| Titel: | Compositional Reasoning about Shared Futures |
| Sprache: | Englisch |
| Publikationsjahr: | 2012 |
| Verlag: | Springer Berlin Heidelberg |
| Buchtitel: | Software Engineering and Formal Methods |
| Reihe: | Lecture Notes in Computer Science |
| Band einer Reihe: | 7504 |
| DOI: | 10.1007/978-3-642-33826-7_7 |
| Kurzbeschreibung (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. |
| ID-Nummer: | TUD-CS-2012-0365 |
| 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 |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum