The Approximate Correctness of Systems Based on δ-bisimulation

摘要

The correctness of system is an important attribute to quantify the quality. δ -bisimulation based on complete lattices have been proposed to generalize the classical bisimulation. To analyze the implementations of system approximates its specification step by step, the infinite evolution mechanism of δ -bisimulation is established. Firstly, the relations between the implementations and specification under δ -bisimulation are analyzed, δ -limit bisimulation is defined and some examples of δ -limit bisimulations are given. Then, δ -bisimulation limit is proposed to state the specification is the limit of implementations. Some algebraical properties of δ -bisimulation limit are proved. Finally, in order to use the flexible hierarchic development and modular design methods to archive the limit, the continuous of δ -bisimulation limit under various combinators are showed.