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

J4 ›› 2011, Vol. 46 ›› Issue (9): 22-27.

• CTCIS 2011 会议 • 上一篇下一篇

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

马艳芳¹,张敏^2,3,陈仪香^2,3

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

收稿日期:2011-06-16 出版日期:2011-09-20 发布日期:2011-09-08
作者简介:马艳芳(1978- ),女,博士,讲师,主要研究方向为程序形式语义,可信度量模型. Email: yfma@sei.ecnu.edu.cn
基金资助:
国家自然科学基金项目(90718013);国家高技术研究发展计划 (863计划)资助项目(2007AA01Z189);安徽省高等学校省级自然科学研究重点项目(KJ2011A248);上海市高可信计算重点实验室开放课题研究项目

The formal description of software correctness based on environment

MA Yan-fang¹, ZHANG Min^2,3, CHEN Yi-xiang^2,3

1. School of Computer Science and Technology, Huaibei Normal University, Huaibei 235000, Anhui, Chian;
2. Institue of Theoretical Computing of East China Normal University, Shanghai 200062, China;
3. Shanghai Key Laboratory of Trustworthy Computing, Shanghai 200062, China

Received:2011-06-16 Online:2011-09-20 Published:2011-09-08

摘要/Abstract

摘要：

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

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

Abstract:

Correctness is a key attribution for software trustworthiness. Abstractly, it can be represented by whether or not the implementations of the software satisfys its specification. Meanwhile, the correctness is also related to its execution environment. On the other hand, the correctness is a course of modifying implementation, i.e., the software is more and more close to correctness. In order to describe the dynamic correctness of software, the abstract characterization of dynamic correctness is proposed based on two-third bisimulation. Firstly, two-thirds limit bi-simulation is defined which reflects the course of modification implementation. Secondly, two-third bisimulation limit is presented which means that the specification of a software is the limit of its implementations. Finally, some algebraic properties are proved.

Key words: limit; two-thirds bi-simulation; correctness; formalization

马艳芳1,张敏2,3,陈仪香2,3. 基于环境的软件正确性形式化描述[J]. J4, 2011, 46(9): 22-27.

MA Yan-fang1, ZHANG Min2,3, CHEN Yi-xiang2,3. The formal description of software correctness based on environment[J]. J4, 2011, 46(9): 22-27.

参考文献

多维度评价

Viewed

Full text

Abstract

Cited

Shared

Discussed

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

The formal description of software correctness based on environment

PDF (PC)

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 0

多维度评价

本文评价

推荐阅读 0