Page 312 - 《软件学报》2026年第5期
P. 312

唐瑞泽 等: 分布式系统模型检验技术研究进展                                                          2191


                 缺陷. 因此, 一致性比对技术是交互式 DMCK 的重要组成部分. 根据规约的定位, 一致性比对技术可用于发现代码
                 中的两类缺陷. 对于高层次规约, 它反映系统的设计需求, 其行为通常被视为正确的, 因此可以作为正确性判据
                 (oracle). 通过一致性比对, 代码中任何与高层次规约不一致的行为都可以视为代码的缺陷. 相比之下, 低层次规约
                 紧贴代码实现细节, 本身可能存在问题, 因此需在一致性比对后, 进一步借助属性规约验证是否违反预期属性. 由
                 于模型与代码已完成交互, 任何违反属性的路径也会出现在代码中. 一致性比对技术有两种方式: 自顶向下与自底
                 向上. 自顶向下的一致性比对从模型生成执行轨迹, 检查该轨迹是否能够在代码中成功重现. 自底向上的一致性比
                 对则从代码生成执行轨迹, 并在模型层进行比对检查.
                  5.2.1    自顶向下的一致性比对方法
                    自顶向下的一致性比对方法通过在代码中复现模型层的执行轨迹来实现. 其主要流程如下: 首先, 对规约进行
                 模型检验, 生成模型层的所有执行轨迹; 然后, 在目标系统中重放这些轨迹                      (重放技术依赖于第       3.1  节中的确定性
                 模拟执行技术), 并检查每一步的动作和状态是否一致. 如果发现不一致, 则需要人工介入分析分歧的原因. 如果使
                 用的是高层次规约, 不一致表明是代码中的实现缺陷, 需要修复代码使其与高层次规约一致; 如果使用的是低层次
                 规约, 不一致则说明规约本身存在转译错误, 需要修复规约. 此过程需持续迭代直到所有生成的执行轨迹都完成比对.
                    然而, 在实践中, 高层次规约常常面临规约本身质量不高或与代码分歧过大的问题, 难以直接确定分歧是否由
                 代码缺陷引起. 此外, 将规约层的所有执行用例复现到代码中还会面临状态爆炸问题. 因此, 当前的工具通常只针
                 对低层次规约的较小规模模型配置或部分状态空间生成执行轨迹, 通过规约分支覆盖率或在一定时间内未发现不

                 一致的情况来判断规约是否达到高质量.
                    SandTable [71] 是一个典型的交互式 DMCK 技术. 它的动机是现有的 DMCK 技术在代码层直接进行状态空间
                 探索时速度过慢, 因此选择在规约层进行状态空间探索, 以显著加速                     DMCK  状态探索速度, 并有效利用规约层的
                 高级状态约减技术       (如 TLC 的对称约减). SandTable 注意到, 现有代码不一定有高层次规约, 或代码实现很可能与
                 现有的高层次规约不一致, 因此选择使用低层次规约, 并手动为系统开发这些规约. 开发方式基于                             SandTable 支持
                 的全局事件类型来编写对应的事件动作. 理论上, 一致性比对过程需要对整个状态空间生成代码层的执行轨迹, 但
                 这在实际中并不现实. 因此, SandTable 通过随机模拟测试            (simulation testing) 来生成执行轨迹, 模拟测试的配置通
                 过启发式算法优化, 从而快速覆盖更多的规约分支. 所有比对不一致的情况                       (discrepancy) 都视为规约转译错误, 修
                 复后, 若一定时间内未发现不一致, 则认为规约质量已达标. 对模型检验中发现的缺陷可以直接使用确定性模拟执
                 行技术在代码中复现. SandTable 首次提出并建立了交互式             DMCK  的工作流程, 在模型检验过程中发现了 17 个代
                 码设计缺陷, 并在一致性比对中发现了 6 个代码实现缺陷.
                    SandTable 的后续工作   Remix [73] 也是一种交互式   DMCK  技术, 其一致性比对流程与        SandTable 相似. Remix
                 的核心在于通过粗细粒度的规约组合来平衡状态爆炸问题和规约与代码语义鸿沟问题, 并提出了一种保交互的粗
                 细粒度组合规约方式       (见第  5.1.2  节).
                  5.2.2    自底向上的一致性比对方法
                    自底向上的一致性比对方法通过在规约的状态空间中对所有可能的代码执行轨迹进行验证, 从而建立代码到
                 高层次规约的精化       (refinement) 关系  [134] . 该方法理论上需要穷举代码层的状态空间      (通过传统 DMCK 技术进行系
                 统性探索), 对每条执行轨迹进行采集, 并将其中涉及的变量状态转换为规约中变量的对应表示, 从而在模型层验

                 证该轨迹是否满足高层规约定义的精化条件.
                    这一思路最早在文献        [135,136] 中初步体现, 但这些工作的研究重点不在于轨迹生成的穷举性策略. 而且, 穷
                 举代码状态空间的开销极高, 导致其在实际缺陷发现场景中性价比较低, 不如直接采用传统                             DMCK  验证属性的方
                 式有效和高效. 因此, 目前尚无工作严格依此思路进行完整验证. 相比之下, 放弃穷举探索、只验证部分运行轨迹
                 是否与规约一致的轻量化派生技术轨迹确认               (trace validation) [137] 被广泛采用, 相关内容将在第  6.2 节中进一步讨论.

                  5.3   互动式的代码层执行
                    互动式 DMCK 的核心机制在于: 在保证模型和规约准确的前提下, 将状态空间的探索卸载                           (offloading) 到模
   307   308   309   310   311   312   313   314   315   316   317