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

Model Checking CSP Based on ASP and Critical-Trace Model of CSP

作　　者：赵岭忠[1,2] 翟仲毅[2] 钱俊彦[2] 郭云川[3] 

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

出　　处：《软件学报》2015年第10期2521-2544,共24页Journal of Software

基　　金：国家自然科学基金(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.实验结果表明:与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,且可同时验证多条性质,在性质不满足时还可提供多条反例.Model checking is a mainstream method for formal verification of communicating sequential processes （CSP）. Existing CSP model checkers are based on operational semantics, which need to translate processes into a label transition system, and to extract the semantic model based on the system. The conversion process is complex. Moreover, in most CSP model checkers, the properties to be verified are described by CSP, which is helpful for refinement checking, but at the same time leads to limited description power and weak generality. To address these issues, a new denotational semantic model of CSP, critical-trace model, is proposed and proved to be reliable for model checking CSP. Based on this model, a framework for model checking CSP is established to allow critical-trace model to be constructed inductively from the traces of its components, and properties to be specified by linear temporal logic （LTL）, a universal property specification language. In addition, automatic mechanisms for generating critical-trace model and verifying LTL formulas are implemented with answer set programming （ASP）. Finally, the two mechanisms are integrated into a CSP model checker T ASP. Compared with the similar systems developed previously, experimental results indicate a higher ability of the proposed system to describe CSP processes and higher verification accuracy. Furthermore, TASP checks multiple properties in one execution of the system. When a property is not satisfied, the system also returns counterexamples for the property.

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

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