Skip to main content
PRL Project

Principles of Stepwise Refinement

by Heiko Mantel


In order to verify complex systems against their requirements one needs intermediate levels of abstraction. This can be achieved best by deriving a system formally by stepwise refinement. Starting from the requirements, at each step one constructs a more concrete description of the system and verifies it against the specification constructed in the previous step until one arrives at the implementation. The focus of my talk is on the question what refinement means formally. Various refinement concepts have been proposed in the literature. I will identify basic principles which are common to many of the existing refinement concepts. The running example will be a well-known refinement concept which assumes that systems are modeled by sets of traces.