| 基于进程迹的CSP模型验证框架 |
| |
| 引用本文： | 赵岭忠,翟仲毅,钱俊彦. 基于进程迹的CSP模型验证框架[J]. 计算机科学, 2013, 40(11): 181-186,221 |
| |
| 作者姓名： | 赵岭忠 翟仲毅 钱俊彦 |
| |
| 作者单位： | 桂林电子科技大学计算机科学与工程学院 桂林541004;桂林电子科技大学计算机科学与工程学院 桂林541004;桂林电子科技大学计算机科学与工程学院 桂林541004 |
| |
| 基金项目： | 本文受国家自然科学基金(61262008,2),广西自然基金(2011GXNSFA018166,1GXNSFA018164),广西可信软件重点实验室基金(kx201113)资助 |
| |
| 摘 要： | CSP(Communicating Sequential Processes)是构建并发系统和网络安全协议的经典方法。当前主流的CSP模型验证方法需将进程转化为迁移系统,转化过程比较复杂；性质采用迹进行规范,不利于活性的描述。提出了一种基于进程迹的CSP模型验证框架,其性质采用通用的规范方法LTL进行描述。利用ASP(Answer Set Programming)技术实现了一个CSP验证系统。实验表明,与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,在性质不满足时还可提供反例。
|
| 关 键 词： | 通信顺序进程(CSP) 并发系统 迹模型 回答集编程(ASP) 中图法分类号TP311文献标识码A |
| 收稿时间： | 2013-01-23 |
| 修稿时间： | 2013-06-17 |
Framework for Model Checking CSP with Traces of Processes |
| |
| ZHAO Ling-zhong,ZHAI Zhong-yi and QIAN Jun-yan. Framework for Model Checking CSP with Traces of Processes[J]. Computer Science, 2013, 40(11): 181-186,221 |
| |
| Authors: | ZHAO Ling-zhong ZHAI Zhong-yi QIAN Jun-yan |
| |
| Affiliation: | School of Computer Science and Engineering,Guilin University of Electronic Technology,Guilin 541004,China;School of Computer Science and Engineering,Guilin University of Electronic Technology,Guilin 541004,China;School of Computer Science and Engineering,Guilin University of Electronic Technology,Guilin 541004,China |
| |
| Abstract: | |
| |
| Keywords: | Communicating sequential processes Concurrent system Trace model Answer set programming |
|
| 点击此处可从《计算机科学》浏览原始摘要信息 |
|
点击此处可从《计算机科学》下载全文 |
|
