大型系统的设计应该采用形式化(Formal Methods)的方法。形式化方法是建立在严格数学基础上,具有精确数学语义的开发方法。形式化技术具有改善系统开发质量和提高工程效率的潜能,在系统的开发过程中具有十分重要的作用。Petri网特别适合描述系统顺序、并发、冲突以及同步等现象。作为一种系统的描述工具,Petri网不仅可以刻画系统的静态结构,而且可以分析系统的动态行为。Petri网既有直观的图形表示,又有深刻的数学内涵和基础,可以利用许多数学的方法对模型验证,所以, Petri网是形式化大型系统开发的有效工具之一。并发是计算机网络的基本特性,网络中的节点可能会频繁地传输文件数据,这些文件传输的顺序是无法确定的,文件传输的资源调度是一项有意义的工作。本文对Gnutella文件共享系统以及并行文件传输分别提出了可行的解决方案：(1)采用扩展有色Petri网构建了一个Gnutella文件共享系统模型,很好的实现了一对一、一对多模型的消息处理和数据处理。然后,应用CPN Tools工具对其服务流程进行模拟仿真,并分析系统的行为。最后,针对多个节点拥有同一文件以及节点的频繁离线情况,将节点的带宽和节点的传输服务质量综合考虑提出了一种带优先级的并行文件传输方案,从而有效降低节点离线情况带来的影响,减少文件传输时间,并能有效实现系统整体的负载均衡,提高系统的整体性能。(2)采用Petri网对并行文件传输的过程进行建模,将时间作为变迁发生的一种消耗性资源,可以直观的描述出文件传输的时间,有利于文件传输的分析。最后,利用Petri网中的不变量性质对模型的一些动态行为进行了分析,验证了该模型的合理性与准确性。