基于Petri网的CSP并发系统验证技术研究

摘要：

通信顺序进程(CSP)和Petri网是两种重要的并发系统建模工具.CSP语言具有高度抽象性,可有效刻画并发进程之间的各种相互作用,但在物理结构的描述与验证分析方面显得不足.Petri网是一种形式化、图形化的并发系统建模和分析工具,侧重于系统的物理结构描述和性质分析.结合两者优点,首先利用CSP描述待验证的并发系统,然后将其转化为Petri网来分析系统的动态行为特性,最后利用性质分析工具TINA对系统性质进行分析和验证.实验结果表明,传统的CSP进程性质验证工具不能验证CSP进程的安全性,但其转化为Petri网后可有效地分析出导致安全性不能满足的危险因素,从而扩大了CSP描述的并发系统可验证性质的范围.

关键词：通信顺序进程(CSP)、并发系统、Petri网、性质验证、安全性

所属期刊栏目：42

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金61262008,61100186;广西自然科学基金2013GXNSFBA019267;广西教育厅重点项目:高可信软件的安全性验证研究,广西高等学校高水平创新团队及卓越学者计划,广西可信软件重点实验室基金项目kx201113;桂林电子科技大学创新团队资助

在线出版日期：2015-11-18（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：244-250,291