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.