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

摘要

通信顺序进程 CSP是一种高度抽象的形式化描述语言，具有严格的数学理论支撑，可有效刻画并发系统进程之间的各种相互作用。然而，在 CSP并发系统的验证方面，由于其本身特性所限，还存在以下不足：1)用CSP语言描述的并发系统没有反映系统的物理结构信息，不便于与此相关的系统特性的分析和验证；2)尽管对并发有一定的刻画，但不能全面反映复杂系统的真实并发行为。Petri网是一种形式化、图形化的并发系统建模和分析工具，虽然在原始模型抽象方面不如CSP，但能够精确地分析系统的静态特性和动态行为性质，侧重于系统的物理结构描述和性质分析。　　本文将Petri网技术引入CSP并发系统验证将有助于弥补单纯基于CSP分析来验证系统性质的不足。首先利用CSP描述待验证的并发系统，将其关键迹转化为Petri网来分析系统的行为特性；然后利用性质分析工具 TINA对系统性质进行分析和验证。实验结果表明，CSP并发系统转化为Petri网后可有效地分析出导致安全性不能满足的危险因素，从而扩大了 CSP描述的并发系统可验证性质的范围。本文主要研究内容如下：　　（1）讨论CSP进程到Petri网的转换规则。该部分包括CSP关键迹模型的基本进程到Petri网的转换规则以及CSP并发操作到Petri网的转换规则，基本进程包括前缀、递归、确定性选择和非确定性选择。并发操作包括交互、并发和穿插，同时，给出基于Petri网的条件约束，保证转换后Petri网的完整性。　　（2）研究 CSP进程与转换后 Petri网的等价关系。基于关键迹模型验证的等价性，证明了 CSP庞大的迹模型与关键迹模型在描述和性质验证方面是等价的，因此将关键迹转换为 Petri网与普通迹转换之间具有等价性，但是关键迹效率更高。在讨论CSP进程与转换后Petri网的等价性时，通过运用Petri网语言和CSP的顺序组件等相关知识，给出了两种模型在等价性方面的理论证明。　　（3）实例分析，以铁路公路交叉口交通控制器为例，运用上述方法，对转换后的Petri网进行可达树分析，利用工具TINA给出改进后Petri网（即时间Petri网）对应的状态类，同时验证并发系统的安全性等重要性质，从而，扩大了CSP并发系统的验证范围。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪论

§1.1 引论

§1.2 研究现状

§1.3 研究内容

§1.4 文章结构

第二章 预备知识

§2.1 CSP概述

§2.2 Petri网概述

§2.3 计算树逻辑CTL*

第三章 CSP基本进程到Petri网的转换规则

§3.1 基于Petri网的CSP并发系统验证框架

§3.2 CSP进程的关键迹模型

§3.3 基本进程的转换规则

§3.4 小结

第四章 CSP并发操作到Petri网的转换规则

§4.1 并发操作下的转换规则

§4.2 基于Petri网的条件约束

§4.3 实例说明

§4.4 小结

第五章 CSP进程与转换后Petri网等价关系研究

§5.1 基于关键迹模型验证的等价性证明

§5.2 CSP进程与转换后Petri网的等价性证明

§5.3 小结

第六章 实例分析与验证

§6.1 CSP并发系统验证

§6.2 Petri网可达树分析

§6.3 时间Petri网验证

§6.4 实验结果

§6.5 小结

第七章 总结与展望

参考文献

致谢

作者在攻读硕士期间的主要研究成果