基于关键迹和ASP的CSP模型检测
模型检测是通信顺序进程(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.实验结果表明:与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,且可同时验证多条性质,在性质不满足时还可提供多条反例.
模型检测、通信顺序进程、关键迹模型、线性时态逻辑、回答集程序设计
26
TP311(计算技术、计算机技术)
国家自然科学基金61262008,61100186;广西自然科学基金2013GXNSFBA019267;武汉大学软件工程国家重点实验室开放基金SKLSE20100806;广西教育厅重点项目;广西高等学校高水平创新团队及卓越学者计划;广西可信软件重点实验室基金kx201113,kx201415;桂林电子科技大学创新团队资助项目
2016-08-19（万方平台首次上网日期，不代表论文的发表时间）
共24页
2521-2544
