Modular specifications in process algebra---with curious queues (extended abstract)

R.J. van Glabbeek, F.W. Vaandrager

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

In recent years a wide variety of process algebras has been proposed in the literature. Often these process algebras are closely related: they can be viewed as homomorphic images, submodels or restrictions of each other. The aim of this paper is to show how the semantical reality, consisting of a large number of closely related process algebras, can be reflected, and even used, on the level of algebraic specifications and in process verifications. This is done by means of the notion of a module. The simplest modules are building blocks of operators and axioms, each block describing a feature of concurrency in a certain semantical setting. These modules can then be combined by means of a union operator +, an export operator □, allowing to forget some operators in a module, an operator H, changing semantics by taking homomorphic images, and an operator S which takes subalgebras. These operators enable us to combine modules in a subtle way, when the direct combination would be inconsistent. We show how auxiliary process algebra operators can be hidden when this is needed. Moreover it is demonstrated how new process combinators can be defined in terms of the more elementary ones in a clean way. As an illustration of our approach, a methodology is presented that can be used to specify FIFO-queues, and that facilitates verification of concurrent systems containing these queues.

Original languageEnglish
Title of host publicationAlgebraic Methods: Theory, Tools and Applications
EditorsM. Wirsing, J.A. Bergstra
PublisherSpringer-Verlag
Pages465-506
Number of pages42
Volume394
ISBN (Electronic)978-3-540-46758-8
ISBN (Print)978-3-540-51698-9
DOIs
Publication statusPublished - 20 Sept 1989
EventAlgebraic Methods: Theory, Tools and Applications, 1987 - Passau, Germany
Duration: 9 Jun 198711 Jun 1987

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume394
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Workshop

WorkshopAlgebraic Methods: Theory, Tools and Applications, 1987
Country/TerritoryGermany
CityPassau
Period9/06/8711/06/87

Fingerprint

Dive into the research topics of 'Modular specifications in process algebra---with curious queues (extended abstract)'. Together they form a unique fingerprint.

Cite this