Petri网不仅可以采用可视化图形描述而且可被形式化的数学方法所支持,是一种形式化、图形化的分布式系统建模和分析工具。它不但能够精确地分析系统的静态特性,而且能够很好地分析系统的动态行为性质,从而很好地刻画系统的动态行为、分析系统的性能。它既可采用形式化直观的图形表示,又可以引入许多数学方法对其性质进行分析与验证。目前,大多数的软件系统都是并发系统,并发是衡量系统运行效率高低的一个参数标准。为了达到“事半功倍”的效果,现在的系统环境越来越需要并发,只有这样才能更好地利用系统资源环境,才能使一个系统具有更强的竞争力。Petri网作为一个优秀的形式化描述和分析工具,能很好地描述和分析这类系统。采用软件形式化技术,不仅有利于开发人员之间的沟通,提高软件的可靠性,而且可以尽可能地缩短开发的总体时间,减少软件设计早期阶段的错误。本文的主要工作如下:(1)在Petri网下对哲学家就餐问题模型进行了分析。哲学家就餐问题是描述在共享资源下同步与并发的经典案例,活性与无饥饿性是求解此问题的前提,效率是基本要求。由于对资源的竞争使几个哲学家不可能同时处于就餐状态,在考虑公平性的情况下定义了延迟Petri网(delayed Petri net)的概念。解决了竞争资源引起的冲突,并提高了就餐的效率。(2)Petri网下对信道复用的建模与改进。解决了用户要求通信且被要求的用户也空闲,但信道被占用;几个用户同时向另外几个用户请求通信时,而另几个用户正在通信中。考虑到信道的利用率及对共享资源带来的冲突,本章采用栈技术对这一问题进行了分析与验证,提出了一个应用性更强,应用范围更广的Petri网模型。