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

• 作者: 李阳 胡斌 高济
• 来源期刊: 浙江大学学报（工学版）
• 学科: 工学
• 关键词: 形式验证 符号模型检验 跨域协作
• 年，卷（期）: 2011,（9）
• 所属期刊栏目: 计算机技术、电信技术
• 页码范围: 1558-1565,1635
• 页数: 9页
• 分类号: TP182
• 语种: 中文
• DOI: 10.3785/j.issn.1008-973X.2011.09.008

摘要

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