基于时态认知逻辑的特征交互无界模型检测-东篱科研大数据发现系统（DRDS）

位置：立项数据库 > 立项详情页

基于时态认知逻辑的特征交互无界模型检测

项目名称：基于时态认知逻辑的特征交互无界模型检测
项目类别：地区科学基金项目
批准号：60763004
申请代码：F0201
项目来源：国家自然科学基金
研究期限：2008-01-01-2010-12-31

项目负责人：骆翔宇
负责人职称：副教授
依托单位：桂林电子科技大学
批准年度：2007

中文摘要：

本项目将类似于电信系统的特征交互问题，推广到分布式软件系统的可信性问题。从分布式软件系统的正确性和安全性等可信需求出发，着重研究和开发了基于时态认知逻辑模型检测的Web服务组合自动验证方法和工具。根据服务的自治性和服务间的交互性特点，自然地将Web服务组合建模为多主体系统。首先提出刻画多主体系统行为的多主体形式模型，在该模型上提出基于CTL*的时态认知逻辑及其语义框架，设计并实现了基于OBDD的无界模型检测算法和工具MCTK。然后以MCTK、认知模型检测工具MCMAS和Verics、以及Spin、Uppaal和Zing模型检测工具为底层验证平台，提出了从Web服务业务流程执行语言BPEL到这些工具输入语言的转换方法，实现对Web服务组合的形式化建模，并利用各个工具的时态和认知性质验证能力对各种可信性质进行自动验证。与类似工具MCMAS和Verics相比，MCTK不仅有相同的知识验证能力，而且时态表示能力更强，效率更高。本项目还在公告逻辑模型检测、基于Competent谓词抽象和有界模型检测优化的模型检测优化技术、知识推理方法和应用扩展等方面做了进一步探索。

中文主题词：符号化模型检测；时态认知逻辑；多主体系统

结论摘要：

英文主题词symbolic model checking; temporal epistemic logic; multi-agent system

成果综合统计