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.