Using Coupled Simulations in Non-atomic Refinement

摘要: Refinement is one of the most important techniques in formal system design, supporting stepwise development systems from abstract specifications into more concrete implementations. Nonatomic refinement employed when level granularity changes during a step, i.e., whenever an operation refined sequence operations, as opposed to single operation. There has been some limited work on non-atomic Z, and purpose this paper extend existing theory. In particular, we strengthen proposed definition exclude certain behaviours which only occur specification but have no counterpart level. To do use coupled simulations: standard simulation relation complemented by second guarantees exclusion undesired behaviour system. These two relations agree at specific points (coupling condition), thus ensuring desired close correspondence between specification.