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

Formal Description of Software Dynamic Correctness

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

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

出　　处：《计算机研究与发展》2013年第3期626-635,共10页Journal of Computer Research and Development

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

摘　　要：软件正确性是一个逐渐改进的过程.通过不断地修改,软件越来越接近于正确.同时软件的执行依赖于环境.为了刻画软件的动态正确性并考虑环境的因素,以参数化互模拟为基础,利用极限的观点,建立软件动态正确性的形式化描述.首先建立参数化互模拟的无限演化理论,给出参数化极限互模拟的定义,并给出几个特殊的参数化极限互模拟实例.其次,建立参数化互模拟极限,给出参数化互模拟极限的规约刻画.最后,证明参数化互模拟极限的唯一性、与参数化互模拟的相容性等代数性质.Correctness is a key attribute of software trustworthiness. Abstractly, software correctness can be represented as whether or not the implementation of software satisfies its specification. However, in the real world, it is difficult to get the satisfaction absolutely. In the course of developing and designing software, implementation is often modified in order to satisfy its specification. This means that the software is more and more close to correctness, i. e. software correctness is a dynamic course. In order to describe the dynamic correctness of software, in this paper, the abstract characterization and the limit theory of dynamic correctness based on parameterized bisimulation are proposed. Firstly, the infinite evolution mechanism of parameterized bisimulation is established. Parameterized limit bisimulation is defined in order to characterize the relation between a series of software implementations obtained in the real design and its specification, and some special examples are shown. Secondly, parameterized bisimulation limit is given, and the recursive characterization of parameterized bisimulation limit is stated. Finally, some algebraic properties are proved, such as the uniqueness of parameterized bisimulation limit and the consistence between parameterized bisimulation limit and parameterized bisimulation.

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

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