随着3C技术(计算机技术、通信技术、控制技术)的不断发展和计算机联锁技术的成熟,铁路行业越来越多地使用计算机联锁来替代电气集中控制。铁路运输涉及到人身安全和财产损失,对安全性和可靠性的要求十分高,这就对计算机联锁的安全性和可靠性提出了很高的要求,计算机联锁软件一旦失效将会造成重大的生命财产损失。如何提高计算机联锁软件的安全性和可靠性,成为了计算机联锁设计者们不断思考和研究的课题。为了提高计算机联锁软件的安全性和可靠性,开发者们必须在软件开发的前期对软件的可靠性进行分析和验证。通常在软件开发前期,对软件进行建模,并对模型进行验证。常用的建模方式有结构化建模、形式化建模、面向对象的建模、UML建模等,各个建模方法各有其优缺点,本论文主要采用形式化建模方法。对于结构化方法等利用自然语言对软件建立的模型,由于自然语言可能存在的二义性,容易使开发者的理解出现偏差,会给软件的后期开发带来严重的问题。而形式化方法是用数学语言来描述模型,具有结构严谨、无二义性等优点,便于实现设计,同时也可以提高软件的可靠性。petri网是一种常用形式化建模方法,具有直观易懂的优点。通过对软件需求和规则的分析之后,用petri网建立它的数学模型,并用petri网独有的验证方法对其分析验证,为开发人员及时发现软件的缺陷提供了极大的帮助。本论文采用CPN(有色petri网)对计算机联锁软件进行建模和分析。CPN可以对模拟量系统和离散量系统建模,有色petri网给不同属性的托肯染上不同的颜色,在有色petri网中用一种染色的托肯来代表一种行为特征。它的颜色集可以是离散值或者连续值。对建立的模型可以用CPN专门的仿真工具CPN TOOLS进行仿真,以此来分析所建模型是否存在死锁等性质。本论文首先介绍了计算机联锁系统的结构、功能,以及计算机联锁软件可靠性的设计要求,提出了用形式化方法对计算机联锁软件进行建模的优越性。然后介绍了形式化建模语言petri网的定义和建模方法。接着采用CPN对计算机联锁软件中的主要设备道岔、轨道区段、信号机进行了建模,并根据计算机联锁软件进路处理的规则,对计算机联锁软件的进路处理进行了建模。最后通过CPN TOOLS仿真、状态空间报告、可达数方法和关联矩阵方法对所建进路模型的性质进行了全面的分析和验证。结果表明,利用CPN所建立的模型满足模型设计的要求,证明了所建立模型的可靠性。因此,在保证计算机联锁软件可靠性方面采用CPN建模是一种十分有效的方法。