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