摘要
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.
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.
基金
Supported by the National Natural Science Foundation of China(61300048)
the Anhui Provincial Natural Science Foundation(1308085QF117,1508085MA14)
the Key Natural Science Foundation of Universities of Anhui Province(KJ2014A003,KJ2014A223)
the Major Teaching Reform Project of Anhui Higher Education Revitalization Plan(2014ZDJY058)
the Excellent Young Talents in Universities of Anhui Province