随着计算机软件的飞速发展，提高软件开发的效率已成为一个非常重要的问题。采用形式化开发方法，不仅可以极大地减少软件设计早期的错误，缩短开发的总体时间，而且有利于开发人员之间的沟通，提高软件的可靠性。Petri网是形式化软件开发的重要方法之一。Petri网是一种对系统软件形式化、图形化的描述和分析工具，具有直观、易懂和易用的优点。对于具有并发、异步、分布、并行、不确定和随机性的离散事件动态系统，都可以利用这种工具构建模型。通过对模型的进一步分析，即可得到有关系统静态结构和动态行为方面的信息，根据这些信息可以对要开发的系统进行评价和改进。本文着重研究了Petri网的建模方法、分析技术及其在路由搜索算法中的应用，列出了目前该领域有待解决的一些问题，取得的主要研究结论如下：第一，从理论上分析了不可见任务的功能，针对相应的类别给出检测方法，提出从日志中挖掘包含不可见任务工作流网的α#算法，该算法突破了对不可见任务的挖掘盲区，并已作为挖掘插件实现到开源的进程挖掘框架ProM当中，通过编写大量的人造日志并收集企业的实际日志，对算法进行了全面的实验评估。文章还对建模的另一个核心环节，建模语言进行了研究。针对BPMN目前存在较多模糊语法的情况，提出将BPMN转换成YAWL语言。转换不仅可令YAWL的分析工具和工作流引擎为BPMN服务，而且严格的YAWL语义能帮助BPMN消除二义性，有利于BPMN规范的进一步完善和改进。第二，分析了目前现有的各种Petri网化简方法，首次将逻辑电路中成熟的技术应用在Petri网中，提出了一种新的基于逻辑代数的化简算法，将化简单位从单个元素扩展到无圈子网，提高了化简效率，并扩充了化简范围。本文还利用结构理论解决了结构活网到活系统的极小标识求解算法，并对Petri网的一类特殊性质：空标识可再生性进行了求证，解决了空标识可再生网在运算中的保持条件。这些结论在进程挖掘领域具有广阔的应用前景。第三，提出了一种融合P2P和CDN优点的新型网络架构，将Petri网技术与蚁群算法相结合，给出了新型网络的最优选径算法。实验表明该模型及路由算法具有较高的稳定性和鲁棒性。