基于关键迹和ASP的CSP模型检测

作     者：赵岭忠 翟仲毅 钱俊彦 郭云川 ZHAO Ling-Zhong;ZHAI Zhong-Yi;QIAN Jun-Yan;GUO Yun-Chuan

作者机构：软件工程国家重点实验室(武汉大学)湖北武汉430072 广西可信软件重点实验室(桂林电子科技大学)广西桂林541004 中国科学院信息工程研究所北京100093 

基　　金：国家自然科学基金(61262008 61100186) 广西自然科学基金(2013GXNSFBA019267) 武汉大学软件工程国家重点实验室开放基金(SKLSE20100806) 广西教育厅重点项目 广西高等学校高水平创新团队及卓越学者计划 广西可信软件重点实验室基金(kx201113 kx201415) 桂林电子科技大学创新团队资助项目 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2015年第26卷第10期

页      码：2521-2544页

摘      要：模型检测是通信顺序进程(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.实验结果表明:与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,且可同时验证多条性质,在性质不满足时还可提供多条反例.

主 题 词：模型检测 通信顺序进程 关键迹模型 线性时态逻辑 回答集程序设计 

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

核心收录：

D　O　I：10.13328/j.cnki.jos.004738

馆 藏 号：203233913...