| PSL的有界模型检验 |
| |
| 引用本文： | 虞蕾,赵宗涛.PSL的有界模型检验[J].电子学报,2009,37(3):614-621. |
| |
| 作者姓名： | 虞蕾 赵宗涛 |
| |
| 作者单位： | 1. 国防科学技术大学计算机学院博士后流动站,湖南,长沙,410073;第二炮兵工程学院计算机系,陕西,西安,710025
2. 第二炮兵工程学院计算机系,陕西,西安,710025 |
| |
| 基金项目： | 国家高技术研究发展计划(863计划)，国家自然科学基金，中国博士后科学基金 |
| |
| 摘 要： | 基于SAT的有界模型检验被视为是基于OBDD的符号化模型检验技术的重要补充,是并行反应式系统的一种有效验证方法.然而,直至现在,有界模型检验已验证的属性逻辑还十分有限.PSL是一种用于描述并行系统的属性规约语言(IEEE-1850),包括线性时序逻辑FL和分支时序逻辑OBE两部分.通过模型检验可验证系统的PSL属性,本文提出了PSL的有界模型检验方法及其算法框架.首先,定义PSL逻辑的有界语义,而后,将有界语义进一步简化为SAT,分别将PSL性质规约公式和系统M的状态迁移关系转换为SAT命题公式,最后验证上述两个SAT命题公式合取式的可满足性,这样就将时序逻辑PSL的存在模型检验转化为一个命题公式的可满足性问题,并用一个队列控制电路实例具体解释算法执行过程.
|
| 关 键 词： | PSL(property specification language) 有界模型检验(bounded model checking BMC) SAT(propositional satisfiability) OBDD(ordered binary decision diagram) |
| 收稿时间： | 2007-01-23 |
Bounded Model Checking of PSL |
| |
| YU Lei,ZHAO Zong-tao.Bounded Model Checking of PSL[J].Acta Electronica Sinica,2009,37(3):614-621. |
| |
| Authors: | YU Lei ZHAO Zong-tao |
| |
| Affiliation: | 1.Postdoctoral Station of Computer School;National University of Defense Technology;Changsha;Hunan 410073;China;2.Department of Computer Science;Second Artillery Engineering College;Xi'an;Shaanxi 710025;China |
| |
| Abstract: | SAT-based bounded model checking(BMC) is introduced as a complementary technique to OBDD-based symbolic model checking,and is a verification method for parallel and reactive systems.However,until now the properties verified by bounded model checking are very limited.Temporal logic PSL is a property specification language(IEEE-1850) describing parallel systems and is divided into two parts,i.e.the linear time logic FL(Foundation Language)and the branch time logic OBE(Optional Branching Extension).The specifi... |
| |
| Keywords: | PSL(property specification language) model checking BMC) SAT(propositional satisfiability) OBDD(ordered binary decision diagram) |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《电子学报》浏览原始摘要信息 |
|
点击此处可从《电子学报》下载全文 |
|
