| |
| |
| 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 | |