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
Some observations on redundancy in a context
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
Let x be a process which can perform an action a when it is in state s. In this article we consider the situation where x is placed in a context which blocks a whenever, x is in s. The option of doing a in state s is redundant in such a context and x can be replaced by a process x′ which is identical to x, except for the fact that x′ cannot do a when it is in s (irrespective of the context). A simple, compositional proof technique is presented, which uses information about the traces of processes to detect redundancies in a process specification. As an illustration of the technique, a modular verification of a workcell architecture is presented.
INTRODUCTION
We are interested in the verification of distributed systems by means of algebraic manipulations. In process algebra, verifications often consist of a proof that the behaviour of an implementation IMPL equals the behaviour of a specification SPEC, after abstraction from internal activity: τI(IMPL) = SPEC.
The simplest strategy to prove such a statement is to derive first the transition system (process graph) for the process IMPL with the expansion theorem, apply an abstraction operator to this transition system, and then simplify the resulting system to the system for SPEC using the laws of (for instance) bisimulation semantics. This ‘global’ strategy however, is often not very practical due to combinatorial state explosion: the number of states of IMPL can be of the same order as the product of the number of states of its components. Another serious problem with this strategy is that it provides almost no ‘insight’ in the structure of the system being verified.
- Type
- Chapter
- Information
- Applications of Process Algebra , pp. 237 - 260Publisher: Cambridge University PressPrint publication year: 1990
- 5
- Cited by