The Evolution Mechanism of Correctness for Cyber-Physical System

Cyber-physical Systems (CPS) are widely used in all areas of life. Ensuring the correctness of CPS remains an enduring challenge during its development and design phases. One approach to ascertain the correctness of CPS is behavior equivalence based on bisimulation. However, whether the implementation development process develops in the right direction has an important impact on obtaining the correct system implementation. Especially, the development process of complex CPS often yields a multitude of implementation versions, the correlation among these versions partly signifies the correctness of the development process. This paper formalizes the relationship between the implementation versions and establishes a formal description of the development process progressing in the correct direction, leveraging the concept of a "limit idea." Initially, we introduce the concept of "limit bisimulation" for CPS systems to delineate implementations acquired during the CPS development process. Specific limit bisimulations are demonstrated to represent distinct scenarios within the development process. Subsequently, the convergence mechanism of implementations is modeled through bisimulation limits, encapsulating the CPS's specification as the ultimate goal of obtained implementations during the development process. Finally, the congruence property of the bisimulation limit is proved, which accounts for the relation between specification and implementation versions can be decomposed into a refinement hierarchy. The limit theorem of bisimulation in CPS can help the designer and developer of CPS to comprehend the development course better.