| |
| |
Preface | |
| |
| |
| |
Introduction | |
| |
| |
| |
Background | |
| |
| |
| |
Perspective | |
| |
| |
| |
Tools | |
| |
| |
| |
What is a communication? | |
| |
| |
| |
A Foundation Course in CSP | |
| |
| |
| |
Fundamental concepts | |
| |
| |
| |
Fundamental operators | |
| |
| |
| |
Algebra | |
| |
| |
| |
The traces model and traces refinement | |
| |
| |
| |
Tools | |
| |
| |
| |
Parallel operators | |
| |
| |
| |
Synchronous parallel | |
| |
| |
| |
Alphabetized parallel | |
| |
| |
| |
Interleaving | |
| |
| |
| |
Generalized parallel | |
| |
| |
| |
Parallel composition as conjunction | |
| |
| |
| |
Tools | |
| |
| |
| |
Postscript: On alphabets | |
| |
| |
| |
Hiding and renaming | |
| |
| |
| |
Hiding | |
| |
| |
| |
Renaming and alphabet transformations | |
| |
| |
| |
A basic guide to failures and divergences | |
| |
| |
| |
Tools | |
| |
| |
| |
Piping and enslavement | |
| |
| |
| |
Piping | |
| |
| |
| |
Enslavement | |
| |
| |
| |
Tools | |
| |
| |
| |
Buffers and communication | |
| |
| |
| |
Pipes and buffers | |
| |
| |
| |
Buffer tolerance | |
| |
| |
| |
The alternating bit protocol | |
| |
| |
| |
Tools | |
| |
| |
| |
Termination and sequential composition | |
| |
| |
| |
What is termination? | |
| |
| |
| |
Distributed termination | |
| |
| |
| |
Laws | |
| |
| |
| |
Effects on the traces model | |
| |
| |
| |
Effects on the failures/divergences model | |
| |
| |
| |
Theory | |
| |
| |
| |
Operational semantics | |
| |
| |
| |
A survey of semantic approaches to CSP | |
| |
| |
| |
Transition systems and state machines | |
| |
| |
| |
Firing rules for CSP | |
| |
| |
| |
Relationships with abstract models | |
| |
| |
| |
Tools | |
| |
| |
| |
Notes | |
| |
| |
| |
Denotational semantics | |
| |
| |
| |
Introduction | |
| |
| |
| |
The traces model | |
| |
| |
| |
The failures/divergences model | |
| |
| |
| |
The stable failures model | |
| |
| |
| |
Notes | |
| |
| |
| |
Analyzing the denotational models | |
| |
| |
| |
Deterministic processes | |
| |
| |
| |
Analyzing fixed points | |
| |
| |
| |
Full abstraction | |
| |
| |
| |
Relations with operational semantics | |
| |
| |
| |
Notes | |
| |
| |
| |
Infinite traces | |
| |
| |
| |
Calculating infinite traces | |
| |
| |
| |
Adding failures | |
| |
| |
| |
Using infinite traces | |
| |
| |
| |
Notes | |
| |
| |
| |
Algebraic semantics | |
| |
| |
| |
Introduction | |
| |
| |
| |
Operational semantics via algebra | |
| |
| |
| |
The laws of [perpendicular, bottom subscript N] | |
| |
| |
| |
Normalizing | |
| |
| |
| |
Sequential composition and SKIP | |
| |
| |
| |
Other models | |
| |
| |
| |
Notes | |
| |
| |
| |
Abstraction | |
| |
| |
| |
Modes of abstraction | |
| |
| |
| |
Reducing specifications | |
| |
| |
| |
Abstracting errors: specifying fault tolerance | |
| |
| |
| |
Independence and security | |
| |
| |
| |
Tools | |
| |
| |
| |
Notes | |
| |
| |
| |
Practice | |
| |
| |
| |
Deadlock! | |
| |
| |
| |
Basic principles and tree networks | |
| |
| |
| |
Specific ways to avoid deadlock | |
| |
| |
| |
Variants | |
| |
| |
| |
Network decomposition | |
| |
| |
| |
The limitations of local analysis | |
| |
| |
| |
Deadlock and tools | |
| |
| |
| |
Notes | |
| |
| |
| |
Modelling discrete time | |
| |
| |
| |
Introduction | |
| |
| |
| |
Meeting timing constraints | |
| |
| |
| |
Case study 1: level crossing gate | |
| |
| |
| |
Checking untimed properties of timed processes | |
| |
| |
| |
Case study 2: the alternating bit protocol | |
| |
| |
| |
Urgency and priority | |
| |
| |
| |
Tools | |
| |
| |
| |
Notes | |
| |
| |
| |
Case studies | |
| |
| |
| |
Combinatorial systems: rules and tactics | |
| |
| |
| |
Distributed data and data-independence | |
| |
| |
| |
Breaking crypto-protocols | |
| |
| |
| |
Notes | |
| |
| |
| |
Mathematical background | |
| |
| |
| |
Partial orders | |
| |
| |
| |
Metric spaces | |
| |
| |
| |
A guide to machine-readable CSP | |
| |
| |
| |
Introduction | |
| |
| |
| |
Expressions | |
| |
| |
| |
Pattern matching | |
| |
| |
| |
Types | |
| |
| |
| |
Processes | |
| |
| |
| |
Special definitions | |
| |
| |
| |
Mechanics | |
| |
| |
| |
Missing features | |
| |
| |
| |
Availability | |
| |
| |
| |
The operation of FDR | |
| |
| |
| |
Basic operation | |
| |
| |
| |
Hierarchical compression | |
| |
| |
Notation | |
| |
| |
Bibliography | |
| |
| |
Main index | |
| |
| |
Index of named processes | |