本文旨在对并行程序设计、通信正确性验证、性能分析给出相应的建模与实 现方法，以利于并行程序的推广应用。本文工作的主要贡献表现在如下几个方 面： (1)在对现有主要的程序建模方法如UML、CSP(通信顺序过程)与CCS(通信 演算系统)和Petri网做了详细的分析，Petri网能较好地描述并发系统的结构， 表示系统中的并行、同步、冲突及顺序等关系，并以图形表示的组合模型，具 有直观、易懂和易用的优点。根据并行程序的具体特点，应用Petri网作为建 模工具，可以较好的描述并行程序中各种通信状态。 (2)研究了Petri网精炼操作动态性质保持关系，包括行为不变性、一致 相关性、状态不减性、公平性、不变量等等。它们为研究MPI并行程序逐步求 精方法奠定了理论基础。 (3)研究了基于Petri网的并行程序建模方法，包括：一般语句的Petri网 模型，MPI通信语句的Petri网模型，并给出MPI逐步求精的设计方法。 (4)研制了并行程序验证系统。本系统在windows环境下，使用Visual C++6.0开发，采用VC的MFC编程。文件的读写使用了VC的顺序化机制，实现 了网文件的永久性保存。充分利用了windows下GUI编程的优点，人机交互方 便，可以对并行程序Petri网模型的性质做分析，以检查并行程序中是否含有 与通信有关的错误。如：孤儿消息、缺发消息、死锁、活锁等。利用该系统， 给出矩阵乘法和快速傅立叶变换两个程序的建模和验证过程。 (5)参与开发移植了程序行为监测和性能分析工具ParaVT系统，该系统对 并行程序的结构进行分析，在程序运行过程中输出必要的调试信息，并且动态 的监视程序的运行情况，当前正在被调用的函数和函数的调用路径可以通过树 形调用图反映出来。根据接收到的调试信息对程序性能分析，给出对并行程序 性能的分析结果，并且可视化地直观呈现给最终的用户。可以查看的分析视图 包括动态运行图、通讯行为图、负载平衡图、通讯矩阵等。 最后，关于进一步工作的方向进行了简要的讨论。 关键词：Petri网、并行程序、精炼操作、设计、验证、死锁、性能分析、插 桩