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

The formal description of software correctness based on the environment

作　　者：马艳芳[1] 张敏[2,3] 陈仪香[2,3] 

机构地区：[1]淮北师范大学计算机科学与技术学院,安徽淮北235000 [2]华东师范大学软件学院,上海200062 [3]上海市高可信计算重点实验室,上海200062

出　　处：《山东大学学报（理学版）》2011年第9期22-27,共6页Journal of Shandong University(Natural Science)

基　　金：国家自然科学基金项目(90718013);国家高技术研究发展计划(863计划)资助项目(2007AA01Z189);安徽省高等学校省级自然科学研究重点项目(KJ2011A248);上海市高可信计算重点实验室开放课题研究项目

摘　　要：软件的运行依赖于环境,在考察软件正确性时需要考虑环境的因素。软件在开发和设计过程中,其正确性是一个逐渐改进的过程,也就是说,通过不断地修改,软件越来越接近于正确。为了刻画软件的这种动态正确性并考虑环境的因素,本文将以三分之二互模拟为基础,利用网极限的观点,建立软件动态正确性的形式化描述。首先建立三分之二互模拟的无限演化理论,给出三分之二极限互模拟的定义。其次建立三分之二互模拟极限,这个极限在一定程度上反映软件规范是其实现的极限形式。最后证明三分之二互模拟极限与三分之二互模拟的相容性等性质。Correctness is a key attribution for software trustworthiness.Abstractly,it can be represented by whether or not the implementations of the software satisfy its specification.Also,the correctness is related to its execution environment.On the other hand,the correctness is a course of modifying implementation,i.e.,the software is closer and closer to correctness.In order to describe the dynamic correctness of software,the abstract characterization of dynamic correctness is proposed based on two-third bi-simulation.First,two-thirds limit bi-simulation is defined which reflects the course of modification implementation.Second,the two-third bi-simulation limit is presented which means that the specification of the software is the limit of its implementations.Finally,some algebraic properties are proved.

关 键 词：极限 三分之二互模拟 正确性 形式化 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]