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

• 作者: 翟仲毅 赵岭忠 郭云川 钱俊彦
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 模型检测 通信顺序进程 关键迹模型 线性时态逻辑 回答集程序设计
• 年，卷（期）: 2015,（10）
• 所属期刊栏目: 系统软件与软件工程
• 页码范围: 2521-2544
• 页数: 24页
• 分类号: TP311
• 字数: 18164字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.004738

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	郭云川	中国科学院信息工程研究所	21	48	3.0	6.0