软件动态正确性的形式化描述

摘要：

软件正确性是一个逐渐改进的过程.通过不断地修改,软件越来越接近于正确.同时软件的执行依赖于环境.为了刻画软件的动态正确性并考虑环境的因素,以参数化互模拟为基础,利用极限的观点,建立软件动态正确性的形式化描述.首先建立参数化互模拟的无限演化理论,给出参数化极限互模拟的定义,并给出几个特殊的参数化极限互模拟实例.其次,建立参数化互模拟极限,给出参数化互模拟极限的规约刻画.最后,证明参数化互模拟极限的唯一性、与参数化互模拟的相容性等代数性质.

关键词：软件正确性、参数化互模拟、形式化、极限、拓扑

所属期刊栏目：50

分类号：TP301.2(计算技术、计算机技术)

资助基金：国家自然科学基金项目91118007;中央高校基本科研业务费专项基金项目78210045;安徽省高等学校省级自然科学研究项目KJ2011A248,KJ2012Z347;上海市高可信计算重点实验室开放课题项目07dz22304201004;安徽省淮北师范大学青年科学基金项目700583

在线出版日期：2013-04-27（万方平台首次上网日期，不代表论文的发表时间）

页数：共10页

页码：626-635