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

• 作者: 张健沛 杨静 赵璐
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 软件模型检测 动态偏序归约 有状态搜索 回溯集 收缩候选集
• 年，卷（期）: 2015,（5）
• 所属期刊栏目: ?体系结构与软件技术?
• 页码范围: 70-76
• 页数: 7页
• 分类号: TP301
• 字数: 7283字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2015.05.012

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张健沛	哈尔滨工程大学计算机科学与技术学院	156	1356	19.0	28.0
2	杨静	哈尔滨工程大学计算机科学与技术学院	178	2073	24.0	37.0
3	赵璐	哈尔滨工程大学计算机科学与技术学院	1	1	1.0	1.0