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

来源：软件学报杂志2015年第10期北京时间：

作者：赵岭忠,翟仲毅,钱俊彦,郭云川

单位：赵岭忠，软件工程国家重点实验室武汉大学, 湖北 武汉 430072;广西可信软件重点实验室桂林电子科技大学, 广西 桂林 54100411,翟仲毅，广西可信软件重点实验室桂林电子科技大学, 广西 桂林 54100402,钱俊彦，广西可信软件重点实验室桂林电子科技大学, 广西 桂林 54100403,郭云川，中国科学院 信息工程研究所, 北京 10009304

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

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

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