Tutorial on Refinement in State-based Specification Languages

In this tutorial we aim to provide:

  1. An introduction to the idea of refinement as a formal development process.
  2. An insight into how refinement is defined in Z and other specification languages.
  3. An understanding of how the relational basis for Z leads to the derivation of the Z simulation rules as they are usually presented.
  4. An understanding of the relationship to various process algebraic refinement relations.

The preliminary outline is as follows:

  • Overview of Refinement
  • A relational framework
  • Data refinement
  • Simulations
  • Refinement in Z
  • Deriving simulations in Z
  • Examples
  • Concurrent models of refinement
  • Unifying relational and concurrent refinement

Last updated 21 Apr 2006.