可信网络软件的形式验证

以网络软件为研究对象，针对软件可信性质中的正确性和安全性，研究确保软件行为一致性和安全性验证的理论和方法。主要包括：研究网络软件的形式化行为建模与安全建模方法和自动抽取模型的方法、从整体功能层面和交互行为层面对网络软件进行行为建模的方法、威胁驱动的网络软件的形式化安全建模方法、Web应用的on-the-fly导航建模方法；研究自动生成一致性和安全行性质的方法、组合式的抽象精化验证方法与技术；采用模型检验和定理证明结合的方法和技术验证网络软件的行为一致性和安全性；应用监控理论的可控制性原理对构件式系统进行安全性质的验证。研究符号模型检测、限界模型检测、偏序规约模型检测和组合模型检测的理论。开发支持工具。该项研究对于提高网络软件的可信性和质量有重大意义。研究成果可以广泛应用到网络软件的开发过程中。

以网络软件为研究对象，针对软件可信性质中的正确性和安全性，研究了确保软件行为一致性和安全性验证的理论和方法。提出了一种基于On-the-fly的Web导航行为建模方法和威胁驱动的Web应用On-The-Fly导航模型的验证方法，采用威胁驱动方法设计和抽取用于性质检验的安全性质，对交互的Web应用建模并验证给定的安全性质；基于模糊集的相关理论给出了服务流程可信性的运算法则、量化服务流程的可信性和相似服务流程的概念；提出了一种验证带有时间约束的Web服务的方法。引入了一种被称为WS时间自动机的形式化技术，以捕获Web服务应用的时间行为。在深入分析用户和Web浏览器交互行为的基础上，引入On-the-fly 策略并采用反例引导的抽象精化验证方法对网络软件的导航行为进行建模和验证。为了对Web服务组合建模，提出一个基于马尔可夫决策过程的Web服务概率行为模型。为了对Web服务组合检验，通过状态商的概率等价关系进行抽象。基于反例引导的思想，迭代地进行抽象精化过程直到不再出现反例或反例被证实为真；用概率时间计算树逻辑PTCTL公式描述错误侦测能力和错误容忍能力的性质，在概率模型检验器PRISM上执行验证并输出定量检验结果。将概率度量理念引入到经典的Petri网模型，找出Petri网系统与概率空间的对应关系，给出了其相应的变迁触发规则和结构特征。提出了一种非确定概率Petri网模型NPPN (nondeterministic probabilistic Petri net)系统，它可用于对带有概率和非确定性的系统的行为进行定性和定量的建模和验证。对形式规格说明语言Z与相应定理证明方法及其应用进行研究。此外，给出了基于模型验证的测试用例生成方法。开发了支持工具。该项研究对于提高网络软件的可信性和质量有重大意义。研究成果可以广泛应用到网络软件的开发过程中。. 课题组在本项目研究期间，积极开展了与国内外同行的学术交流，培养了多名博士和硕士研究生。