Petri⽹预备知识
死锁产⽣原因
（1）互斥：同时争夺唯⼀资源
（2）占⽤且等待
（3）⽆抢占
（4）循环等待
死锁产⽣的原因及四个必要条件
产⽣死锁的原因主要是：
（1）因为系统资源不⾜。
（2）进程运⾏推进的顺序不合适。
（3）资源分配不当等。
如果系统资源充⾜，进程的资源请求都能够得到满⾜，死锁出现的可能性就很低，否则
就会因争夺有限的资源⽽陷⼊死锁。其次，进程运⾏推进顺序与速度不同，也可能产⽣死锁。产⽣死锁的四个必要条件：
（1）互斥条件：⼀个资源每次只能被⼀个进程使⽤。这个资源只能是空闲待⽤或者分配给确定的任务，不可被两个或两个以上任务同时使⽤。
（2）请求与保持条件：⼀个进程因请求资源⽽阻塞时，对已获得的资源保持不放，更导致其他进程想获得资源⽽得不到资源，更导致进程瘫痪。
（3）不剥夺条件:进程已获得的资源，在末使⽤完之前，不能强⾏剥夺。只有当正在使⽤这个资源的任务进程结束后，此资源才能被释放，被其他任务占⽤。
（4）循环等待条件:若⼲进程之间形成⼀种头尾相接的循环等待资源关系。
这四个条件是死锁的必要条件，只要系统发⽣死锁，这些条件必然成⽴，⽽只要上述条件之⼀不满⾜，就不会发⽣死锁。
死锁的解除与预防：
理解了死锁的原因，尤其是产⽣死锁的四个必要条件，就可以最⼤可能地避免、预防和
解除死锁。所以，在系统设计、进程调度等⽅⾯注意如何不让这四个必要条件成⽴，如何确定资源的合理分配算法，避免进程永久占据系统资源。此外，也要防⽌进程在处于等待状态的情况下占⽤资源。因此，对资源的分配要给予合理的规划。
因此，前三个条件通常是满⾜的，⽽第四个条件可因资源的请求、分配和释放等因素，随时间⽽变化。只要发⽣死锁，这四个条件必然都满⾜。反之，只要有⼀个条件不满⾜，系统就不会发⽣死锁。因此想要控制系统死锁的发⽣，必须破坏第四个条件即循环等待条件。Petri⽹建模优势
对系统中的并发、资源共享、冲突、相互抑制以及⾮确定性等有简单表⽰；
（1）可以使⽤⾃顶向下和⾃底向上的设计⽅法，使系统具有不同的抽象层次；
Petri网原理
（The Theory of Petri Net）
学分数3 周学时 3
课程性质：计算机科学与技术选修课
预修课程：集合论与图论，代数结构与数理逻辑
教学目的：通过本课程的教学，使学生掌握Petri网原理的基本内容，并对采用Petri网进行系统模拟以及在描述同步和拓扑等方面的思想和方法深入理解和体会，初步培养学生通过Petri网来解决问题的能力。
基本内容：Petri网系统和通用网论
基本要求：学生应按本大纲具体要求，理解Petri网原理的基本概念和基本理论，掌握采用Petri网进行系统模拟以及在描述同步和拓扑等方面的思想和方法，并能综合运用所学的知识通过Petri网来分析和解决简单的实际问题。
教学用书：《Petri网原理》，袁崇义，电子工业出版社，1998年
参考书：
[1] T. Murata. Petri Nets: Properties, Analysis and Applications. Proceedings of the IEEE, Vol. 77,
No 4, April, 1989, pp. 541-580.
[2] W. Reisig, Petri Nets, An Introduction. EATCS, Monographs on Theoretical Computer Science,
W.Brauer, G. Rozenberg, A. Salomaa (Eds.), Springer Verlag, Berlin, 1985.
[3] C. Girault, R. Valk. Petri Nets for Systems Engineering: A Guide to Modeling, Verification,
and Applications. Springer-Verlag, 2002, ISBN: 3-540-41217-4.
１０００—９８２５／２００２／１３（０８）１６９８—０７ ０２００２ Ｊｏｕｒｎａｌ ｏｆ Ｓｏｆｔｗａｒｅ软件学报 Ｖｏ１．１３，Ｎｏ．８
网上证券交易系统的时序Ｐｅｔｒｉ网描述及验证
杜玉越１，２，３，蒋昌俊
。（同济大学计算机科学与工程系，上海２０００９２）；
（聊城师范学院计算机科学系，山东聊城２５２０５９）；
（中国科学院软件研究所计算机科学重点实验室，北京 １０００８０）
Ｅ—ｍａｉｌ：ｙｙｄｕ００１＠１６３．ｃｏｍ；ｃｊｊ＂ｉａｎｇ＠ｏｎｌｉｎｅ．ｓｈ．ｃａ
ｈｔｔｐ：／／ｗｗｗ．ｔｏｎｇｊｉ．ｅｄｕ．ｃａ
摘要：基于时序Ｐｅｔｒｉ网对我国现行网上静态和动态证券交易系统进行了模拟、形式描述及功能正确性验证．
应用时序逻辑推理规则，从形式上严格证明了证券交易系统需求规范及其时序Ｐｅｔｒｉ网模型动态行为的一致性．
结果表明．时序Ｐｅｔｒｉ网能够清楚而简单地描述事件间的因果关系和时序关系以及并发系统中某些与时间有关
的重要性质，如最终性和公平性．因此，时序Ｐｅｔｒｉ网可作为并发系统形式化描述和分析的有力工具．
关键词：模型检查；证券交易系统；时序逻辑；Ｐｅｔｒｉ网；形式描述；正确性验证；电子商务
中图法分类号：ＴＰ３ｌｌ 文献标识码：Ａ
网上证券交易具有公平性、速度快等特点，因此越来越受到众多券商和股民的青睐．它也是电子商务中最
早实现电子数据交换的重要领域之一．但是与传统的证券交易方式相比，在线证券交易系统需要更高的安全性
和可靠性．其安全性通过数据加密技术和数字签名技术来实现，可靠性反映了交易数据的有效性、公平性及交
易撮合过程的正确性．在证券交易系统中，股民申报的交易数据，先由所委托的券商验证交易数据的有效性，再
由券商处理系统将验证后的有效数据发送到相应的交易所，最后在交易所前置机中记录交易数据的到达时间，
把它们按其所属股票进行分类，并输送到交易机进行撮合处理．
任何采用非形式化设计方法产生的交易协议，都需要进行分析和校验，以确保协议规范和其服务规范的一
丁技术 ： ！ ＳＣＩＬＮＣＩ＆Ｉ ＬＣＨＮＯＩ ＯＧＹ ＩＮＩ ＯＲＭＡ Ｉ ＩＯＮ
Ｐｅｔｒｉ网应用研究
王志坚 （广东商学院信息学院广州５１ ０３２０）
摘要：本文介绍了Ｐｅｔｒｉ网的基本概念及其发展，以及Ｐｅｔｒｉ网的研究方向，讨论ｒ Ｐｅｔｒｉ网与面向对象技术的结合，以及Ｐｅｔｒｉ
网在ＣＩＭＳ领域里的应用研究。 关键词：Ｐｅｔｒｉ网 面向对象技术 ＣＩＭＳ 中图分类号：ＴＰ３１９ 文献标识码：Ａ
１．Ｐｅｔｒｉ网 Ｐｅｔｒｉ网是由德国的ｃ．Ａ．Ｐｅｔｒｉ教授首先提出的一种计算模
型，现以证明在引入禁止符以后，其模型能力与图灵机等价。
Ｐｅｔｒｉ网从图形上看由四种不同类型的元素组成，即库所、变迁、
连接库所和变迂的有向弧及位于库所中的托肯。其中库所与资
源、步及条件相对应，库所中有托肯则表示某种资源可用、进程
执行到某步或某个条件被满足。变迁对应于事件或操作，变迁触
发则对应于事件的发生。一个变迁能触发当且仅当它的所有输入
库所中有相应数量的托肯，即满足对应事件的发生条件。变迁触
发后，每个输入库所被移去相应数量的托肯，而每个输出库所则
产生相应数量的新托肯，以表示事件的发生引起系统的状态变
化，而形成新的条件。在Ｐｅｔｒｉ网中，系统的状态是通过托肯在
所有库所中的数量分布来表示的，系统状态演变反映为托肯在库
所间的流动。
２．Ｐｅｔｒｉ网的研究
Ｐｅｔｒｉ网的研究已经由最初的Ｐ／Ｔ网等基本网不断深入，在
网络的种类、特性、分析、工具等众多方面都取得了长足的进展。 概括起来，近年来国内外关于Ｐｅｔｒｉ网的研究主要集中在以下几
个方面。
２．１降低模型的复杂程度：谓词网、着色网等一系列高级
Ｐｅｔｒｉ网先后提出，网络模型显著地简化了。在高级Ｐｅｔｒｉ网中，
模型的简化抽象过程是通过抽取共同点来完成的，相同子结构的
重叠或用一个子结构来代表几个子结构成为简化模型的基本方
法。这样的高级Ｐｅｔｒｉ网已经适合分布、并行和具有同构子结构
