资料下载
×
基于关键迹和ASP的CSP模型检测
消耗积分:2 |
格式:rar |
大小:0.96 MB |
2018-01-23
分享资料个
模型检测是通信顺序进程（communicatmg sequential processes，简称CSP）形式化验证的重要手段．当前，CSP模型检测方法基于操作语义，需将进程转化为迁移系统，进而提取语义模型，但转化过程较为复杂；待验证性质采用CSP语言进行描述，虽然有利于精炼检测（refinement checking），但描述能力较弱，通用性不强．鉴于此，提出了一种新的CSP指称语义模型一一关键迹模型（critical-trace model）及基于该指称语义模型的CSP模型检测方法，并证明了其验证的可靠性，避免了上述问题．关键迹模型采用递归策略计算，待验证性质采用线性时态逻辑（linear temporal logic，简称LTL）描述，基于回答集程序设计（answer set programming，简称ASP）实现了关键迹模型的自动生成及LTL的自动验证，并开发了一个CSP模型检测原型系统-T ASP.实验结果表明：与类似系统相比，该系统的描述能力更强，验证结果的准确性更高，且可同时验证多条性质，在性质不满足时还可提供多条反例．
声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉
评论(0)
发评论
- 相关下载
- 相关文章
