作者搜索
新闻
  10.5.5
C-DBLP系统正式发布作者研究兴趣及学术活动展示功能，请访问作者页面试用。
  09.7.6
C-DBLP的文献BibTex信息展示功能正式上线，请访问文章详细页面使用。
  09.7.29
C-DBLP系统新增同名区分功能，欢迎大家在作者页面试用。该功能部分使用了清华大学王建勇老师课题组提出的GHOST（GrapH-based framewOrk for name diStincTion）算法，在此表示感谢。
  09.6.2
C-DBLP系统集成了作者的相关图片并在搜索结果页面展示，敬请试用。
  更多>>
 
并发程序的切片模型检验方法  BibTex
作者： 董威 王戟 齐治昌
单位： 国防科学技术大学计算机学院 长沙410073 (董威;王戟);国防科学技术大学计算机学院 长沙410073(齐治昌)
关键词： 模型检验;并发;程序切片
出处： 计算机学报 2003 年 03期
基金： 国家“八六三”高技术研究发展计划 ( 2 0 0 1AA113 2 0 2 );国家自然科学基金( 69973 0 5 1,90 10 40 0 7);霍英东青年教师基金 ( 710 64 )资助
全文链接： 查看全文>>
摘要：
　　提出了一种对并发程序进行切片以缩减模型检验状态空间的方法 .首先针对并发程序中的同步与通信定义了一组依赖关系 ,包括并发分支与接合、非确定性、信道、共享变量等特征 .对于从要验证的时态逻辑性质中提取的关于多个程序点的切片标准 ,文中给出算法根据相应的依赖关系通过不动点运算得到并发程序切片 .可以证明得到的切片与原程序对于该性质具有相同的可满足性
正文快照：
　　1　引　言模型检验 (ｍｏｄｅｌｃｈｅｃｋｉｎｇ)是一种重要的自动验证技术 ,主要通过显式状态搜索或隐式不动点计算来验证有穷状态并发系统的模态 命题性质 .由于模型检验可以自动执行 ,并能在系统不满足性质时提供反例路径 ,因此在应用中比演绎证明更受推崇 .模型检验面临
Slicing Concurrent Programs for Model Checking
Author： DONG Wei WANG Ji QI Zhi Chang (School of Computer Science;National University of Defense Technology;Changsha 410073)
Keywords： model checking;concurrency;program slicing
Abstract：
　Model checking is an important technology of automatic verification, and its main problem faced is space explosion, which is usually caused by the concurrency in the system. This paper presents an efficient approach to slice concurrent programs for model checking. A set of dependence relations is defined corresponding to the characteristics of synchronization and communication in concurrent programs, such as parallel fork and joint, non deterministic, channel, share variable, and lock. The dependence graph of concurrent program can be constructed from these dependence relations. To ensure the correctness of verification result for temporal property, the multi points relevant slicing criterion is extracted from the property. Then, the paper presents a method to compute the slice of concurrent program, which only includes the statements reachable from the slicing criterion in dependence graph. The correctness of the resulted slice is guaranteed with respect to the satisfaction of the desired property. The method throws away the irrelevant portions of the program corresponding to the property, which will reduce the state space to be explored in model checking. Finally, slicing is compared with partial order reduction, another method that reduces the state space according to the property, and the similarities and differences of these two methods are discussed.