期刊文献+

基于Petri网的列控系统形式化分析方法 被引量:2

Formal analysis approaches of train control system based on Petri nets
下载PDF
导出
摘要 利用原型Petri网对列车控制系统建模难于实现,用带抑止弧的增广Petri网则可以较好地描述问题。将带抑止弧的增广Petri网作为计算模型,对列车控制系统的一些关键问题进行了建模并给出了两个控制子系统:车站调度子系统与区间运行子系统。车站调度子系统实现了对列车请求进入和驶离车站的协调控制,区间运行子系统则实现了闭塞区间的车辆的安全性控制、突发事件时(如遭遇雷击,信号丢失的情况发生等)的安全性处理和公路铁路交叉口的调度等。最后,利用S-不变量对模型的活性、可达性和有界性等给予了形式化的验证。 Formal approaches are construction methods with accurate mathematical semantics,which are based on strict mathematical proofs.Generally,Petri nets are considered as a class of computation models to model the concurrent behavior.Also,formal specifications and analysis of a system can be conveniently developed by Petri nets.However,it is difficult to model a train control system with prototype Petri nets.The difficulties can be solved by extended Petri nets with inhibitor arcs.Hence,some key problems of train control systems were modeled and analyzed by the computation models of extended Petri nets in this paper.Two control sub-systems,station management sub-system and interval operation sub-system.were proposed.The former performed the entering and leaving of trains from stations by cooperative control.The later executed the safety control of block regions in stations,the safety recovery of emergency situations such as lightning stroke and the loss of signals,and the management of railway crossings.Finally,the activity,reachability,and boundedness of the proposed models were analyzed by S-invariants.
出处 《计算机应用》 CSCD 北大核心 2013年第4期1132-1135,1160,共5页 journal of Computer Applications
基金 国家自然科学基金资助项目(60872089) 四川省教育厅应用基础研究项目(09226030)
关键词 PETRI网 抑止弧 列车控制系统 闭塞区间 形式化 Petri net inhibitor arc train control system block section formalization
  • 相关文献

参考文献11

二级参考文献67

共引文献70

同被引文献19

  • 1吴尽昭.多值逻辑定理机器证明的代数方法[J].计算机学报,1996,19(10):773-779. 被引量:5
  • 2HULSHOF P J H, KORTBEEK N, BOUCHERIE R J, et al. Taxo- nomic classification of planning decisions in health care: a review of the state of the art in OR/MS [J]. Health Systems, 2012, 1(2): 129 - 175.
  • 3VUYST S D, BRUNEEL H, FIEMS D. Computationally efficient e- valuation of appointment schedules in health care [ J]. European Journal of Operational Research. 2014, 237(3) : 1142 - 1154.
  • 4DENTON B T, ALAGOZ O, HOLDER A, et al. Medical decision making: open research challenges [ J]. IIE Transactions on Health- care Systems Engineering. 2011, 1(3) : 161 - 167.
  • 5SILVA M, TERUEL E. Petri nets for the design and operation of manufacturing systems [ J]. European Journal of Control, 1997, 3 (3): 182-199.
  • 6VALENTIN V, EMILIA M C, GREGORIO D, et al. A Petri net approach for the design and analysis of Web services choreographies [J]. The Journal of Logic and Algebraic Programming, 2009, 78 (5) : 359 -380.
  • 7GRADISAR D, MUSIC G. Automated Petri-net modeling based on production management data [ J]. Mathematical and Computer Mod- elling of Dynamical Systems, 2007, 13(3) : 267 -290.
  • 8SIMONA B, JAVIER C, JOSE M. Timing-failure risk assessment of UML design using time Petri net bound techniques [ J]. IEEE Transactions on Industrial Informatics, 2011, 7( 1): 90 -104.
  • 9BOWDEN F D J. A brief survey and synthesis of the roles of time in Petri nets [ J]. Mathematical and Computer Modelling, 2000, 31(10-12): 55-68.
  • 10黄小庆,夏安邦.基于有色Petri网和分类服务的Web服务组合模型[J].计算机集成制造系统,2009,15(1):53-62. 被引量:5

引证文献2

二级引证文献4

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部