随着人们日常工作生活和工业生产的信息化，软件开发的质量越来越受到人们的重视。传统软件开发方法在分析和设计过程中所可能带来的二义性、含糊性、不完整性以及抽象层次混杂的问题，已经愈发难以满足现代软件开发，尤其是安全性要求很高的大型系统的要求，任何微小的软件错误都可能导致生命危险和严重的经济后果。在此背景下，形式化软件开发方法开始受到软件开发人员的重视。形式化软件开发方法带来的好处是不言而喻的，它能够在软件工程的设计雏形阶段最大限度的减少错误，缩短工程的开发时间，能帮助软件开发人员设计出更可靠的系统，而且还方便开发人员之间的交流沟通。形式化方法是严格的建立在数学理论基础之上，通过分析并且验证软件开发流程中的模糊性和不完备性，以达到对软件的各项性能指标进行有效控制的方法。形式化方法分为两个部分：形式化规格说明和形式化验证。Petri网是目前符合上述要求的一种较好的形式化描述工具。列车控制系统将先进的控制技术、通信技术、计算机技术与铁路信号技术有机的联系在了一起，作为保障运营效率和安全的重要手段，列控系统组成单元之多，物理系统构成复杂，规模庞大并且对实时性和可靠性要求都很高,要保障系统的正确运行，需要各个子系统协同配合工作。作为一种形式化描述工具，Petri网建立在严格的数学基础之上，同时具有图形化的特征，简洁直观，易懂易用。虽然大型软件的开发完全实现形式化尚需时日，但是国内外相关领域的工作人员已经做了大量的工作，一些系统的软件开发平台已经投入使用，形式化开发和仿真技术在应用层面上的结合，已经成为未来大型软件开发技术发展的潮流。因此，可以用Petri网对列车控制系统构建模型，然后对其进行分析和验证，用所得到的信息再对列控系统进行评价和改进。通过Petri网开发人员和其它人员得到了一个强有力的平台环境，使得软件开发的过程形式化。论文的主要研究内容是运用Petri网理论构建列控系统在列车不同运行阶段的模型，分为站内调度系统和区间运行系统，站内调度系统又分别对进站调度和到发线调度进行了建模，同时，对列车运行的一些特殊情况，比如信号异常、公路铁路交叉口的运行控制进行了分析；运用Petri网S-不变量性质对模型的一些动态行为进行了分析和验证，对保证列控系统的安全和可靠性起到了很大的作用。