Model-based Development Method Of Signalling Interlocking System For Urban Rail Transit

The computer interlocking system is an important equipment to ensure traffic safety in urban rail transit signal system.As a safety-critical system,interlocking system must meet the safety requirements of the safety integrity level SIL-4,which directly related to people's lives and property security.Using the traditional development method is difficult to find errors and security risks,model-based development method is gradually accepted in safety-critical systems.SCADE(Safety-Critical Application Development Environment)is dedicated to the development of embedded software with high safety requirements,which can reduce the risk of software development,shorten the verification time and reduce the development cost.However,it is difficult to verify because of the difficulty of expressing safety attributes and the large-scale of the safety model.Interlocking functional model based on the moving block has been modeled and simulated under SCADE.And safety analysis and verification method of SCADE interlocking function model based on Fault Tree Analysis(FTA)has been put forward.The main work of this paper includes:(1)Analyzing the structure and function requirements of the urban rail interlocking system.Studing the special route and the requirements of the route control process under the moving block.Realizing the interlocking system functional module design.According to the route state,the route control functional module is divided into routing module,route consistency checking module,route checking module,signal opening module,approach locking module,releasing module and route cancl module;(2)The interlocking functional module based on SCADE is designed and modeled.Focusing on the design of the route control module under the moving block mode.And realizing the control of the multi-train route,turn-back route,automatic route and overlap protection;(3)Proposing FTA-based safety analysis and verification method of interlocking function model basing on the process of formal verification in SCADE and establishing the verification framework of interlocking functional model under SCADE.Based on FTA analyzing the safety of the interlocking functional model,constructing the fault tree model of functional model,which is used as the safety model for formal verification;(4)Building the fault tree of functional model based on Failure Modes Effect Analysis(FMEA).Constructing the fault tree of route control functional module.Taking the route establiment procee as an example,the fault tree model is established to analyze the safety of the route establishment function model.And the effectiveness of the fault tree as a safety model is proved by fault injection.SCADE-based development of interlocking system is benefit to reduce the potential hazards and hidden mistakes during the interlocking software design and development,and the reliability and safety of the interlocking software can be improved.Combined with FTA,the safety of the interlocking functional model has been analyzed and formalized,which embodies the completeness of formal verification.Furthermore,the safety of the model is thoroughly analyzed and the indefinable safety attributes as well as the complexity of the safety model have been avoided.