一种基于场景模型的安全性分析算法研究

Study on Safety Analysis Algorithm based on Scenario Model

为了确保安全苛求系统的安全性,其开发过程中必须使用安全性分析技术。传统的安全性分析方法需要花费大量的时间和精力,分析的完整性和一致性难以保障,分析结果易于出错。本文提出一种基于场景模型的安全性分析算法,该算法从基于UML时序图的需求描述出发,生成系统的形式化模型,通过故障自动注入与形式化模型扩展,采用扩展的启发式广义büchi自动机判空检测算法自动验证与分析系统的安全性。通过铁路车站联锁系统中基本进路建立的安全性分析实例,验证了该方法的正确性与实际可行性。与已有的安全性分析方法相比,本文提出的方法从效率和安全质量方面改善了安全苛求软件的设计与开发,为安全苛求系统的安全性保障与安全评估提供了有力的技术支撑。

In order to ensure the safety of the safety-critical system,the safety analysis technology shall be adopted in development of the safety-critical system.The conventional safety analysis methods are labor intensive and time consuming are hard to guarantee analysis integrity and consistency and are easy to generate erroneous results.In this paper,we proposed the safety analysis algorithm based on the scenario model to resolve the problems of the conventional methods.With the proporsed algorithm,we built the FSP（Finite State Processes） process algebra models for the system and its components from UML sequence diagrams and domain knowledge,injected faults from the existing failure mode library to the formalized model of the system and acquired the extended formal models with failure behaviors automatically.We adopted the heuristic empty check algorithm with the extended generalized büchi automata to analyze and verify system safety automatically.As case study,safety analysis on establishment of receiving and sending routes in the railway station interlocking system proves the feasibility and correctness of the proposed method.Compared with the traditional methods,the proposed method improves the design and development of safety-critical software in respect of efficiency and quality and provides strong technical support to safety guarantee and evaluation of safety-critical computer systems.