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

作     者：左贵征 赵岭忠 Zuo Guizheng;Zhao Lingzhong

作者机构：桂林电子科技大学计算机科学与工程学院 

基　　金：国家自然科学基金(61262008 61100186) 广西可信软件重点实验室基金(KX201113) 

出 版 物：《桂林电子科技大学学报》 (Journal of Guilin University of Electronic Technology)

年 卷 期：2015年第35卷第5期

页      码：401-407页

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

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

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

D　O　I：10.16725/j.cnki.cn45-1351/tn.2015.05.012

馆 藏 号：203874600...