Table of Contents

Acknowledgements
1. Introduction

1.1 What is FDR?
1.2 The CSP View of the World
1.3 CSP Refinement

1.3.1 Using refinement
1.3.2 Simple buffer example
1.3.3 Checking refinement

1.4 Specification Example

1.4.1 Multiplexed buffer example

2. Using FDR

2.1 The Main Window
2.2 On-line Help
2.3 File and Model Commands

2.3.1 The Load command
2.3.2 The Reload command
2.3.3 The Edit command
2.3.4 The All Asserts command
2.3.5 The Exit command

2.4 The Assertion List
2.5 The Process List
2.6 The Tab Pane
2.7 Options
2.8 Tab Bar Commands
2.9 The FDR Process Debugger

2.9.1 Debugger menu commands
2.9.2 Viewing process behaviours

2.9.2.1 The process structure
2.9.2.2 The behaviour information

2.10 Interface Conventions

2.10.1 GUI conventions
2.10.2 Keyboard short-cuts

3. Tutorial

3.1 Describing Processes

3.1.1 Sample script for FDR2

3.2 Using the Checker

3.2.1 Environment
3.2.2 Getting started
3.2.3 Debugging

4. Intermediate FDR

4.1 Building a Model

4.1.1 Abstract model
4.1.2 Use components

4.2 Tuning for FDR

4.2.1 Share components
4.2.2 Factor state
4.2.3 Use local definitions

4.3 Choice of Model

5. Advanced Topics

5.1 Using Compressions

5.1.1 Methods of compression
5.1.2 Compressions in context
5.1.3 Hiding and safety properties
5.1.4 Hiding and deadlock

5.2 Technical Details

5.2.1 Generalised Transition Systems
5.2.2 State-space Reduction

5.2.2.1 Computing semantic equivalence
5.2.2.2 Diamond elimination
5.2.2.3 Combining techniques

A. Syntax Reference

A.1 Expressions

A.1.1 Identifiers
A.1.2 Numbers
A.1.3 Sequences
A.1.4 Sets
A.1.5 Booleans
A.1.6 Tuples
A.1.7 Local definitions
A.1.8 Lambda terms

A.2 Pattern Matching
A.3 Types

A.3.1 Simple types
A.3.2 Named types
A.3.3 Datatypes
A.3.4 Subtypes
A.3.5 Channels
A.3.6 Closure operations

A.4 Processes
A.5 Operator Precedence
A.6 Special Definitions

A.6.1 External
A.6.2 Transparent
A.6.3 Assert
A.6.4 Print

A.7 Mechanics
A.8 Missing Features

B. Changes to FDR

B.1 Changes from FDR1 to FDR2
B.2 Changes from 2.0 to 2.1
B.3 Changes from 2.1 to 2.20
B.4 Changes from 2.20 to 2.22
B.5 Changes from 2.22 to 2.23
B.6 Changes from 2.23 to 2.24
B.7 Changes from 2.24 to 2.25
B.8 Changes from 2.25 to 2.26
B.9 Changes from 2.26 to 2.27
B.10 Changes from 2.27 to 2.28
B.11 Changes from 2.28 to 2.64
B.12 Changes from 2.64 to 2.68
B.13 Changes from 2.68 to 2.69
B.14 Changes from 2.69 to 2.76
B.15 Changes from 2.76 to 2.77
B.16 Changes from 2.77 to 2.78
B.17 Changes from 2.78 to 2.80
B.18 Changes from 2.80 to 2.81
B.19 Changes from 2.81 to 2.82

C. Direct control of FDR

C.1 Batch interface
C.2 Script interface
C.3 Object model

C.3.1 Notes on the object model
C.3.2 Session objects
C.3.3 Ism objects
C.3.4 Hypothesis objects
C.3.5 FDRSet objects

D. Configuration

D.1 Environment variables

D.1.1 Location
D.1.2 Tools
D.1.3 Paging

D.2 Performance

E. Multiplexed Buffer Script
F. Bibliography