基于环境交互的软件近似正确性量化模型研究

Correctness of software is an important content of software engineering research and an key attribute of software trustworthiness. Research to software correctness can supply the guarantee to improve software quality. The execution of software depends on its envirionment. The same software running on different environment will produce the different correctness. Because in the real world, many softwares are approximate correct, it is necessary to research the approximate correctness of software. This project will establish the quantitive model of software approximate correctness based on its interactive envirionment. Based on Process Algebra, the aims of this project are as follows: (1) We establish the interactive measure model between software and environment and explore its important properties, which provides a foundation for checking whether or not software executes correctly on its environment; (2) We propose the degree which to the soft implementation satisfies its specification and research its modal logic, which lays a basis for analyzing software correctness;(3)We present the degree which to the trend of software implementation improvement is in the correct direction and discuss its continuity, which provides a basis for examining the correctness of software development process.

软件工程的一项重要内容是保证软件的正确性，它是软件可信性的重要属性，因此研究软件的正确性是提高软件质量的重要保障。而软件的运行依赖于环境，同一软件在不同环境下运行时其正确性不同，因此很多软件在实际应用时都是近似正确的，其近似程度直接影响软件的正确性，因此本项目将从定量方面对基于环境的软件近似正确性进行研究。 基于进程代数理论，本项目主要研究以下内容：（一）建立软件与环境交互程度的度量描述，研究度量模型的重要性质，为验证软件的运行环境提供理论依据；（二）结合软件的运行环境，建立软件实现与其规范之间近似程度的度量模型，研究度量模型的模态逻辑刻画，为分析软件的正确程度提供理论保证；（三）建立软件实现的改进过程按正确方向发展的度量模型，探讨度量模型的连续性，为检验软件开发过程的正确性提供理论基础。

软件正确性是提高软件质量的重要保证，而软件运行依赖环境，在考察软件正确性时需要考虑环境的因素。本项目提出软件与环境的交互度量理论，从定量和定性两个方面建立了软件近似正确性模型，其研究成果具有重要的理论意义和一定的应用价值。经过三年的研究，我们得到了以下四部分的研究成果：（一）建立软件与环境交互程度的度量模型，研究度量模型的重要性质，为验证软件的运行环境提供理论依据；（二）结合软件的运行环境，建立软件实现与其规范之间近似程度的度量模型， 同时得到了概率和模糊系统近似正确性模型。 这些模型为分析软件的正确程度提供理论保证;（三）建立软件实现的改进过程按正确方向发展的形式化模型，为检验软件开发过程的正确性提供理论基础；（四）结合度量模型，通过数学建模以及离散化，得到了一系列的非线性问题，从数值代数和最优化两个方面研究大规模非线性方程组的数值算法，为度量模型的应用提供理论依据。