基于APTL的开放系统模型检测

随着国民经济、国防建设和人民生活日益增长的需求以及互联网技术的发展，开放环境下的软件系统已成为重要的软件系统。与封闭系统相比较，开放系统与环境不断地交互，系统的行为随环境的变化而变化，并且系统的行为影响着环境的变化。如何保障开放软件系统的可信性，是可信软件领域面临的一个新的挑战。本项目研究基于交互式投影时序逻辑APTL的开放系统模型检测理论与方法。在现有的投影时序逻辑PTL的基础上，通过将时序操作符扩展到Agent相关的时序操作符，建立基于并发博弈结构的APTL模型，包括该逻辑的语法、语义以及逻辑规则，并研究APTL的可判定性；建立基于并发博弈结构的自动机模型ACG，研究ACG的判空、求交等算法；研究基于ACG的APTL模型检测算法，以及相应的状态空间缩减技术，并开发相应的模型检测支持工具。以分布式软件系统为示范，研究基于APTL的模型检测在开放系统中的应用。

本项目解决了命题投影时序逻辑（PPTL）的表达性问题，证明PPTL具有完全正则表达能力，并给出了PPTL的5个子集的刻画；改进了PPTL的判定算法；建立了命题投影时序逻辑（PPTL）的公理系统；基于投影操作建立了柱面计算模型；提出了基于Agent的交互式投影时序逻辑APTL系统；定义了基于并发博弈结构的自动机模型；给出了基于APTL的开放软件系统模型检测算法；通过引入新的布尔变量将抽象模型精化问题归结到多项式问题，从而避免了原有抽象精化中的NP完全问题，而且还可以得到更小的精化模型；提出了线性的虚假路径检测算法。在项目的资助下，课题组共发表论文48篇，其中国际期刊论文9篇（SCI收录），英文专著章节1篇，重要国际会议论文28篇，国内重要期刊论文11篇，申请专利22项，获软件著作权5项。组织国际会议TASE 2011，合办国际研讨会WSFOL 2012，参加国际会议/研讨会10余次。