基于环境的软件正确性形式化描述

摘要：

　　软件的运行依赖于环境，在考察软件正确性时需要考虑环境的因素。软件在开发和设计过程中，其正确性是一个逐渐改进的过程，也就是说，通过不断地修改，软件越来越接近于正确。为了刻画软件的这种动态正确性并考虑环境的因素，本文将以三分之二互模拟为基础，利用网极限的观点，建立软件动态正确性的形式化描述。首先建立三分之二互模拟的无限演化理论，给出三分之二极限互模拟的定义。其次建立三分之二互模拟极限，这个极限在一定程度上反映软件规范是其实现的极限形式。最后证明三分之二互模拟极限与三分之二互模拟的相容性等性质。

关键词： 运行环境 软件规范 极限形式 进程演算

作者: 马艳芳 张敏 陈仪香

作者单位: 淮北师范大学计算机科学与技术学院，安徽淮北 235000 华东师范大学软件学院，上海 200062 上海市高可信计算重点实验室，上海 200062

会议类型: 国内会议

会议名称: 2011年第五届中国可信计算与信息安全学术会议(CTCIS2011)

会议地点: 贵阳

会议语种:中文

页码: 22-27

在线出版日期: 2011-08-01（万方平台首次上网日期，不代表论文的发表时间）