Failures-Divergence Refinement

FDR2 User Manual

24 October 1997

• 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 FDR2 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 Channels
    • A.3.5 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 Migrating to FDR2.28
  • 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.26 to 2.27
• 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
• D Multiplexed Buffer Script
• E Bibliography

This document was generated on 23 November 1998 using the texi2html translator version 1.51.