Book contents
- Frontmatter
- Preface
- Contents
- An introduction to process algebra
- Two simple protocols
- Proving mutual exclusion with process algebra
- Process algebra as a tool for the specification and verification of CIM-architectures
- A process creation mechanism in process algebra
- Correctness proofs for systolic algorithms: palindromes and sorting
- Verification of an algorithm for log-time sorting by square comparison
- On the Amoeba protocol
- Process algebra semantics of POOL
- Some observations on redundancy in a context
- A modular approach to protocol verification using process algebra
- Index of concepts
- Index of names
- Index of symbols and notation
Process algebra semantics of POOL
Published online by Cambridge University Press: 03 December 2009
- Frontmatter
- Preface
- Contents
- An introduction to process algebra
- Two simple protocols
- Proving mutual exclusion with process algebra
- Process algebra as a tool for the specification and verification of CIM-architectures
- A process creation mechanism in process algebra
- Correctness proofs for systolic algorithms: palindromes and sorting
- Verification of an algorithm for log-time sorting by square comparison
- On the Amoeba protocol
- Process algebra semantics of POOL
- Some observations on redundancy in a context
- A modular approach to protocol verification using process algebra
- Index of concepts
- Index of names
- Index of symbols and notation
Summary
In this article we describe a translation of the Parallel Object-Oriented Language POOL to the language of ACP, the Algebra of Communicating Processes. This translation provides us with a large number of semantics for POOL. It is argued that an optimal semantics for POOL does not exist: what is optimal depends on the application domain one has in mind. We show that the select statement in POOL makes a semantical description of POOL with handshaking communication between objects incompatible with a description level where message queues are used. Attention is paid to the question how fairness and successful termination can be included in the semantics. Finally it is shown that integers and booleans in POOL can be implemented in various ways.
INTRODUCTION
At this moment there are a lot of programming languages which offer facilities for concurrent programming. The basic notions of some of these languages, for example CSP, occam and LOTOS, are rather close to the basic notions in ACP, and it is not very difficult to give semantics of these languages in the framework of ACP. Milner showed how a simple high level concurrent language can be translated into CCS. However, it is not obvious at first sight how to give process algebra semantics of more complex concurrent programming languages like Ada, Pascal-Plus or POOL. This is an important problem because of the simple fact that a lot of concurrent systems are specified in terms of these languages. In this article we will tackle the problem, and give process algebra semantics of the language POOL.
- Type
- Chapter
- Information
- Applications of Process Algebra , pp. 173 - 236Publisher: Cambridge University PressPrint publication year: 1990
- 20
- Cited by