一个基于形式化方法的系统安全性建模分析实例研究  

Case Study of Formal Model Based System Safety Modeling Analysis

作　　者：石梦烨 胡军[1,2] 陈朔 唐红英 王立松 SHI Meng-ye;HU Jun;CHEN Shuo;TANG Hong-ying;WANG Li-song(Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China;Collaborative Innovation Center of Novel Software Technology and Industrialization,Nanjing 211106,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京211106 [2]软件新技术与产业化协同创新中心,南京211106

出　　处：《小型微型计算机系统》2020年第2期327-332,共6页Journal of Chinese Computer Systems

基　　金：南京航空航天大学研究生创新基地(实验室)开放基金项目(kfjj20181607)资助.

摘　　要：随着安全关键性系统的日益复杂,如何提高安全关键系统的安全性成为急需解决的问题.基于形式化模型的复杂系统设计与分析是一种重要的安全性分析方法.本文工作对AIR6110标准中的机轮刹车实例系统进行了基于形式化方法的安全性分析研究,包括:在系统模型设计层级对机轮刹车系统(WBS)的架构进行层次化分析,将自然语言描述的WBS系统功能用形式化语言(AADL的子集SLIM)进行严格的建模描述,消除AIR6110标准中自然语言描述存在的需求语义的二义性,从而建立了WBS系统的形式化模型;考虑系统可能发生的故障并设计多种类的故障模式,基于这些故障模式对建立的形式化功能模型进行失效行为语义的扩展,然后对获得的扩展系统模型进行安全性分析.实例分析论证了基于模型的安全性分析方法在工业系统中的有效性和实用性.With the increasing complexity of safety-critical systems,it’s a great challenge to improve the safety during the stage of system designs. Model based complex system design and formal analysis are an important system safety modelling and analysis methodology.In this paper,a case study is given to show how to apply this method into aerospace industry,that is,a Wheel Brake System( WBS)( which is a typical safety-critical sample system adopted in an aviation standard SAE-AIR6110) is used for demonstration of modelling and formal analysis. In AIR6110 standard,the requirement semantics described by natural language are ambiguous. Therefore,it is necessary to eliminate the ambiguity and establish a formal model of WBS system firstly,including: the structure of WBS is analyzed hierarchically at the system model design level,and the functions of WBS system described by natural language are strictly modeled in a formal language( SLIM,a subset of AADL). The possible faults of the system elements are considered and various types of fault modes are designed. Also the semantics of faulty behavior of the formal functional model is extended based on these fault modes. Then the safety of the extended system model is analyzed,such as FTA analysis. The case analysis demonstrates the validity and practicability of the model-based safety analysis method in industrial systems.

关 键 词：机轮刹车系统 AADL SLIM xSAP 故障树 FMEA表 

分 类 号：N945.1[自然科学总论—系统科学]