The Quantitative Analysis of Approximate Correctness for Real-Time Systems

In order to formalize the correctness of real-time systems, strong timed bisimulation in TCCS has been proposed to characterize the relation between implementation and specification.The usual action and time delay must be the same in strong timed bisimulation.However, in some real situations, many real-timed systems can not satisfy the exact match.In this paper, in order to characterize the approximate usual action and time delay, the strong timed bisimulation in TCCS is generalized to numerical version.Firstly, the definition of global timed bisimulation index of a binary relation is established to describe the relation between implementation and specification.Secondly, in order to quantify the approximate degree between implementation and specification, the global timed λ -bisimulation is defined.Finally, the congruence of the global timed λ -bisimulation is proven to guarantee the modular development and hierarchic design methods which are used in the real software development.