基于符号模型检验的可信跨域协作系统验证方法 (2011年)

针对规范调控的可信跨域协作系统属性验证的困难，提出一种基于符号模型检验的可信跨越协作系统验证方案.该方案包括规范语法及其状态语义、系统抽象模型、验证算法三大部分。其中规范的状态语义是方案的核心，它将规范集映射为其所对应的状态或状态转移集，消除了系统模型和规范的语义不一致性；系统抽象模型包括规范Kripke结构和路径规范性定义，以及规范Kripke结构的分支时态逻辑（CTL）语义3个部分，实现了可信系统的形式建模；验证算法描述了系统符号模型检验的具体实现过程.与基于定理证明的验证方案相比，该方案有效降低了验