基于时间有色Petri网的计算机联锁系统建模

摘要

随着我国铁路的快速发展，对提高铁路系统的安全性和可靠性需求日益增加。尤其是铁路计算机联锁系统，它作为一种实时的安全苛求系统，对实现铁路的安全高效运行发挥着至关重要的作用。目前，我国正在大力修建多条铁路新建线，并完成对旧线的强化改造。为了能够评估这些铁路线上相应车站的性能，需要寻找合适的工具和技术来确定这些铁路车站的控制质量。同时为满足CENELEC(EuropeanCommitteeforElectrotechnicalStandardization，欧洲电工标准化委员会)标准的要求，设计者需要确保联锁系统能够实现可靠安全的系统性能。本文就是基于此目的着手建立计算机联锁系统模型，以减少开发时间和提高系统可靠性。
　　Petri网是目前使用的最广泛的建模方法，它为设计人员提供了简单的错误跟踪和可视化功能。Petri网作为一种图形化建模语言，已被证明能为各种有复杂依赖关系和真正并发的实时系统建模提供良好的形式化框架。因此，本文使用ITCPN(IntervalTimedColouredPetriNets，区间时间有色Petri网)来对铁路车站计算机联锁系统进行建模和分析。
　　ITCPN是一种有色Petri网在时间上的延长，在令牌和变迁上的时间决定了每一个令牌产生的延迟，这种延迟是由一个上下界指定的时间间隔。ITCPN模型允许大型复杂系统的动态行为建模，例如本文中对铁路联锁系统的建模和分析。因此本文针对一个简单的铁路站场，采用ITCPN对计算机联锁系统进行建模，开发一个满足需求标准的计算机联锁系统模型，并对联锁系统组件（信号，道岔和轨道电路等）进行建模，以及对进路办理和进路解锁过程建模，在此基础上对部分模型进行形式化分析，以便能够丰富车站联锁系统的建模和分析能力。
　　结果表明，采用ITCPN描述方法对计算机联锁系统进行形式化定义、建模和分析，可以用来评估车站的运行情况和联锁设备情况，减少联锁系统中的不确定性因素，消除系统死锁等情况。通过该模型可以有效的降低联锁软件的复杂性，保证联锁软件的正确性。这在系统开发的早期阶段，对联锁系统进行建模和仿真来确认系统的可行性是非常适合的。而在系统开发阶段，使用形式化模型对特定属性进行形式化分析和验证也是合适的。通过对模型的具体分析，可以以抽象的方式验证模型的特定属性。因此，在联锁系统设计和开发阶段，采用ITCPN对联锁系统组件和逻辑过程进行建模和形式化分析是非常必要的。

目录

声明

摘要

1 绪论

1．1 选题背景及意义

1．2 国内外研究动态

1．2．1 Petri网应用

1．2．2 计算机联锁系统

1．2．3 计算机联锁系统建模

1．3 研究目的及研究内容

2 Petri网基本理论

2．1 基本Petri网定义

2．1．1 基本Petri网概念

2．2．2 Petri网的发射规律

2．2．3 Petri网的性质

2．3 有色Petri网

2．4 时间Petri网

3 ITCPN理论

3．1 ITCPN介绍

3．2 ITCPN定义

3．2．1 ITCPN的动态行为

3．2．2 ITCPN的模型举例

3．3 ITCPN分析方法

4 计算机联锁系统组件建模

4．1 计算机联锁系统组成

4．2 道岔的建模

4．3 信号的建模

4．4 轨道区段的建模

5 计算机联锁系统过程建模

5．1 计算机联锁系统模型假设

5．2 进路建立的ITCPN模型

5．3 进路解锁的ITCPN模型

5．3 模型分析

结论

致谢

参考文献

攻读学位期间的研究成果