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