On the relation of rely-guarantee and assume-guarantee reasoning

Eissing, Marcel; Mertens, Hannah; Noll, Thomas; Verscht, Lena; Katoen, Joost-Pieter

doi:10.18154/RWTH-2025-09295

On the relation of rely-guarantee and assume-guarantee reasoning

Eissing, Marcel^RWTH*

2025

Verantwortlichkeitsangabeby Marcel Eissing

ImpressumAachen : RWTH Aachen University 2025

Umfang1 Online-Ressource : Illustrationen

Bachelorarbeit, RWTH Aachen University, 2025

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor)^RWTH* ; Noll, Thomas (Thesis advisor)^RWTH* ; Verscht, Lena (Consultant)^RWTH* ; Mertens, Hannah (Consultant)^RWTH*

Tag der mündlichen Prüfung/Habilitation
2025-09-07

Online
DOI: 10.18154/RWTH-2025-09295
URL: https://publications.rwth-aachen.de/record/1020873/files/1020873.pdf

Einrichtungen

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Assume-guarantee and rely-guarantee reasoning are well-established compositional methods dealing with the verification of composite systems. While assume-guarantee reasoning targets parallel com- position of transition systems, rely-guarantee reasoning is tailored to concurrent shared memory pro- grams. Both concepts are similar in their approach, as they focus their analysis on a local component and introduce an abstraction of its environment. The abstraction of the environment is used as an assumption under which a desired property can be guaranteed. Though the concepts work in a similar fashion, they exhibit substantial differences. This thesis explores the concrete nature of the relationship of assume-guarantee and rely-guarantee reasoning. We propose a formal construction that translates the verification of a rely-guarantee specification on a concurrent program to the verification of properties on transition systems in the context of assume-guarantee reasoning. We show that our construction is indicative of a close relation between the inference rule for concurrency in rely-guarantee reasoning and a non-circular assume-guarantee inference rule. Additionally, we show that our construction can be used as a new means to prove a rely-guarantee specification of a concurrent program.

OpenAccess:
PDF