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 |