| 基于Petri网的CSP并发系统验证技术研究 |
| |
| 引用本文： | 刘彦青,赵岭忠,钱俊彦.基于Petri网的CSP并发系统验证技术研究[J].计算机科学,2015,42(10):244-250, 291. |
| |
| 作者姓名： | 刘彦青 赵岭忠 钱俊彦 |
| |
| 作者单位： | 桂林电子科技大学计算机科学与工程学院 桂林541004,桂林电子科技大学计算机科学与工程学院 桂林541004,桂林电子科技大学计算机科学与工程学院 桂林541004 |
| |
| 基金项目： | 本文受国家自然科学基金(61262008,61100186),广西自然科学基金(2013GXNSFBA019267),广西教育厅重点项目:高可信软件的安全性验证研究,广西高等学校高水平创新团队及卓越学者计划,广西可信软件重点实验室基金项目(kx201113),桂林电子科技大学创新团队资助 |
| |
| 摘 要： | 通信顺序进程(CSP)和Petri网是两种重要的并发系统建模工具。CSP语言具有高度抽象性,可有效刻画并发进程之间的各种相互作用,但在物理结构的描述与验证分析方面显得不足。Petri 网是一种形式化、图形化的并发系统建模和分析工具,侧重于系统的物理结构描述和性质分析。结合两者优点,首先利用CSP描述待验证的并发系统,然后将其转化为Petri网来分析系统的动态行为特性,最后利用性质分析工具TINA对系统性质进行分析和验证。实验结果表明,传统的CSP进程性质验证工具不能验证CSP进程的安全性,但其转化为Petri网后可有效地分析出导致安全性不能满足的危险因素,从而扩大了CSP描述的并发系统可验证性质的范围。
|
| 关 键 词： | 通信顺序进程(CSP) 并发系统 Petri网 性质验证 安全性 |
| 收稿时间： | 2014/10/17 0:00:00 |
| 修稿时间： | 2/3/2015 12:00:00 AM |
Verification of Concurrent CSP Systems Based on Petri Net |
| |
| LIU Yan-qing,ZHAO Ling-zhong and QIAN Jun-yan.Verification of Concurrent CSP Systems Based on Petri Net[J].Computer Science,2015,42(10):244-250, 291. |
| |
| Authors: | LIU Yan-qing ZHAO Ling-zhong and 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 and School of Computer Science and Engineering,Guilin University of Electronic Technology,Guilin 541004,China |
| |
| Abstract: | |
| |
| Keywords: | Communicating sequential processes (CSP) Concurrent systems Petri net Property verification Safety |
| 本文献已被 万方数据 等数据库收录！ |
| 点击此处可从《计算机科学》浏览原始摘要信息 |
|
点击此处可从《计算机科学》下载全文 |
|
