期刊文献+

基于Event-B的联锁进路控制建模验证方法研究 被引量:2

Research on Event-B based modeling and verification of interlocking route control
下载PDF
导出
摘要 计算机联锁系统具有典型的安全苛求特性。传统的联锁软件开发方法难以完整准确地定义需求,单纯依靠测试也无法发现软件中的所有错误,使软件在功能完整性和安全性方面难以得到保证。本文利用形式化Event-B方法和相关工具对联锁系统的核心功能—进路控制的相关功能需求和安全需求进行了建模、精化和验证,对开发高安全苛求和高可靠性的联锁软件提供了新的方法借鉴。 Computer Interlocking System was a safety critical system. Traditional development method for interlocking software couldn't ensure the completeness and safety of software function. The all errors couldn't be found by test. This paper used Event-B formalization method and relative tools to build models for the core function of interlocking---concerning its function requirement and safety requirement of route control, refined and proved the models. This method provided a new way of developing interlocking software.
出处 《铁路计算机应用》 2013年第6期57-61,共5页 Railway Computer Application
关键词 联锁 进路控制 Event-B建模 形式化方法 interlocking route control Event-B modeling formalization method
  • 相关文献

参考文献5

  • 1Eugenio Roanes-Lozano, Antonio Hernando, Jose Antonio Alonso, Luis M. Laita. A logic approach to decision taking in a railway interlocking system using Maple[J]. Mathematics and Computers in Simulation, Volume 82, Issue 1, September 2011, Pages 15-28.
  • 2Khan, S.A.; Zafar, N.A.Towards the formalization of railway interlocking system using Z-notations[C]. 2nd In-ternational Conference on Computer, Control and Communication, vol., no., pp.1-6, 17-18 Feb. 2009.
  • 3王铁江,郦萌.计算机联锁软件的Z规格说明[J].铁道学报,2003,25(4):62-66. 被引量:7
  • 4陈邦兴,吴芳美.铁路信号联锁逻辑形式化建模研究[J].铁道学报,2002,24(6):50-54. 被引量:24
  • 5Jean-Raymond Abrial. Modeling in Event-B[C]. Cambridge University Press, 2010.

二级参考文献11

  • 1陈邦兴,吴芳美.铁路信号控制逻辑的有色Petri网描述方法[J].铁道学报,2001,23(z1):54-58. 被引量:4
  • 2Hasen K M. Linking Safety Analysis to Software Requirements: Exemplified by Railway Interlocking Systems[D].Institute for Information Technology, Denmarks Tekniske University. 1996.
  • 3Wong W. A simple graph theory and its application in railway signaling[A]. In: M. Archer, J.J. Joyce, K. N.Levitt, P. J. Windley ed. International Workshop on Higher Order Logic Theorem Proving its Applications[C].New York: IEEE CS Press, 1991. 395--410.
  • 4Monigel M. Formal representation of track topologies by double vertex graphs[A]. In: Proceedings of the Railcomp92-Computers in Railways[C]. New York: Computational Mechanics Publications, 1992.
  • 5Guiho G, Hennebert C. SACEM software validation[A].In: Proeeedings of the 12th International Conferenee on Software Engineering[C]. New York: IEEE CS Press/ACM Press, 1990. 186--191.
  • 6Jacky J. Specifying a safety-critical control system in Z[J].IEEE Transaction on software engineering. 1995, 21 (2)99--106.
  • 7Johnson C W. Using Z to support the design of interactive safety-critical systems [J]. Software engineering journal.1995, 10(2): 49--60.
  • 8Hall P A. Relationship Between Specification and Testing [J]. Information and Software Technology, 1991,33 (1) : 47--52.
  • 9Hall P A. Towards Testing with Respect to Formal Specification[A]. In: Second IEE/BCS Conference on Software Engineering[C]. New York.. IEEE Press. 1988. 159--163.
  • 10兰毓华,毛法尧,曹化工.基于Z规格说明的软件测试用例自动生成[J].计算机学报,1999,22(9):963-969. 被引量:22

共引文献29

同被引文献4

引证文献2

二级引证文献5

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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