Abstract: Formal approaches are construction methods with accurate mathematical semantics, which are based on strict mathematical proofs. Generally, Petri nets are considered as a class of computation models to model the concurrent behavior. Also, formal specifications and analysis of a system can be conveniently developed by Petri nets. However, it is difficult to model a train control system with prototype Petri nets. The difficulties can be solved by extended Petri nets with inhibitor arcs. Hence, some key problems of train control systems were modeled and analyzed by the computation models of extended Petri nets in this paper. Two control sub-systems, station management sub-system and interval operation sub-system. were proposed. The former performed the entering and leaving of trains from stations by cooperative control. The later executed the safety control of block regions in stations, the safety recovery of emergency situations such as lightning stroke and the loss of signals, and the management of railway crossings. Finally, the activity, reachability, and boundedness of the proposed models were analyzed by S-invariants.

Key words: Petri net, inhibitor arc, train control system, block section, formalization

摘要： 利用原型Petri网对列车控制系统建模难于实现，用带抑止弧的增广Petri网则可以较好地描述问题。将带抑止弧的增广Petri网作为计算模型，对列车控制系统的一些关键问题进行了建模并给出了两个控制子系统：车站调度子系统与区间运行子系统。车站调度子系统实现了对列车请求进入和驶离车站的协调控制，区间运行子系统则实现了闭塞区间的车辆的安全性控制、突发事件时(如遭遇雷击，信号丢失的情况发生等)的安全性处理和公路铁路交叉口的调度等。最后，利用S-不变量对模型的活性、可达性和有界性等给予了形式化的验证。

关键词: Petri网, 抑止弧, 列车控制系统, 闭塞区间, 形式化