计算机工程与应用 ›› 2008, Vol. 44 ›› Issue (27): 46-48.DOI: 10.3778/j.issn.1002-8331.2008.27.015

• 理论研究 • 上一篇    下一篇

基于吴方法的符号模型检验

曾 琼1,黄 健2,3,魏 乐2,3   

  1. 1.成都信息工程学院 计算机基础教学部,成都 610103
    2.成都信息工程学院 计算机系,成都 610103
    3.电子科技大学 计算机系,成都 610054
  • 收稿日期:2007-11-13 修回日期:2008-02-18 出版日期:2008-09-21 发布日期:2008-09-21
  • 通讯作者: 曾 琼

Symbolic model checking based on Wu’s method

ZENG Qiong1,HUANG Jian2,3,WEI Le2,3   

  1. 1.Department of Computer Foundation Studies,Chengdu University of Information Technology,Chengdu 610103,China
    2.Department of Computer,Chengdu University of Information Technology,Chengdu 610103,China
    3.Department of Computer,University of Electronic Science and Technology of China,Chengdu 610054,China
  • Received:2007-11-13 Revised:2008-02-18 Online:2008-09-21 Published:2008-09-21
  • Contact: ZENG Qiong

摘要: 模型检验技术广泛应用于验证并发系统的性质。它的瓶颈一直是内存爆炸问题,将BDD技术引入到模型检验中的方法能有效地缓和状态组合爆炸问题。然而,随着系统规模的增大,BDD的大小仍呈指数增长。吴方法是一种处理多项式的符号计算方法,能有效地求解代数方程组并成功地应用于几何定理机器证明。给出应用吴方法计算表示Kripke结构和CTL公式的多项式的特征列的方法,从而实现对较大规模的系统性质的验证,进一步缓和状态组合爆炸问题。

Abstract: Model checking is widely used in verifying properties of concurrent systems.Its bottleneck is always the problem of memory explosion,the method adding BDD technology to model checking can effectively alleviate the combination state explosion problem.However,the size of BDDs greatly increases with the system becoming larger and more complex.Wu’s method is an efficient method in symbolic computation,it is efficient to solve algebraic equations,and has succeeded in geometry theorem proving.This paper presents a framework to apply Wu’s method to calculate the characteristic sets of polynomials that represent Kripke structures as well as CTL formulas,and further alleviates the combination state explosion problem.