Refinement and state machine abstraction
Precise module interface specifications are essential in modular software development. The role of state in these specifications has been the issue of some debate and is central to the notion of data refinement. In previous work, Hoffman and Strooper introduce a state-abstraction lattice that defines a partial order on specifications for deterministic and complete languages. They use this lattice to define a notion of state abstractness and show that this intuitive notion corresponds to the use of the terms "abstract" and "concrete" as used in data-refinement proofs. In this paper, we extend this work for a class of specifications and languages that we call demonic and semi-deterministic. We also introduce a notion of backward refinement and prove that backward refinement together with the common forward refinement of VDM and Z form a sound and complete refinement technique with respect to a partial order on languages defined by demonic specifications. We illustrate the ideas using simple languages and specifications. (C) 2001 Elsevier Science B.V. All rights reserved.
refinement state machine abstraction specification modular software development formal methods