基于petri网的csp并发系统验证技术研究

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