用有色Petri网建立铁路联锁表模型的经验
Experience using Coloured Petri Nets to Model Railway Interlocking Tables
摘要：
联锁表是定义允许训练通过的进路的功能规范。与路由相关的所有相关信号设备的状态和动作也被指定。众所周知，联锁表的设计和校验是劳动密集型的、繁琐的并且容易出错。为了帮助验证过程和快速检测错误，我们正式建模和分析联锁表使用有色Petri网（CPNs）。虽然大型联锁表可以很容易地建模，分析模型是相当困难的，由于状态爆炸问题和不希望的安全死锁。安全的死锁是当没有训练碰撞，但训练交通不能继续前进。为了便于分析，我们将自动进路设置和自动取消进路功能纳入模型。这有助于减少死锁的数量。我们还利用CPN工具的新功能;优先转换;抑制弧;和重置弧。这有助于减少状态空间的大小。我们还包括一个故障安全规格称为侧翼保护到联锁模型。
英文摘要：
Interlocking tables are the functional specification defining the routes on which the passage of the train is allowed. Associated with the route, the states and actions of all related signalling equipment are also specified. It is well-known that designing and verifying the interlocking tables are labour intensive, tedious and prone to errors. To assist the verification process and detect errors rapidly, we formally model and analyse the interlocking tables using Coloured Petri Nets (CPNs). Although a large interlocking table can be easily modelled, analysing the model is rather difficult due to the state explosion problem and undesired safe deadlocks. The safe deadlocks are when no train collides but the train traffic cannot proceed any further. For ease of analysis we incorporate automatic route setting and automatic route cancelling functions into the model. These help reducing the number of the deadlocks. We also exploit the new features of CPN Tools; prioritized transitions; inhibitor arcs; and reset arcs. These help reducing the size of the state spaces. We also include a fail safe specification called flank protection into the interlocking model.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
