PSL的有界模型检验

• 作者: 虞蕾 赵宗涛
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: PSL(property, specification, language) 有界模型检验(bounded, model, checking,BMC) SAT(propositional, satisfiability) OBDD(ordered, binary, decision, diagram)
• 年，卷（期）: 2009,（3）
• 所属期刊栏目: 科研通信
• 页码范围: 614-621
• 页数: 8页
• 分类号: TP301
• 字数: 8644字
• 语种: 中文
• DOI: 10.3321/j.issn:0372-2112.2009.03.034

摘要

基于SAT的有界模型检验被视为是基于OBDD的符号化模型检验技术的重要补充,是并行反应式系统的一种有效验证方法.然而,直至现在,有界模型检验已验证的属性逻辑还十分有限.PSL是一种用于描述并行系统的属性规约语言(IEEE-1850),包括线性时序逻辑FL和分支时序逻辑OBE两部分.通过模型检验可验证系统的PSL属性,本文提出了PSL的有界模璎检验方法及其算法框架.首先,定义PSL逻辑的有界语义,而后,将有界语义进一步简化为SAT,分别将PSL性质规约公式和系统肘的状态迁移关系转换为SAT命题公式,最后验证七述两个SAT命题公式合取式的可满足性,这样就将时序逻辑PSL的存在模型检验转化为一个命题公式的可满足性问题,并用一个队列控制电路实例具体解释算法执行过程.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	赵宗涛	第二炮兵工程学院计算机系	53	570	13.0	22.0