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

详细信息

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

School of Information Science and Technology, Southwest Jiaotong University, Chengdu 611756, China

摘要: 对于铁路车站计算机联锁软件中的重要部分之一的进路模块，使用UML对其进行建模。针对UML没有精确语义、缺少模型分析和验证手段不足的缺点，利用具有严格理论分析方法的Petri网对模型进行形式化验证，保证模型的精确性和安全性。
- 车站联锁 /
- UML /
- Petri网 /
- 建模
Abstract: 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.
- station interlocking /
- UML /
- Petri net /
- modeling

[1]	林瑜筠, 吕永昌. 计算机联锁[M]. 北京：中国铁道出版社,2013.
[2]	韦启盟. 计算机联锁软件仿真测试系统的研究与实现[D].成都：西南交通大学, 2008.
[3]	Grady Booch, James Rumbaugh, Ivar Jacobson. UML 用户指南[M] . 邵维忠，译. 北京：人民邮电出版社, 2013.
[4]	Peterson J L. Petri Net Theory and the Modelling of Systems[M]. Prentice Hall, 1981.
[5]	杨扬. 车站信号控制系统[M]. 成都：西南交通大学出版社,2012.
[6]	周长红. UML 图的Petri 网建模[D]. 济南：山东科技大学,2004.
[7]	杨扬, 潘明, 何梅芳. 联锁软件的Petri 网形式化定义[J].北京：中国铁道科学, 2002, 23（3）： 49-54.
[8]	Mustafa S.Durmus, Ugur Yildirim, Mehmet T.Soylemez. Automatic Generation of Petri Net Supervisors for Railway Interlocking Design[C]. Australian Control Conference, 2012.