| 基于ASP的CSP模型验证性质反例生成技术研究 |
| |
| 引用本文： | 王雪松,赵岭忠,张 超.基于ASP的CSP模型验证性质反例生成技术研究[J].计算机应用研究,2013,30(1):52-55. |
| |
| 作者姓名： | 王雪松 赵岭忠 张 超 |
| |
| 作者单位： | 桂林电子科技大学 a. 电子工程与自动化学院; b. 广西可信软件重点实验室, 广西 桂林 541004 |
| |
| 基金项目： | 国家自然科学基金资助项目（61262008, 61063002）; 广西科学基金资助项目（2011GXNSFA018166, 2011GXNSFA018164）; 广西可信软件重点实验室基金资助项目（kx201113） |
| |
| 摘 要： | 为了解决当前通信顺序进程(CSP)模型检测不支持在验证工具的一次运行中验证多个性质的问题,建立了基于ASP的CSP并发模型验证框架。主要研究在该框架下当待验证的系统性质不满足时生成相应性质反例的技术。把ASP程序调试中的ASP程序支撑原因分析技术应用于该问题的研究,提出了相应的反例生成算法,实例表明了该算法的正确性。
|
| 关 键 词： | 通信顺序进程 回答集编程 支撑原因 |
Counterexample generation in ASP-based CSP model verification |
| |
| WANG Xue-song,ZHAO Ling-zhong,ZHANG Chao.Counterexample generation in ASP-based CSP model verification[J].Application Research of Computers,2013,30(1):52-55. |
| |
| Authors: | WANG Xue-song ZHAO Ling-zhong ZHANG Chao |
| |
| Affiliation: | a. School of Electronic Engineering & Automation, b. Guangxi Provincial Key Laboratory of Trusted Software, Guilin University of Electronic Technology, Guilin Guangxi 541004, China |
| |
| Abstract: | This paper proposed an ASP based framework for verifying concurrent model described by CSP to solve the problem of verifying multiple properties in one run of a model checker. It mainly discussed the problem of generating counterexamples while the verified property was not satisfied in this framework. The technique of justification of ASP program, which was usually used in the debugging of ASP programs, applied to this study and proposed an algorithm for generating property counterexamples. The effectiveness of the algorithm is shown by examples. |
| |
| Keywords: | |
| 本文献已被 CNKI 等数据库收录！ |
| 点击此处可从《计算机应用研究》浏览原始摘要信息 |
|
点击此处可从《计算机应用研究》下载全文 |
|
