基于petri网的列控系统形式化分析方法

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