%0 Journal Article
%T 基于关键迹和asp的csp模型检测
%A 赵岭忠？
%A 翟仲毅？
%A 钱俊彦？
%A 郭云川？
%J 软件学报
%P 2521-2544
%D 2015
%R 10.13328/j.cnki.jos.004738
%X 模型检测是通信顺序进程(communicatingsequentialprocesses,简称csp)形式化验证的重要手段.当前,csp模型检测方法基于操作语义,需将进程转化为迁移系统,进而提取语义模型,但转化过程较为复杂;待验证性质采用csp语言进行描述,虽然有利于精炼检测(refinementchecking),但描述能力较弱,通用性不强.鉴于此,提出了一种新的csp指称语义模型——关键迹模型(critical-tracemodel)及基于该指称语义模型的csp模型检测方法,并证明了其验证的可靠性,避免了上述问题.关键迹模型采用递归策略计算,待验证性质采用线性时态逻辑(lineartemporallogic,简称ltl)描述.基于回答集程序设计(answersetprogramming,简称asp)实现了关键迹模型的自动生成及ltl的自动验证,并开发了一个csp模型检测原型系统——t_asp.实验结果表明:与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,且可同时验证多条性质,在性质不满足时还可提供多条反例.
%K 模型检测
%K 通信顺序进程
%K 关键迹模型
%K 线性时态逻辑
%K 回答集程序设计
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=4738&flag=1