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

基金项目类型：

国家自然科学基金

基金项目编号：

61003078

来源网站：

国家自然科学基金委员会

来源网址：

http://www.nsfc.gov.cn/

负责人：

田聪

完成单位：

西安电子科技大学

中文关键词：

时序逻辑; 开放系统; 模型检测; 表达性; 状态空间;

其他语种关键词：

Temporal Logic; Open Systems; Model Checking; Expressiveness; State Space

项目类型：

青年科学基金项目

语种：

中文

开始日期：

2011-01-01

结束日期：

2013-12-31

中文摘要：

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