Probabilistic Model of Software Approximate Correctness

摘要

Correctness is a key attribute of software. Parameterized bisimulation provides a kind of abstract description to verify the correctness of software under environment. In real world situations, many softwares contain some probabilistic information. In this paper, we focus on the probabilistic construction of parameterized bisimulation. Firstly, we extend parameterized bisimulation to probabilistic parameterized bisimulation. Secondly, a quantitative model of approximate correctness of software is proposed. Finally, the subsititutivity laws of quantitative model with various combinators are proved.