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

从软件系统的可靠性和安全性需求出发，研究基于无界模型检测技术的业务特征交互检测方法。本项目将把软件系统形式化建模为多智能体系统Kripke模型。为了便于在基系统中灵活地集成各种业务特征，本项目将设计基系统描述语言和业务特征描述语言，然后设计算法将这两种语言自动集成为新系统的描述语言。该语言用于产生多智能体系统Kripke语义模型。本项目将在该语义模型上提出基于CTL*的时态认知逻辑及其语义框架，最后设计基于SAT技术的无界模型检测算法，实现相关模型检测工具并用之于一些典型软件系统的业务特征交互检测。