| 基于关键迹和ASP的CSP模型检测 |
| |
| 引用本文： | 赵岭忠,翟仲毅,钱俊彦,郭云川.基于关键迹和ASP的CSP模型检测[J].软件学报,2015,26(10):2521-2544. |
| |
| 作者姓名： | 赵岭忠 翟仲毅 钱俊彦 郭云川 |
| |
| 作者单位： | 软件工程国家重点实验室武汉大学, 湖北 武汉 430072;广西可信软件重点实验室桂林电子科技大学, 广西 桂林 541004,广西可信软件重点实验室桂林电子科技大学, 广西 桂林 541004,广西可信软件重点实验室桂林电子科技大学, 广西 桂林 541004,中国科学院 信息工程研究所, 北京 100093 |
| |
| 基金项目： | 国家自然科学基金(61262008,61100186);广西自然科学基金(2013GXNSFBA019267);武汉大学软件工程国家重点实验室开放基金(SKLSE20100806);广西教育厅重点项目;广西高等学校高水平创新团队及卓越学者计划;广西可信软件重点实验室基金(kx201113,kx201415);桂林电子科技大学创新团队资助项目 |
| |
| 摘 要： | 模型检测是通信顺序进程(communicating sequential processes,简称CSP)形式化验证的重要手段.当前, CSP模型检测方法基于操作语义,需将进程转化为迁移系统,进而提取语义模型,但转化过程较为复杂;待验证性质采用CSP语言进行描述,虽然有利于精炼检测(refinement checking),但描述能力较弱,通用性不强.鉴于此,提出了一种新的CSP指称语义模型——关键迹模型(critical-trace model)及基于该指称语义模型的CSP模型检测方法,并证明了其验证的可靠性,避免了上述问题.关键迹模型采用递归策略计算,待验证性质采用线性时态逻辑(linear temporal logic,简称LTL)描述.基于回答集程序设计(answer set programming,简称ASP)实现了关键迹模型的自动生成及LTL的自动验证,并开发了一个CSP模型检测原型系统——T_ASP.实验结果表明:与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,且可同时验证多条性质,在性质不满足时还可提供多条反例.
|
| 关 键 词： | 模型检测 通信顺序进程 关键迹模型 线性时态逻辑 回答集程序设计 |
| 收稿时间： | 2013/9/10 0:00:00 |
| 修稿时间： | 2014/9/29 0:00:00 |
Model Checking CSP Based on ASP and Critical-Trace Model of CSP |
| |
| ZHAO Ling-Zhong,ZHAI Zhong-Yi,QIAN Jun-Yan and GUO Yun-Chuan.Model Checking CSP Based on ASP and Critical-Trace Model of CSP[J].Journal of Software,2015,26(10):2521-2544. |
| |
| Authors: | ZHAO Ling-Zhong ZHAI Zhong-Yi QIAN Jun-Yan and GUO Yun-Chuan |
| |
| Affiliation: | State Key Laboratory of Software Engineering Wuhan University, Wuhan 430072, China;Guangxi Key Laboratory of Trusted Software Guilin University of Electronic Technology, Guilin 541004, China,Guangxi Key Laboratory of Trusted Software Guilin University of Electronic Technology, Guilin 541004, China,Guangxi Key Laboratory of Trusted Software Guilin University of Electronic Technology, Guilin 541004, China and Institute of Information Engineering, The Chinese Academy of Sciences, Beijing 100093, China |
| |
| Abstract: | |
| |
| Keywords: | model checking communicating sequential process critical-trace model linear temporal logic answer set programming |
|
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
