2012 | OriginalPaper | Buchkapitel
Abstraction as a Unifying Link for Formal Approaches to Concurrency
verfasst von : Cliff B. Jones
Erschienen in: Software Engineering and Formal Methods
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Abstraction is a crucial tool in specifying and justifying developments of systems. This observation is recognised in many different methods for developing sequential software; it also applies to some approaches to the formal development of concurrent systems although there its use is perhaps less uniform. The rely/guarantee approach to formal design has, for example, been shown to be capable of recording the design of complex concurrent software in a “top down” stepwise process that proceeds from abstract specification to code. In contrast, separation logics were –at least initially– motivated by reasoning about details of extant code. Such approaches can be thought of as “bottom up”. The same “top down/bottom up” distinction can be applied to “atomicity refinement” and “linearisability”. Some useful mixes of these approaches already exist and they are neither to be viewed as competitive approaches nor are they irrevocably confined by the broad categorisation. This paper reports on recent developments and presents the case for how careful use of abstractions can make it easier to marry the respective advantages of different approaches to reasoning about concurrency.