Model of software approximate correctness under ε-bisimulation

Computer Engineering and Applications ›› 2013, Vol. 49 ›› Issue (11): 15-19.

Previous Articles Next Articles

Model of software approximate correctness under ε-bisimulation

MA Yanfang1，2, CHEN Liang3

1.School of Computer Science and Technology, Huaibei Normal University, Huaibei, Anhui 235000, China
2.Shanghai Key Laboratory of Trustworthy Computing, Shanghai 200062, China
3.School of Mathematical Sciences, Huaibei Normal University, Huaibei, Anhui 235000, China

Online:2013-06-01 Published:2013-06-14

基于ε-互模拟的软件近似正确性模型

马艳芳1，2，陈亮3

1.淮北师范大学计算机科学与技术学院，安徽淮北 235000
2.上海市高可信计算重点实验室，上海 200062
3.淮北师范大学数学科学学院，安徽淮北 235000

Abstract

Abstract: The correctness of software is a key attribution for trustworthiness of software. In the real development and design, the software is modified constantly in order to get correctness, and the software is correct more and more. This paper focuses on the dynamic characterization of correctness. Based on ε-bisimulation of probabilistic process algebra, ε-limit bisimulation is defined which reflects the relation between implementation and its specification, and some special ε-limit bisimulations are showed. ε-bisimulation limit is presented, which states that specification is the limit of implementations. Some important pro-perties are proved.

Key words: trustworthiness, correctness, formalization, process algebra

摘要： 软件正确性是软件可信性的重要属性。在实际软件开发和设计中，需要不断地对软件进行修改，从而软件越来越正确。为了讨论软件的动态近似正确性，基于概率进程代数的ε-互模拟，建立软件越来越正确的形式化描述。定义ε-极限互模拟，用来反应软件实现与规范之间的关系，给出一些特殊的ε-极限互模拟。提出ε-互模拟极限，用其刻画规范是软件实现的极限形式，同时证明ε-互模拟极限的一些性质。

关键词: 可信性, 正确性, 形式化, 进程代数

MA Yanfang1，2, CHEN Liang3. Model of software approximate correctness under ε-bisimulation[J]. Computer Engineering and Applications, 2013, 49(11): 15-19.

马艳芳1，2，陈亮3. 基于ε-互模拟的软件近似正确性模型[J]. 计算机工程与应用, 2013, 49(11): 15-19.

[1]	CHAI Lei, WANG Zhixue, HE Ming. Formal Framework of Command Control Cooperative Capability Requirements System-of-Systems [J]. Computer Engineering and Applications, 2020, 56(5): 49-56.
[2]	BAI Chuan1, ZHANG Xuan1，2, WANG Xu3, KANG Yanni1. Economic method analysis to non-functional requirements of trustworthiness software [J]. Computer Engineering and Applications, 2017, 53(22): 249-257.
[3]	WEN Xingzi1, LIU Youjin1, OUYANG Junlin2. Simulating software trustworthiness evolution based on moving cellular automata [J]. Computer Engineering and Applications, 2015, 51(7): 12-17.
[4]	FENG Lulu, DING Zuohua. Study to improve coverage-based fault localization based on discovery of coincidental correctness test cases [J]. Computer Engineering and Applications, 2015, 51(22): 252-257.
[5]	ZHANG Jin1，2, LIU Manxia2, ZHAO Erqun2, LIU Junfei3. Software partial correctness verification based on XYZ/SE [J]. Computer Engineering and Applications, 2015, 51(14): 46-50.
[6]	MA Yanfang1，2, CHEN Liang3. Approximate measure model of software based on partial interaction [J]. Computer Engineering and Applications, 2014, 50(24): 32-37.
[7]	XIE Guozhen, MA Xiaoxing. Logical validity in dynamic updating of C programs [J]. Computer Engineering and Applications, 2013, 49(14): 39-44.
[8]	LIU Guanghui. DoubleRun：using temporal redundancy to insure the reliability of processors [J]. Computer Engineering and Applications, 2011, 47(21): 17-22.
[9]	LI Hong1，2，MA Xiaoping1. Research on feature and formal representation of granule [J]. Computer Engineering and Applications, 2011, 47(11): 3-6.
[10]	SONG Pei-yan，LIU Ning-jing. Multi-levels model for G-anaphora disambiguation between sentences [J]. Computer Engineering and Applications, 2010, 46(5): 24-27.
[11]	YANG Yi，WANG Li-ming. Research on multi-Agent interaction protocols based on RASA [J]. Computer Engineering and Applications, 2010, 46(28): 232-235.
[12]	TANG Yong-xin¹，LIU Zeng-liang². Progress in software trustworthiness metrics models [J]. Computer Engineering and Applications, 2010, 46(27): 12-16.
[13]	LI Sheng-hong. Modeling interaction based information alignment of Web choreography [J]. Computer Engineering and Applications, 2010, 46(2): 11-13.
[14]	XU Jin-bao¹，LIAO Lei¹，YE Qiao-lin². Least squares support vector machine classifiers with guaranteed classification performance [J]. Computer Engineering and Applications, 2009, 45(21): 48-50.
[15]	WANG Qin,GUO Ya-Jun,XU Fen. Fuzzy logic-based trust evaluation model in pervasive computing environment [J]. Computer Engineering and Applications, 2008, 44(3): 170-172.

Model of software approximate correctness under ε-bisimulation

基于ε-互模拟的软件近似正确性模型

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics