Please wait a minute...
Welcome to Railway Signalling & Communication Engineering, Today is 中文

Current Issue

  • Formal Modeling and Verification of Point Control System Based on Method B
  • Liu Ning, Han Cheng, Wang Zheng, Hou Xili, Wang Keming
  • 2022 Vol. 19 (6): 5-11. DOI:10.3969/j.issn.1673-4440.2022.06.002
  • Abstract ( ) PDF (1740KB)( )
  • In order to solve the realistic problems such as that the current mainstream validation method for safety critical system cannot prove whether the system exists defects, this paper researches to set up a formalized model for software function logic to achieve the verification of software requirements specification, and finally generate code C by taking the point control system for trackside equipment interlocking control as the specific research object, according to the software requirements specification, aiming at the safety point control system function, and using formal approach to software development method (method B). The research shows that the code C automatically generated by formal model can run normally and meet the software requirements of point control system after passing the verifications of automatic machine proof and manual interactive proof. In this paper, the formal method is applied to the whole process of software development of point control system, the technical route and development method used can effectively improve the safety and reliability of point control system, and reduce the workload in the coding stage, which has important reference significance to the development of other safety critical systems.
Railway Signalling & Communication Engineering
  • 月刊 Monthly
  • 第21卷 第6期 总第期
  • Vol.21 No.6 S.No.
  • 出版: 2024-06-24
  • Published on:
  • 创刊:2004 年
  • First Issue: 2004