计算机科学 ›› 2014, Vol. 41 ›› Issue (6): 125-130.doi: 10.11896/j.issn.1002-137X.2014.06.025
陈娟娟,魏欧
CHEN Juan-juan and WEI Ou
摘要： 多值模型可用于对包含不确定与不一致信息的软件系统进行建模与验证。提出了采用基于分解的方式来刻画多值模型之间的逼近关系,这为采用抽象方法解决模型检测时所产生的状态爆炸问题奠定了理论基础。为此,首先给出了多值模型分解为多个三值模型的方法,并且证明了任意μ演算公式在多值模型上的检测结果等于在分解后所有三值模型上的检测结果的合并。进一步,由三值模型上的混合模拟关系给出了多值模型间逼近关系的结构定义,并证明对于任意给定的两个满足逼近关系的多值模型,μ演算公式在其上的检测结果在信息序关系上得以保持。
| [1] Clarke E,Grumberg O,Peled D．Model Checking[M]．MIT press,1999 [2] Shoham S,Grumberg O．Multi-valued model checking games[J]．Journal of Computer and System Sciences,2012,78(2):414-429 [3] Ginsberg M L．Multi valued logics:a uniform approach to rea-soning in artificial intelligence[J]．Computational intelligence,1988,4(3):265-316 [4] Kleene S C．Introduction to Metamathematics[M]．North Holland,1987 [5] Chechik M,Devereux B,Easterbrook S,et al．Multi-valued symbolic model-checking[J]．ACM Transactions on Software Engineering and Methodology (TOSEM),2003,12(4):371-408 [6] Dams D,Gerth R,Grumberg O．Abstract interpretation of reactive systems[J]．ACM Transactions on Programming Languages and Systems (TOPLAS),1997,19(2):253-291 [7] Godefroid P,Jagadeesan R．Automatic abstraction using genera-lized model checking[M]∥Computer Aided Verification．Springer Berlin Heidelberg,2002:137-151 [8] Godefroid P,Jagadeesan R．On the expressiveness of 3-valued models[M]∥Verification,Model Checking,and Abstract Interpretation．Springer Berlin Heidelberg,2003:206-222 [9] Gurfinkel A,Wei O,Chechik M．Model checking recursive programs with exact predicate abstraction[M]∥Automated Technology for Verification and Analysis．Springer Berlin Heidelberg,2008:95-110 [10] Ball T,Kupferman O,Yorsh G．Abstraction for falsification[M]∥Computer Aided Verification．Springer Berlin Heidelberg,2005:67-81 [11] Meller Y,Grumberg O,Shoham S．A framework for compositional verification of multi-valued systems via abstraction-refinement[M]∥Automated Technology for Verification and Analysis．Springer Berlin Heidelberg,2009:271-288 [12] 陈娟娟,魏欧,黄志球,等．基于双格的多值模型的精化关系与对称化简[J]．计算机工程与应用,2013,49(22):40-45 [13] Bruns G,Godefroid P．Model checking partial state spaces with 3-valued temporal logics[M]∥Computer Aided Verification．Springer Berlin Heidelberg,1999:274-287 [14] Huth M,Pradhan S．Lifting assertion and consistency checkers from single to multiple viewpoints[M]．Imperial College of Science,Technology and Medicine,Department of Computing,2002 [15] Chechik M,Gurfinkel A,Devereux B．χChek:A multi-valuedmodel-checker[M]∥Computer Aided Verification．Springer Berlin Heidelberg,2002:505-509 [16] Gurfinkel A,Chechik M．Multi-valued model checking via classical model checking[M]∥CONCUR 2003-Concurrency Theory．Springer Berlin Heidelberg,2003:266-280 [17] 魏欧,袁泳,蔡昕烨,等．循环对称化简及在三值模型上的扩展[J]．软件学报,2011,22(6) [18] Gurfinkel A,Wei O,Chechik M．Systematic construction of abstractions for model-checking[M]∥Verification,Model Checking,and Abstract Interpretation．Springer Berlin Heidelberg,2006:381-397 [19] Kupferman O,Lustig Y．Latticed simulation relations and games[M]∥Automated Technology for Verification and Analysis．Springer Berlin Heidelberg,2007:316-330 |
| No related articles found! |
|
||
首页