基于Petri网的全自动无人驾驶列车停站场景形式化建模与验证

为进一步提高全自动无人驾驶系统的安全性，采用Petri网理论在全生命周期早期对系统运营场景的实现流程进行形式化建模与验证。选取正线运营中的列车停站这一典型运营场景，进行对象提取与状态分析，结合各对象与库所、变迁的对应关系，建立Petri网模型，并利用仿真软件PIPE对其有效性和正确性进行形式化验证。针对可能出现的异常情况对模型进行优化，设置车门与站台门开关时序，避免乘客拥挤时出现安全隐患。试验结果表明：建立的Petri网模型有界、安全且无死锁，满足列车停站场景功能需求，模型的可靠性和有效性得以验证，为全自动无人驾驶系统的开发应用与安全分析提供理论支撑。