Model Checking CSP Concurrent Systems Based on CTL
- 分享到:
摘要：
主要通过指称语义和回答集程序(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.
作者：
王亚丽 杨育捷 赵岭忠 翟仲毅
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)
机构地区：
betway官方app 计算机与信息工程学院 betway官方app 智慧商务与物联网技术河南省工程实验室 桂林电子科技大学广西可信软件重点实验室
出处：
《betway官方app 学报：自然科学版》 CAS 北大核心 2016年第5期140-145,共6页
基金：
国家自然科学基金(61262008) 广西可信软件重点实验室开放课题(kx201415) 河南省科技厅基础与前沿技术研究项目(132300410430)
关键词：
模型检测 迹模型 计算树逻辑 回答集程序设计
model checking trace model computing tree logic answer set programming
分类号：
TP311 [自动化与计算机技术—计算机软件与理论]
