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

摘要：

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

关键词：可信性、正确性、形式化、进程代数

所属期刊栏目：49

分类号：O159;TP301(代数、数论、组合理论)

资助基金：安徽省自然科学基金1308085QF117;安徽高校省级自然科学研究重点项目KJ2011A248;安徽高校省级自然科学研究一般项目KJ2012Z347;上海市高可信计算重点实验室开放项目07DZ22304201004

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

页数：共6页

页码：15-19,60