一个命题投影时序逻辑符号模型检测器

• 作 者: 逢涛 段振华 刘晓芳
• 机 构: 西安电子科技大学计算理论与技术研究所,综合业务网理论与关键技术国家重点实验室（西安电子科技大学）
• 出 处: 软件学报
• 发表日期: 2015年8期
• 关键词: 符号模型检测 时序逻辑 模型检测器 嵌入式系统验证 symbolic model checking temporal logic model checker
• 基金项目: 国家自然科学基金（61133001,61202038,61272117,61272118,61322202）,国家重点基础研究发展计划（973）（2010CB328102）

现有模型检测工具的形式化规范语言，如计算树逻辑（computation tree logic，简称CTL）和线性时序逻辑（linear temporal logic，简称LTLl等的描述能力不足，无法验证ω正则性质．提出了一个命题投影时序逻辑（propositional projection temporal logic,简称PPTL）符号模型检测工具——PLSMC（PPTL symbolic model checker）的设计与实现过程．该工具基于著名的符号模型检测系统NuSMV,实现了PPTL的符号模