基于CTL的并发系统CSP模型验证  

Model Checking CSP Concurrent Systems Based on CTL

作　　者：王亚丽[1,2] 杨育捷[1,2] 赵岭忠[3] 翟仲毅[3] WANG Yali YANG Yujie ZHAO Lingzhong ZHAIi Zhongyi(College of Computer and Information Engineering Engineering Lab of Intelligence Business ＆ Internet of Things, Henan Normal University, Xinxiang 453007,China School of Computer Science and Engineering, Guilin University of Electronic Technology, Guilin 541004, China)

机构地区：[1]河南师范大学计算机与信息工程学院,河南新乡453007 [2]河南师范大学"智慧商务与物联网技术"河南省工程实验室,河南新乡453007 [3]桂林电子科技大学广西可信软件重点实验室,广西桂林541004

出　　处：《河南师范大学学报（自然科学版）》2016年第5期140-145,共6页Journal of Henan Normal University(Natural Science Edition)

基　　金：国家自然科学基金(61262008);广西可信软件重点实验室开放课题(kx201415);河南省科技厅基础与前沿技术研究项目(132300410430)

摘　　要：主要通过指称语义和回答集程序(Answer Set Programming,简称ASP)完成迹模型的生成,并构建了一套基于计算树逻辑(computing tree logic,简称CTL)的CSP模型验证方法.实验表明,该方法对于分支类型的性质具有较好的描述能力,且保证了验证的正确性.CSP is one of the main methods of model checking.Denotational semantics and operational semantics are the two approaches adopted for model validation.Compared with operational semantics,denotational semantics computation model is intuitive,and easy to extend.This paper mainly completed the trace model＇s generation by denotational semantics and ASP mechanism,and developed a set of CSP model validation method based on CTL.Results showed that,this method has a good description ability for the properties of the branch type,and can ensure the accuracy of verification.

关 键 词：模型检测 迹模型 计算树逻辑 回答集程序设计 

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