参数化验证：群成员算法
计算机科学中的逻辑
2016-08-31 v1
摘要
我们解决 TTP 协议中验证 clique 规避问题的难题。TTP 允许车内多个站点进行通信。该协议包含众多机制以确保对故障的鲁棒性。具体而言，TTP 包含一种算法，使站点能够自我识别故障并离开通信。该算法必须满足关键的“非-clique”属性：不可能存在两个或多个互不相交的站点组，这些组仅与自身组成内的站点通信。本文提出了一种用于任意站点数量 和给定故障数 的自动化验证方法。我们提供了一种抽象模型，使该算法可通过无界（参数化）计数自动机进行建模。我们在单一故障情形下，使用 ALV 工具和 LASH 工具对该模型进行了非-clique 属性验证。
引用
@article{arxiv.cs/0505033,
title = {Parametric Verification of a Group Membership Algorithm},
author = {Ahmed Bouajjani and Agathe Merceron},
journal= {arXiv preprint arXiv:cs/0505033},
year = {2016}
}
备注
34 pages. To appear in Theory and Practice of Logic Programming (TPLP)