基于 ASP 及稳定失败语义的 CSP 模型检测

摘要：

针对现有模型检测工具对活性描述不足、模型转换复杂,提出一种基于 ASP 及稳定失败语义的 CSP 模型检测方法。该方法采用时态逻辑 LTL 刻画性质,将进程的稳定失败模型和 LTL 公式转化为 ASP,利用 ASP 求解器验证性质,实现一次运行验证多条性质。实验结果表明,该方法既扩大了基于稳定失败模型的活性验证范围,也避免了不同模型之间的转换。

关键词：通信顺序进程、线性时态逻辑、稳定失败语义、回答集程序设计

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金61262008,61100186;广西可信软件重点实验室基金KX201113

在线出版日期：2015-12-01（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：401-407