Understanding Concurrent Systems (Texts in Computer Science)

Preface
	Overview and Goals
	Organisation and Features
		Part I: An Introduction to CSP
		Part II: Theory
		Part III: Using CSP
		Part IV: Exploring Concurrency
	Target Audience
	Notes to the Instructor
	Teaching Resources
	And Finally…
Acknowledgements
Contents
A Foundation Course in CSP
	Building a Simple Sequential Process
		Basic Operators
			Prefixing
			Recursion
			Guarded Alternative
		Choice Operators
			External Choice
			Nondeterministic Choice
			Conditional Choice
			Multi-Part Events: Extending the Notation of Channels
		A Few Important Processes
		Traces Refinement
		What is a Communication?
		Tools
			Finite-State Machines
	Understanding CSP
		Algebra
		The Traces Model and Traces Refinement
			Working out traces(P)
			Traces and Laws
			Unique Fixed Points
			Specification and Refinement
			Afters and Initials
		Operational Semantics and Labelled Transition Systems
		Tools
	Parallel Operators
		Synchronous Parallel
			Turning Parallel Processes into Sequential Ones
		Alphabetised Parallel
		Interleaving
		Generalised Parallel
		Parallel Composition as Conjunction
		Tools
		Postscript: On Alphabets
	CSP Case Studies
		Sudoku in CSP
		Deadlock-Free Routing
			Head for the Trees!
			Uncloggable Rings
			The Mad Postman
		Communications Protocols
	Hiding and Renaming
		Hiding
			The Consequences of Hiding
			Hiding versus Constructiveness
		Renaming and Alphabet Transformations
			Injective Functions
			Non-injective Functions
			Relational Renaming
				One-to-Many Renaming as a Magic Wand
		Linking Operators
		Tools
	Beyond Traces
		A Brief Introduction to Failures and Divergences
		Failures and Divergences in Specifications
		Ungranted Requests and the Limits of Failures
		Avoiding Divergence
		Abstraction by Hiding
		Tools
	Further Operators
		Termination and Sequential Composition
			What is Termination?
				Iteration
			Distributed Termination
			Effects on the Failures-Divergences Model
		Interrupting Processes
		Tools
	Using FDR
		What is FDR?
			Running and Debugging Checks
			FDR\'s Settings
			Defining Non-Process Objects
			The Limits of FDR
		Checking Parallel Processes
		The Structure of a Refinement Check
		Failures and Divergences
		Watchdogs
		Breadth versus Depth, Symmetry and Divergence
		Determinism Checking
		Compression
			Using Compression
				Compression on the Left-Hand Side of a Refinement Check
		Notes and Reflections
Theory
	Operational Semantics
		Transition Systems and State Machines
		Firing Rules for CSP
			SOS Style Operational Rules
			Combinator Style Operational Rules
		From Combinators to Supercombinators!
		Translating Combinators to CSP
		Relationships with Abstract Models
			Extracting Failures and Divergences
			Infinite Traces and Infinite Branching
		Tools
		Notes
	Denotational Semantics and Behavioural Models
		Introduction
			Fixed-Point Theory
		Analysing Traces Semantics
		The Stable Failures Model
			Applications
			Channel-Based Failures
		The Failures-Divergences Model
		Determinism, Confluence and Proof
		Full Abstraction and Congruence
		Notes
	Finite Observation Models
		What is a Behavioural Model?
			The Finest Model of Them All
				Applications
			Clouding the Glass
		A Tour through the Hierarchy
			The Ready Sets, or Acceptances Model A
				Applications
			The Stable Refusal Testing Model RT
				Applications
			The Stable Revivals Model
				Applications
			Other Models
				Possible Futures: A Study in Linearity
		The Big Picture
		Tools
	Infinite-Behaviour Models
		Divergence-Strict Models for Finite Nondeterminism
			Determinism amongst the Richer Models
			Applications
		Strict Divergence for General CSP
			Healthiness Conditions
			Fixed Point Theories for Unbounded Nondeterminism
			Applying Infinite-Behaviour Models
		The Hierarchy of Divergence-Strict Models
		Seeing Beyond Divergence
			Applications of M#
		The Fixed Point Theory of M#
		The Hierarchy
		Tools
		Notes
	The Algebra of CSP
		Introduction
		AOS Form
		Algebraic Operational Semantics
		Normal Forms
		A Tour through the Hierarchy
		General Programs
		Notes
Using CSP in Practice
	Timed Systems 1: -CSP
		Introduction
		A Brief History of Time in CSP
		tock-CSP
			Expressing Timing Constraints
		Case Study: Bully Algorithm
			The Bully Algorithm
			Part 1: Specification
			Part 2: Implementation
			Analysis
			Conclusions
		Maximal Progress and Priority
			Case Study: Timed Routing
		Specifying and Metering tock-CSP
		Tools
	Timed Systems 2: Discrete Timed CSP
		Modelling Timed CSP
			Semantics
		Examples
		Digitisation
		Notes for Chapters 14 and 15
	More About FDR
		Normalisation
			Stage 1
		More About Compression
			Strong Bisimulation
			DRW-Bisimulation
			tau-Loop Elimination
			Diamond Elimination
			Laziness and chase
		Handling Large Checks
			Memory Locality
			Parallel Implementation
		Generalising the Specification Model
	State Explosion and Parameterised Verification
		Induction
			The Limitations of Induction
		Data Independence
			Thresholds
				When |T|=1 is Enough
				When |T|=2 is Enough
				The General Case
			Beyond Thresholds
		Data-Independent Induction
		Buffer Tolerance
			Definitions, Basics and Tree Networks
			Functional and Confluent Processes
		Approximation Based Methods
		Notes
Exploring Concurrency
	Shared-Variable Programs
		Writing a Compiler in CSPM
			Data Types
			Variable Names
			Compilation Strategy
			Compiling a Thread
			Evaluating an Expression
				Pros and Cons of Compiler Writing in CSP
		Applying Compression
		The Front End of SVA
			SVL
			The GUI
			Possible Extensions
		Specifications in SVA
		Case Study: Lamport\'s Bakery Algorithm
		Case Study: The Dining Philosophers in SVL
		Notes
	Understanding Shared-Variable Concurrency
		Dirty Variables
		Case Study: Simpson\'s 4-Slot Algorithm
		Observing and Refining SVL Programs
			The Bakery Algorithm Revisited
		Atomic Equivalent Programs
		Overseers: Modelling Complex Data-Types
		Abstraction in SVA
			Two Threads out of Many
			Finitely Representing an Infinite Linear Order
		Notes
	Priority and Mobility
		Case Study: Knight\'s Tour
		Priority
			Statecharts
			Synchronous Two-Phase Automata
				Determinism of Two-Phase Models
		Mobility
			An Introduction to Mobility
			Towards a \"Mobile CSP\"
			Pass the Port!
			Closed Worlds
			Opening Out
		Notes
Notation
	Sets and Numbers
	Logic
	Partial Orders
	Communications
	Sequence/Trace Notation (See pp. 30 and 36)
	Transition Systems (See Sect. 9.1)
	Processes
	Semantic Models
References
Index