Refinement Relations on Partial Specifications
Shiva Nejati · TSpace (University of Toronto) · 2003
We discuss the problem of refining partial specifications of software systems at different levels of abstraction. In general, refinement is the process of deriving an implementation from a specification and verifying the correctness of the derivation. Recently, partial specifications have been advocated for describing software systems mainly because they do not impose a commitment to all decisions made at initial stages of software development life-cycle. Using finite-state transition systems with partial transitions and propositions as our modeling formalism, we define a refinement relation that is insensitive to finite stuttering. We refer to our proposed refinement relation as stuttering refinement relation. We then present a logical characterization of this refinement relation and describe an algorithm for computing it.