Axiomise 基于智能追踪器抽象的串行数据包设计穷尽形式验证案例

Axiomise 的 Ashish Darbari 以案例形式展示了如何用形式验证穷尽验证串行数据包设计。这类设计因每个数据包状态依赖此前所有在途数据包的历史而难以验证，作者采用智能追踪器（smart tracker）抽象，结合不变量作为辅助属性与 assume-guarantee 流程，在保证不遗漏合法行为缺陷的同时改善证明收敛。