摘要
在智能轨道交通中,信号系统作为指挥列车安全运行的核心控制系统,在列车运行过程中,控制不当可能导致对人类生命,财产或环境造成灾难性后果。传统的自然语言描述使系统开发缺乏统一的标准,而形式化方法可以有效验证和评估系统设计正确性。文章研究了形式化安全保障技术在智能轨道交通领域的应用,针对全自动驾驶FAO系统中各子系统之间复杂的交互作用,文章结合了形式化方法和STPA方法。以车载ATP系统为例,进行形式化和安全分析方法的结合分析,按照STPA步骤进行安全分析,识别系统相关的安全约束,并运用了XSTAMPP软件辅助分析过程。研究结果实现了自然语言的安全需求到线性时序逻辑(LTL)的形式化规范的转化,有效避免了可能存在的二义性,体现了STPA与形式化结合方面的实际应用价值,并为接下来进行形式化验证提供参考。
In Intelligent Transportation,as the core control system for the safe operation of trains,the signal system may cause disastrous consequences to human life,property or the environment if it is not properly controlled during the train operation.Because the traditional system development is based on natural language description,which may result in different understanding.In contrast,the formalized method can effectively verify and evaluate the correctness of the system design.This paper studies the application of formalized safety assurance technology in the field of Intelligent Transportation.Aiming at the complex interactions among subsystems in Fully Automatic Operation(FAO)system,this paper combines the formalized method with the System-Theoretic Process Analysis(STPA).Taking ATP system as an example,this paper combines formal analysis with safety analysis methods,carries out safety analysis according to STPA steps,identifies safety constraints related to the system,and uses XSTAMPP software to assist the analysis process.The results prove that the safety requirements obtained from the analysis can be translated into the formal specification of Linear Temporal Logic(LTL)which effectively avoid the possible ambiguity.The study reflects the practical application value of the combination of STPA and formal method,and provides a reference for the following formal verification.
出处
《科技创新与应用》
2021年第3期175-178,共4页
Technology Innovation and Application
