期刊文献+

Probabilistic Model of Software Approximate Correctness

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. 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.
出处 《Wuhan University Journal of Natural Sciences》 CAS CSCD 2016年第1期47-55,共9页 武汉大学学报(自然科学英文版)
基金 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
关键词 METRIC INTERACTION environment process calculus probabilistic bisimulation metric interaction environment process calculus probabilistic bisimulation
  • 相关文献

参考文献23

  • 1Hoare C A R. Communicating sequential processes [J]. Communications oftheACM, 1978, 21: 666-677.
  • 2Hoare C A R. Communicating Sequential Processes [M]. Boston: Prentice Hall, 1985.
  • 3Milner R. Communication and Concurrency [M]. Boston: Prentice Hall, 1989.
  • 4Larsen K G. Context-Dependent Bisimulation between Process [M]. Edinburgh: University of Edinburgh, 1986.
  • 5Segala R, Lynch N. Probabilistic simulations for probabilistic processes [C] //Proc 5th International Conference on Concurrency Theory. Berlin, Heidelberg: Springer-Verlag, 1994: 481-496.
  • 6Deng Y X, Glabbeek R J, Hennessy M, et al. Testing finitary probabilistic processes [C] //Proc 20th International Conference on Concurrency Theory. Amsterdam: Elsevier, 2009: 274-288.
  • 7Song L, Deng Y X, Cai X J. Towards automatic measurement of probabilistic processes [C] //Proc 7th International Conference on Quality Software. San Jose : IEEE Press, 2007: 50-59.
  • 8Glabbeek R J, Smolka S A, Steffen B. Reactive, generative, and stratified models of probabilistic processes [J]. Infromation and Computation, 1995, 121(1): 59-80.
  • 9Larsen K G, Skou A. Bisimulation through probabilistic testing [J]. Information and Computation, 1991, 94(1): 1-28.
  • 10Larsen K G, Skou A. Compositional verification of probabilistic processes [C] //Proc 3th International Con- ference on Concurrency Theory. Berlin, Heidelberg: Springer- Verlag, 1992: 46-471.

二级参考文献23

  • 1Baeten J C, Weijland W P. Process Algebra. New York, USA: Cambridge University Press, 1990.
  • 2Hoare C A R. Communicating sequential processes. Commu- nications of the ACM, 1978, 21(8): 666-677.
  • 3Hoare C A R. Communicating Sequential Processes. New Jersey, USA: Prentice Hall, 1985.
  • 4Milner R. Communication and Concurrency. New Jersey, USA: Prentice-Hall, 1989.
  • 5Ying M S, Wirshing M. Approximate bisimilarity. In Proc. the 8th International Conference of Algebraic Methodology and Software Technology, May 2000, pp.309-322.
  • 6Ying M S. Bisimulation indexes and their applications. The- oretical Computer Science, 2002, 275(1/2): 1-68.
  • 7Ying M S. Topology in Process Calculus: Approximate Cor- rectness and Infinite Evolution of Concurrency Programs. New York: Springer-Verlag, 2001.
  • 8Segala R, Lynch N. Probabilistic simulations for probabilis- tie processes. In Proe. the 5th International Conference on Concurrency Theory, August 1994, pp.481-496.
  • 9Deng Y X, van Glabbeek R, Hennessy M, Morgan C. Testing finitary probabilistic processes. In Proc. the 20th Interna- tional Conference on Concurrency Theory, September 2009, pp.274-288.
  • 10Song L, Deng Y X,Cai X J. Towards automatic measurement of probabilistic processes. In Proc. the 7th International Con- ference on Quality Software, Oct. 2007, pp.50-59.

共引文献3

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部