基于UML建模的计算机联锁进路模块Petri网验证

摘要

对于铁路车站计算机联锁软件中的重要部分之一的进路模块,使用UML对其进行建模.针对UML没有精确语义、缺少模型分析和验证手段不足的缺点,利用具有严格理论分析方法的Petri网对模型进行形式化验证,保证模型的精确性和安全性.%Route module is one of the important parts in railway station computer interlocking software, it can be modeled by using UML. For disadvantages that UML is lack of precise semantics, lack of model analysis and validation methods, Petri net, which has strict theoretical analysis method, was used to formal verifying for the module, ensure the accuracy and security of the module.