论文部分内容阅读
软件是信息基础设施的灵魂.随着软件规模的日趋庞大,软件的可信性越来越引起人们的关注.可信软件基础研究已经成为国内外研究的一个热点,软件可信性度量的研究是其中一个重要研究内容.软件可信性度量的研究,需要有合适的度量方法,以形式化理论为基础建立软件的可信性度量理论与模型,从而给出对软件可信性的评价,使其能成为反映软件品质及其产品竞争力的一个重要指标.另一方面,在开放的网络环境下,软件系统的可信性受到了更大的挑战,软件系统的降级替换是研究提高其可信性的方法之一而保证降级替换的正确性、评价降级替换的可信程度等问题也将是软件可信性度量研究的重要内容.本文基于语言对软件系统的可信性进行形式化刻画和度量,主要的贡献可以概括为以下几方面：■理论：(1)随机-混成进程代数(Stochastic-Hybrid CSP,S-HCSP)可信性量化理论.将随机因素引入HCSP,得到修改后的语言称为S-HCSP.基于S-HCSP,先对其原子构造形式化地定义可信度,再利用经济学的木桶原理和太极图的阴阳转化平衡原理等对其算子定义可信度计算规则,从而建立S-HCSP的可信性量化理论；(2)概率拟Hoare逻辑(Probabilistic Quasi-Hoare Logic,PQHL)可信性量化理论.在Hoare逻辑(Hoare Logic,HL)的基础上提出PQHL,用于刻画程序的可信度,定量地描述理论与程序实际执行之间的差距,反映理论被程序实现的程度,从而量化理论上正确的程序在实际执行时出错的可能性以及解释可信度很高两个程序(或是构件)的串行复合之后可信度可能并不高等问题.证明了一种特殊概率拟Hoare逻辑—[α1,α2]1-拟Hoare逻辑的可靠性,并进一步分析了PQHL的思想背景及其与Hoare逻辑之间的关系；(3)Web服务降级替换可信性量化理论.在原有进程代数基础上添加超时处理算子和延时处理算子,从而给出了Web服务降级替换的一致性条件,保证了Web服务降级替换的合成正确性,进一步研究了Web服务降级替换的可信程度,建立了Web服务降级替换的可信性量化理论.■应用：(1)将建立S-HCSP可信性量化理论的组合分析方法应用到基于语言的软件以及Web服务可信性度量的研究,分别建立了基于结构化程序设计语言的软件可信性度量模型和基于BPEL(Business Process Execution Language)的Web服务可信性度量模型；(2)将PQHL应用到基于构件的软件可信性度量的研究.以PQHL为理论基础,提出一种通过比较需求前置、后置与构件前置、后置之间差别来评价构件对需求实现程度的近似匹配度量方法.然后,通过复用构件之间的约束关系(顺序组装、选择组装和重复组装),建立基于构件的软件可信性度量模型.■工具：以基于结构化程序设计语言的软件可信性度量模型为基础,利用Ruby/Tk开发了一个软件可信性度量的工具—软件可信性度量可视化工具(Software Trustworthiness Measurement Visual Tool, STMVT)通过STMVT可以对源代码(如,C代码)进行分析,从而计算程序的可信度,并给出程序抽象可信度的可视化、程序的可信度波动曲线等等.STMVT可以为软件的可信性评估提供参考,并有助于改进软件的可信性.同时,它也说明了本文所给的理论、方法和模型的实际可行性.综上所述,本文基于语言来建立软件系统的可信性度量理论,并将建立的理论及其相关方法应用到具体软件和Web服务可信性度量的研究,还开发了相关的可信性度量工且STMVT.