Quantitative Analysis of Software Approximate Correctness

Parameterized bisimulation provides an abstract description of software correctness. In real world situations, however, many software products are approximately correct. To characterize the approximate correctness, we generalize the parameterized bisimulation to numerical version and probabilistic setting. First, we propose the definition of the parameterized bisimulation index that expresses the degree to which a binary relation is parameterized bisimulation. Then, -parameterized bisimulation over environment and its substitutivity laws are presented. Finally, -parameterized probabilistic bisimulation is established to describe complicated software products with probabilistic phenomena.