期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

结合搜索空间划分和抽象进行LTL模型检测 被引量：6

原文传递
导出
摘要 在应用模型检测于工业系统时,状态空间爆炸仍然是一个主要的障碍.基于抽象的方法在克服状态空间爆炸方面取得了很大的成功.提出一种结合搜索空间划分和抽象的方法来降低模型检测的空间复杂度.划分依赖于每个所分划的搜索空间的表达.特别地,划分可以逐步求精以获得更好的空间消减.从数值实验看,这种搜索空间划分和抽象的结合在基于内存的需求上能提高验证的效率,同时能得到比单独使用其中一种方法更好的效果.
作者 蒲飞 张文辉
机构地区 中国科学院软件所计算机科学国家重点实验室
出处 《中国科学（E辑）》 CSCD 北大核心 2007年第12期1504-1520,共17页 Science in China(Series E)
基金 国家自然科学基金(批准号:60573012 60421001) 国家重点基础研究发展规划(批准号:2002cb312200)资助项目
关键词 搜索空间划分 求精 抽象 LTL模型检测
分类号 TP311.52 [自动化与计算机技术—计算机软件与理论]
  • 相关文献

参考文献1

二级参考文献25

  • 1Peled D. All from one, one for all, on model-checking using representatives. Lecture Notes in Computer Science 697, CAV, 1993, pp.409-423.
  • 2Peled D. Ten years of partial order reduction. Lecture Notes in Computer Science 1427, Vancouver, Canada,CAV, 1998, pp.17-28.
  • 3Holzmann G J. The model checker Spin. IEEE Trans.Software Engineering, May 1997, 23(5): 279-295.
  • 4Berezin S, Campos S, Clarke E M. Compositional reasoning in model checking. Lecture Notes in Computer Science 1536, COMPOS, 1997, pp.81-102.
  • 5Millett L I, Teitelbaum T. Issues in slicing PROMELA and its applications to model checking, protocol understanding, and simulation. STTT, 2000, 2(4): 343-349.
  • 6Emerson E A. Temporal and modal logic. Handbook of Theoretical Computer Science, 1990, (B): 997-1072.
  • 7Gerth R, Peled D, Vardi M, Wolper P. Simple on-the-fly automatic verification of linear temporal logic. In 15th IFIP WG6.1 Int. Syrup. Protocol Specification, Testing and Verification, Warsaw, Poland, June 1995, pp.3-18.
  • 8Bloem R, Ravi K, Somenzi F. Efficient decision procedures for model checking of linear time logic properties.Lecture Notes in Computer Science 1633, Trento, Italy,CAV, 1999, pp.222-235.
  • 9Somenzi F, Bloem R. Efficient Biichi automata from LTL formulae. Lecture Notes in Computer Science 1855, Chicago, USA, CAV, 2000, pp.248-263.
  • 10Stahl K, Baukus K, Lakhnech Yet al. Divide, abstract,and model-check. Lecture Notes in Computer Science 1680, In Proc. the 5th International SPIN Workshop,Trento, Italy, July 1999, pp.57-76.

共引文献2

同被引文献158

  • 1卿斯汉.高安全等级安全操作系统的隐蔽通道分析[J].软件学报,2004,15(12):1837-1849. 被引量：31
  • 2沈昌祥,张焕国,冯登国,曹珍富,黄继武.信息安全综述[J].中国科学（E辑）,2007,37(2):129-150. 被引量：358
  • 3李暾,屈婉霞,郭阳,刘功杰,李思昆.基于符号模拟和约束逻辑编程的RTL级Verilog谓词抽象方法[J].计算机学报,2007,30(7):1138-1144. 被引量：1
  • 4HuthM,RyanM.面向计算机科学的数理逻辑系统建模与推理[M].北京:机械工业出版社,2007.
  • 5Dhurjati D, Adve V. Backwards-compatible array bounds checking for C with very low overhead[C]//Proc of the 28th Int Conf on Software Engineering. New York: ACM, 2006: 162-171.
  • 6Livshits V, Lain M. Tracking pointers with path and context sensitivity for bug detection in C programs [C] //Proc of the 9th European Software Engineering Conf Held Jointly with 11th ACM SIGSOFT Int Syrup on Foundations of Software Engineering. New York: ACM, 2003: 317-326.
  • 7Zitser M. Securing software: An evaluation of static source code analyzers [D]. Cambridge: MIT, 2003.
  • 8Clarke E M, Grumberg O, Peled D. Model Checking [M]. Boston: MIT, 1999.
  • 9Cousot P. Formal language, grammar and set-constraint- based program analysis by abstract interpretation [C]//Proc of the 7th Int Conf on Functional Programming Languages and Computer Architecture. New York: ACM, 1995: 170- 181.
  • 10FSF. GCC, the GNU compiler collection FEB/OLd. [2009- 10-17]. http://gcc, gnu. org/.

引证文献6

二级引证文献26

中国科学（E辑）
2007年 第12期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部