期刊文献+

CTCS-4无线通信故障恢复模型的形式化研究

Research on Fault Recovery Modeling of CTCS-4 Wireless Communication System
下载PDF
导出
摘要 对CTCS-4的无线通信系统的故障恢复模型进行了研究,使用Event-B对CTCS-4无线通信系统的故障恢复过程进行建模.通过证明义务对模型的逻辑正确性和完备性进行验证,证明其可以满足要求. The fault recovery model of CTCS-4 wireless communication system is studied, and the model of fault recovery process of wireless communication system is built with Event-B. The model's logical correctness and completeness are verified by proof obligations to proof it can meet the requirements.
出处 《兰州交通大学学报》 CAS 2013年第1期68-72,共5页 Journal of Lanzhou Jiaotong University
基金 国家自然科学基金(61163009)
关键词 CTCS-4 EVENT-B GSM-R 证明义务 CTCS-4 Event-B GSM-R proof obligation
  • 相关文献

参考文献5

  • 1Zimmermann A. Hommel G-A train control system case study in model-based real time system design. Proc of International Parallel and Distributed Process- ing Symposium Nice, IEEE Computer Society, 2003: 118-130.
  • 2徐田华,赵红礼,唐涛.基于有色Petri网的ETCS无线通信可靠性分析[J].铁道学报,2008,30(1):38-42. 被引量:28
  • 3贾毓杰.铁道信号与通信设备[M].北京:中国铁道出版社,2007.
  • 4钟章队,艾渤,刘秋妍,等.铁路数字移动通信系统GSM-R应用基础理论[M].北京:清华大学出版社,2009.
  • 5当代中国铁路信号2001-2005编委会.当代中国铁路信号2001-2005[M].北京:中国铁道出版社,2007.

二级参考文献6

  • 1Armin Z , Gunter H. A train control system case study in model-based real time system design [C]// International parallel and distributed processing symposium, IEEE, 2003, 118-126.
  • 2Holger H , David N J, Yaroslav S U. A Comparative Reliability Analysis of ETCS Train Radio Communications [R]//AVACS Technical Report No. 2. Berlin: Olderog University. 2005.
  • 3Jensen K. Coloured Petri Nets Basic Concepts, Analysis Method and Practical Use (Vol. 1-3) [M].Becond Edition. Berlin: Springer-Verlag, 1997.
  • 4Design/CPN Online [EB/OL]. http://www. daimi. au. dk/designCPN/, 1996.
  • 5Euroradio FFFIS : class 1 requirements [EB/OL]. http:// www. aeif. org/db/docs/ccm/SUBSET-052 v200. PDF, 2000.
  • 6Euroradio FFFIS : class 1 requirements [EB/OL]. http:// www. aeif. org/db/docs/ccm/SUBSET-093 v230. PDF, 2003.

共引文献28

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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