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

CSP model checking based on ASP and stable failure semantics

作　　者：左贵征 赵岭忠[1] 

机构地区：[1]桂林电子科技大学计算机科学与工程学院

出　　处：《桂林电子科技大学学报》2015年第5期401-407,共7页Journal of Guilin University of Electronic Technology

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

摘　　要：针对现有模型检测工具对活性描述不足、模型转换复杂,提出一种基于ASP及稳定失败语义的CSP模型检测方法。该方法采用时态逻辑LTL刻画性质,将进程的稳定失败模型和LTL公式转化为ASP,利用ASP求解器验证性质,实现一次运行验证多条性质。实验结果表明,该方法既扩大了基于稳定失败模型的活性验证范围,也避免了不同模型之间的转换。Aiming at lack of activity description and the complexity of models transition of CSP model checkers,CSP model checking based on ASP and stable failure semantics is proposed.In this method,the properties are specified by linear temporal logic（LTL）,the description of CSP system and LTL properties are implemented with answer set programming（ASP）,then multiple properties are verified in one execution of ASP solvers.The experimental result shows that the method expands the scope of liveness properties based on stable failure model,and prevents transition from different models.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]