Tutorial on Refinement in State-based Specification Languages
In this tutorial we aim to provide:
- An introduction to the idea of refinement as a formal development process.
- An insight into how refinement is defined in Z and other specification languages.
- An understanding of how the relational basis for Z leads to the derivation of the Z simulation rules as they are usually presented.
- 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
- Refinement in Z
- Deriving simulations in Z
- Concurrent models of refinement
- Unifying relational and concurrent refinement