软件形式化开发是大型软件开发的主要手段，能够在软件设计初期最大限度的降低错误率，节省开发时间，便于开发人员间的交流，同时还可以提高软件的可信度。形式化方法是在严格的数学基础之上建立的，通过分析、验证发现软件在设计及开发过程中的不完备性和模糊性，在此基础上进行软件实现。形式化方法分为形式化规格说明及验证。Petri网是满足以上要求的很不错的分析描述工具。并发是网络环境的主要特征。并发意指同时、顺序以及无序。描述并发有很多工具，Petri网是其中之一。Petri网具有图形化的特征，简洁直观。可以使用图论的结论作为分析工具，同时Petri网又是形式化的，有着深厚的数学基础，可以对系统的静态结构加以描述，对其动态行为进行分析和验证。在网络环境中，系统不停的在接收着用户的各种操作需求，网络不可能让每个用户都按先后顺序进行操作，处理用户的请求最好采用并发的形式，如此能够最大程度的提高网络资源利用率，在时间效率上满足人们的最大需求与愿望。许多因素可能会影响到网络的传输效率，如可能是系统无法及时处理所有的操作请求。造成请求等待的一个很重要的原因是因竞争资源所致，具体包括：1.全部资源在某个时间段都已经被占用；2.操作申请未到达目标地址；3.响应的请求仍在传输过程中等等。因此网络系统对所有的操作请求有必要进行异步处理。本文的主要工作如下：（1）在带抑制弧的增广Petri网的基础上构造了无冲突并行文件传输网系统模型，结合时间触发子系统准确无误的对整个文件传输的过程进行模拟。利用Petri网的S-不变对系统的一些动态行为进行分析，验证该模型传输的可行性。（2）采用数据交换网络的方式进行文件的发送接收，使得接收和发送间不存在直接关系，避免了因传输双方之一没有传输资源导致的等待困扰，同时引入Petri网的时间和有色概念，利用分层的思想建立了基于扩展有色网的文件传输模型。有效的减少了数据传输的时间，提高网络的通信性能。运用Petri网不变量性质对模型的一些动态行为进行分析、验证，同时利用CPN Tools工具对模型进行仿真验证，为文件传输问题提供了很好的帮助。