Author Login Editor-in-Chief Peer Review Editor Work Office Work

Computer Engineering

Previous Articles     Next Articles

Stateful Dynamic Partial-order Reduction Method of Shrinking Candidate Backtrack Set

ZHAO Lu,ZHANG Jianpei,YANG Jing   

  1. (College of Computer Science and Technology,Harbin Engineering University,Harbin 150001,China)
  • Received:2014-04-14 Online:2015-05-15 Published:2015-05-15

收缩候选回溯集的有状态动态偏序归约方法

赵 璐,张健沛,杨 静   

  1. (哈尔滨工程大学计算机科学与技术学院,哈尔滨150001)
  • 作者简介:赵 璐(1983 - ),女,博士研究生,主研方向:软件形式化验证,模型检测;张健沛、杨 静,教授、博士生导师。
  • 基金资助:
    国家自然科学基金资助项目(61370083,61073043,61073041);教育部高等学校博士学科点专项科研基金资助项目(2011 2304110011,20122304110012);哈尔滨市科技创新人才研究专项基金资助项目(2011RFXXG015)。

Abstract: To verify multithreaded concurrent programs,combine stateless or stateful search based software model checking methods with Dynamic Partial-order Reduction(DPOR) so as to significantly reduce the state space of programs explored. DPOR uses current candidate backtrack set to refine corresponding backtrack set, however, the former computation cost actually exceeds the latter refinement demand. To solve the problem,a stateful DPOR method of shrinking candidate backtrack set is presented. The shrinking candidate set is formally defined,which can delete the redundant transitions for the same backtrack condition. For every interleaving backtrack state, the proposed method exploits current shrinking candidate set to refine corresponding backtrack set. Consequently,the method performs the stateful DPOR method to verify concurrent programs. Experimental results show that the method reduces the number of transitions explored,speeds up the refinement process and increases the efficiency of dynamic model checking compared with existing DPOR method.

Key words: software model checking, Dynamic Partial-order Reduction ( DPOR ), stateful search, backtrack set, shrinking candidate set

摘要: 在验证多线程并发程序时,将基于无状态或有状态搜索的软件模型检测与动态偏序归约方法相结合,能大 幅缩减待验证程序的状态空间,而动态偏序归约需不断利用当前候选回溯集更新相应回溯集,导致更新回溯集的 计算成本过高。为此,形式化定义收缩候选回溯集,消除原候选回溯集中满足同一回溯条件的冗余迁移。针对各 交织的回溯点,使用当前收缩候选回溯集更新相应回溯集,实现基于有状态动态偏序归约方法的并发多线程程序 验证。实验结果表明,与现有动态偏序归约方法相比,该方法能减少遍历迁移数,加速回溯集更新,提高动态软件 模型检测效率。

关键词: 软件模型检测, 动态偏序归约, 有状态搜索, 回溯集, 收缩候选集

CLC Number: