Din, Crystal Chang ; Dovland, Johan ; Johnsen, Einar Broch ; Owe, Olaf (2012)
Observable behavior of distributed systems: Component reasoning for concurrent objects.
In: Journal of Logic and Algebraic Programming, 81 (3)
doi: 10.1016/j.jlap.2012.01.003
Artikel, Bibliographie
Kurzbeschreibung (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.
| Typ des Eintrags: | Artikel |
|---|---|
| Erschienen: | 2012 |
| Autor(en): | Din, Crystal Chang ; Dovland, Johan ; Johnsen, Einar Broch ; Owe, Olaf |
| Art des Eintrags: | Bibliographie |
| Titel: | Observable behavior of distributed systems: Component reasoning for concurrent objects |
| Sprache: | Deutsch |
| Publikationsjahr: | 2012 |
| Titel der Zeitschrift, Zeitung oder Schriftenreihe: | Journal of Logic and Algebraic Programming |
| Jahrgang/Volume einer Zeitschrift: | 81 |
| (Heft-)Nummer: | 3 |
| DOI: | 10.1016/j.jlap.2012.01.003 |
| Kurzbeschreibung (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. |
| ID-Nummer: | TUD-CS-2012-0366 |
| 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