软件的近似正确及与环境交互度量模型研究.pdf

摘 要 随着软件系统的日趋庞大和复杂，软件可信性问题越来越得到人们的关注．软件的 可信性是在软件的正确性、可靠性、安全性等众多属性基础上发展起来的一个新概念． 而正确性是软件可信研究中一个重要的内容，其主要体现在软件执行结果能否符合人们 软件实现都是其规范的近似实现，实现与规范之间的近似程度直接影响着软件的正确程 度，这是软件的近似正确问题．另一方面，软件的运行依赖于环境，有些软件在一些环境 下运行是正确的，而在另一些环境下运行未必是正确的，所以在考虑软件的正确性时需 要考虑运行环境的因素，这种因素主要体现在软件与环境的交互，软件与环境在多大程 度上交互对软件的正确性有着很大的影响，这是软件与环境的交互问题． 从软件实现来看，软件的近似正确问题可以分为动态和静态两类：其动态性体现在， 人们可以不断地修改实现使其越来越满足其规范，进而软件是越来越接近于正确；静态 近似性表现为，给定的软件实现与其规范之间允许存在一定的误差，此时软件是近似正 确的．而软件与环境的交互问题可以从软件接受环境和拒绝环境两个方面来考察． 本文主要基于进程代数理论中的CCS模型对软件的近似正确性和软件与环境的交互 性进行形式化描述和度量．主要贡献可以概括为以下内容： 一、软件的近似正确性 1．在动态近似方面．从拓扑学中网收敛的观点来看，软件实现的不断修改过程构成 一个拓扑网，并且收敛于软件规范．本文以K．G．Larsen提出的参数化互模拟和三分之二 互模拟理论为基础，分别从软件接受环境和拒绝环境角度考察这种收敛性．首先给出参 数化互模拟和三分之二互模拟的无限演化理论，并建立其拓扑结构，如子网闭包、尾闭 包、自然延拓和复合等．其次，提出参数化互模拟极限和三分之二互模拟极限的概念，表 明极限的唯一性及其与参数化互模拟和三分之二互模拟的相容性等性质．最后，证明这 两个极限都产生一个收敛类，并且可以构造相应的拓扑，称为参数化互模拟拓扑和三分 之二互模拟拓扑，这两个拓扑有利于从数学角度更好地理解和分析软件的动态近似特征． 2．在静态近似方面．利用拓扑学中的度量理论，从软件拒绝环境的角度，建立软件 实现与其规范之间近似程度的度量模型．首先提出三分之二互模拟索弓l(index)及A一三 分之二互模拟等价的概念．其次，构造一个模态逻辑语言，给出该语言的语义模型，建 立入一三分之二互模拟等价的模态逻辑刻画：两个进程是A一三分之二互模拟等价当且仅 当他们满足相同的模态逻辑公式．最后，讨论A一三分之二互模拟关于进程算子的拟同余 性(pre．congruence)，并在此基础上建立实现与规范之间近似程度的度量模型． 二、软件与环境的交互性 从接受环境角度，建立软件与环境交互程度的度量模型． 1．把软件抽象为进程，利用经典进程的完整迹语义，建立三种度量模型：{o，1)- 模型、[0，1卜模型及[o，1协模型．基于这些度量给出进程集合和环境集合上的加 细(refinement)关系，这些加细关系在一定程度上给出评价软件和环境的标准． 2．把软件抽象为概率进程，提出概率进程的完整概率迹语义，并在此基础上建立概 率进程与环境交互的度量模型：p7{o，1)·模型、p’[o，1卜模型及p7[o，1睁模型．基于这些度量 给出概率进程集合上的加细关系．同时，为了描述软件在近似环境下的运行效果，建立软 件与近似环境交互度量的估计模型． 综上所述，本文根据进程代数理论，建立软件实现与其规范之间的动态近似性和静 态近似性的形式化描述，并给出静态近似的度量模型．同时建立软件与环境交互的度量 刻画，根据这些度量模型，给出评价软件和环境的标准，并进一步建立软件与近似环境交 互度量的估计模型． 关键词：软件实现；软件规范；进程代数(Ccs)；概率进程代数；参数化互模拟；三分之 二互模拟；完整迹；度量；拓扑 ll Abstract forsoftware correctness isa attribution Correctness key canbe thatits the ofasoftware