以并行计算为基础的高性能计算科学当前已经成为科学研究的第三大支柱。使用并行计算的首要因为是高性能高效率,而并行程序的首要条件是正确性。以往的设计和分析工具都只关注于正确性和高性能的其中一个方面。　　 针对以上情况,作者提出了一种能同时进行正确性验证和性能分析的工具原型,该工具原型可使正确性验证和性能分析一直贯穿于设计、运行、直到结果分析的全过程中。通过比较,给出用Petri网系统对并行程序建立模型的优越性。　　 现在最广泛应用的编程模式是基于消息传递的,而MPI已经成为事实上的标准。本文研究了并行程序函数的特点,给出了其所嵌套的C语言结构的Petri网系统模型,提出针对并行程序建模初步的步骤与方法,给出了静态可执行的和并行正确的两种并行程序概念,验证了并行正确的并行程序模型的强连通性、可达性、安全性、活性与可逆性,给出了违背这些性质的可能的因为,并提出使用图的遍历和Petri网模型的T-不变量、可达图/树等算法,对以上性质和错误因为进行检验。　　 并行程序的基础是正确性,由于其的复杂性,对其验证要困难得多,因此要进行建模并验证其性质。将并行程序转换为Petri网系统模型后,证明出相对于并行正确并行程序的Petri网系统模型应当满足的结构性质,包括S不变量、T不变量、强连通性、守恒性以及受控死锁性质,最后举例说明了这些性质在程序验证中的应用。由于这些性质可以事前验证,从而避免了通过动态性质验证会出现状态死锁的问题,因此提高了程序设计效率,同时以上方法具有广泛的可推广性。　　 若用网系统的结构性质进行分析,无需形成可达树/图,这样就避免了可达状态爆炸的问题,从而提高了验证的准确度。由于是从编程角度来证明Petri网模型的性质,因此此方法符合并行程序验证的原理,同时并行程序消息传递的模式有良好的可移植性,因此得到的模型和性质具有普遍的可适用性。　　 本文针对基于Petri网系统模型的并行程序做了一些正确性验证,可以总结为几个方面:　　 1、对当前基于消息传递的并行程序模式,和该模式事实上的编程标准及其所嵌套的C语言,在研究其特性的基础上,给出Petri网系统模型。并给出了并行程序建立模型的方法和步骤。　　 2、讨论了并行程序模型的动态性质(安全性、可逆性、活性、可达性)和结构性质(强连通性、T-不变量、有界性、守恒性)。　　 3、给出了验证算法,并对常见的并行编程错误提出了验证的算法,举出几个验证实例。