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

Verification of computer interlocking route module by Petri net based on UML modeling

作　　者：薛丰[1] 杨扬[1] 谢林[1] XUE Feng;YANG Yang;XIE Lin(School of Information Science and Technology, Southwest Jiaotong University, Chengdu 611756, China)

机构地区：[1]西南交通大学信息科学与技术学院,成都611756

出　　处：《铁路计算机应用》2017年第4期10-14,共5页Railway Computer Application

摘　　要：对于铁路车站计算机联锁软件中的重要部分之一的进路模块,使用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.

关 键 词：车站联锁 UML PETRI网 建模 

分 类 号：U284.3[交通运输工程—交通信息工程及控制] TP39[交通运输工程—道路与铁道工程]