面向SysML模型的安全性分析与验证方法

doi:10.11896/jsjkx.181001850

计算机科学 ›› 2019, Vol. 46 ›› Issue (11): 100-108.doi: 10.11896/jsjkx.181001850

面向SysML模型的安全性分析与验证方法

李宛倩, 胡军, 陈松, 张维珺

(南京航空航天大学计算机科学与技术学院南京211106)

收稿日期:2018-10-07 出版日期:2019-11-15 发布日期:2019-11-14
通讯作者: 胡军(1973-),男,博士,副教授,CCF会员,主要研究方向为模型驱动的系统安全性分析、软件验证等,E-mail:hujun.nju@gmail.com
作者简介:李宛倩(1994-),女,硕士,主要研究方向为系统安全性分析与验证,E-mail:wqli@nuaa.edu.cn;陈松(1991-),男,硕士,主要研究方向为软件分析和模型检测;张维珺(1994-),女,硕士,主要研究方向为机载系统安全性分析。
基金资助:
本文受国家重点基础研究发展计划-973计划(2014CB744903),国家航空科学基金(20165515001),南京航空航天大学研究生创新基地开放基金(kfjj20171611),中央高校基本科研业务费专项资金资助。

Method of System Safety Analysis and Verification for SysML Models

LI Wan-qian, HU Jun, CHEN Song, ZHANG Wei-jun

(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China)

Received:2018-10-07 Online:2019-11-15 Published:2019-11-14

摘要/Abstract

摘要： 近年来,随着航空、交通、医疗等安全关键系统的规模越来越大,涉及到的复杂度也越来越高,基于模型的系统安全性分析与验证成为安全关键系统工程领域的一个重要研究方向,因而如何对以 SysML为典型的系统模型进行安全性分析与验证是一个非常重要的问题。文中以基于模型的安全性分析(MBSA)为框架,设计了一个面向SysML模型的系统安全性分析与验证方法,实现了从模型构建到安全性分析与属性验证的完整过程。首先,从需求层面和设计层面对SysML系统架构设计模型和最新系统安全性建模语言AltaRica3.0进行了介绍,构建了从SysML的核心模型元素到AltaRica3.0模型的语义等价的转换规则,给出了转换规则的形式化描述并分析证明转换规则的正确性;然后,基于模型驱动的方法设计了一个原型工具平台来完成模型的自动转换和安全性分析过程,该原型工具集成了转换、编译生成故障树、故障树分析、单步仿真及故障路径动态演示等功能,实现了系统设计和安全性分析的同步性,并在此基础上给出了AltaRica3.0至Promela模型的转换关键点,结合穷尽式模型验证工具SPIN对模型的属性进行安全性验证;最后,根据4761标准中对机轮刹车系统的体系结构设计描述和安全性的需求建立SysML模型,依据原型工具平台和属性验证工具实现模型的自动转换和安全性分析验证,进而来说明此转换方法的有效性。

关键词: AltaRica3.0, Promela, SysML, 安全关键系统, 机轮刹车系统

Abstract: In recent years,with the increasing scale and complexity of safety-critical systems such as aviation,transportation and medical treatment,model-based system safety analysis and verification has become an important research direction in the field of safety-critical system engineering.How to analyze and verify the safety of SysML as a typical system model is a very important issue.Based on the framework of model-based safety analysis,this paper designed a safety analysis and verification method for the SysML models,which realizes the complete process from model construction to safety analysis and attribute verification.Firstly,this paper introduced SysML system architecture design model and the latest system safety modeling language AltaRica3.0 from requirement level and design level,constructed the semantic equivalence transformation rules from the core model elements of SysML to AltaRica 3.0,gave the formal description of transformation rules,analyzed and proved the transformation rules.Then,this paper designed a prototype tool platform based on the model-driven method to complete the process of automatic transformation and safety analysis of the model.The prototype tool combines the functions of transformation,compilation and generation of fault tree,fault tree analysis,stepwise simulation and dynamic demonstration of fault path.The synchronization of system design and safety analy-sis was realized.On the basis of this,the key points of transformation from AltaRica 3.0 to Promela model were given,and the attributes of the model were verified by the exhaustive model verification tool SPIN.Finally,the SysML model was established according to the architecture design description and safety requirements of the wheel brake system in 4761 standard,and the automatic conversion,safety analysis and verification of the model were realized based on the prototype tool platform and attribute verification tool,which further illustrates the effectiveness of the conversion method.

Key words: AltaRica3.0, Promela, Safety-critical system, SysML, Wheel brake system

中图分类号:

TP311

李宛倩, 胡军, 陈松, 张维珺. 面向SysML模型的安全性分析与验证方法[J]. 计算机科学, 2019, 46(11): 100-108. https://doi.org/10.11896/jsjkx.181001850

LI Wan-qian, HU Jun, CHEN Song, ZHANG Wei-jun. Method of System Safety Analysis and Verification for SysML Models[J]. Computer Science, 2019, 46(11): 100-108. https://doi.org/10.11896/jsjkx.181001850

参考文献

[1]GOMES A,MOTA A,SAMPAIO A,et al.Systematic ModelBased Safety Assessment Via Probabilistic Model Checking[J].Lecture Notes in Computer Science,2010,6415:625-639.
[2]FRIEDENTHAL S,MOORE A,STEINER R.A practical guideto SysML:the systems modeling language[M].San Francisco:Morgan Kaufmann,2014.
[3]FRIEDENTHAL S,MOORE A,STEINER R.OMG SystemsModeling Language (OMG SysML?) Tutorial[C]∥INCOSE International Symposium.INCOSE,2008:1731-1862.
[4]MICHEL B,TATIANA P,ANTOINE R.AltaRica3.0 Language Specification[M/OL].https://www.openaltarica.fr/docs-downloads/.
[5]BIEBER P,BOUGNOL C,CASTEL C,et al.Safety Assessment with Altarica[M]∥Building the Information Society.US:Springer,2004:505-510.
[6]ERICSON C A.Fault tree analysis[C]∥System Safety Conference.Orlando,Florida,1999:1-9.
[7]INVERARDI P,MUCCINI H,PELLICCIONE P.Automatedcheck of architectural models consistency using SPIN[C]∥Proceedings 16th Annual International Conference on Automated Software Engineering (ASE 2001).IEEE,2001:346-349.
[8]PROSVIRNOVA T,BATTEUX M,BRAMERET P A,et al.The altarica 3.0 project for model-based safety assessment[J].IFAC Proceedings Volumes,2013,46(22):127-132.
[9]PROSVIRNOVA T,RAUZY A.AltaRica 3.0 project:compileGuarded Transition Systems into Fault Trees[C]∥European Safety and Reliability Conference.2013.
[10]CLARKE E M,GRUMBERG O,PELED D.Model checking[M].Massachu-setts MIT Press,1999.
[11]KOVSE J,HARDER T.Generic XMI-based UML model transformations[C]∥International Conference on Object-Oriented Information Systems.Springer,Berlin,Heidelberg,2002:192-198.
[12]WANG J,HU L,CHEN S,et al.Verification of RiskA calculation engine based on Open-PSA platform[C]∥2013 International Conference on Quality,Reliability,Risk,Maintenance,and Safety Engineering (QR2MSE).IEEE,2013:32-35.
[13]INVERARDI P,MUCCINI H,PELLICCIONE P.Automatedcheck of architectural models consistency using SPIN[C]∥16th Annual International Conference on Automated Software Engineering,2001.(ASE 2001).IEEE,2001:346-349.
[14]HU J,CHEN S,WANG M M.Method oftransformation and verification from AltaRica3.0 to Promela[J].Computer Engineering &Science,2017,39(4):708-716.(in Chinese)
胡军,陈松,王明明.AltaRica3.0模型到Promela模型转换与验证方法研究[J].计算机工程与科学,2017,39(4):708-716.
[15]LUO W L,WEI O,HUANG M Y.Computing minimal cut sets of fault tree using SAT solver[J].Computer Engineering & Scien-ce,2017,39(4):725-733.(in Chinese)
罗炜麟,魏欧,黄鸣宇.基于SAT求解器的故障树最小割集求解算法[J].计算机工程与科学,2017,39(4):725-733.
[16]SAE International.Guidelines and methods for conducting thesafety assessment process on civil airborne systems and equipment[M].SAE International,1996.
[17]BOZZANO M,CIMATTI A,PIRES A F,et al.Formal design and safety analysis of AIR6110 wheel brake system[C]∥Internatio-nal Conference on Computer Aided Verification.Springer,Cham,2015:518-535.
[18]DAVID P,IDASIAK V,KRATZ F.Automating the synthesis of AltaRica Data-Flow models from SysML[C]∥Proceedings of European Safety and Reliability Conference (ESREL09).2009:105-112.
[19]BOZZANO M,CIMATTI A,LISAGOR O,et al.Safety assessment of AltaRica models via symbolic model checking[J].Science of Computer Programming,2015,98(4):464-483.

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed

面向SysML模型的安全性分析与验证方法

Method of System Safety Analysis and Verification for SysML Models

PDF (PC)

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 9

Metrics

本文评价

推荐阅读 0

[1]	唐红英, 胡军, 陈朔, 石梦烨. 面向SysML的系统安全性分析工具与实例研究 System Safety Analysis Tool for SysML and Case Study 计算机科学, 2020, 47(5): 284-294. https://doi.org/10.11896/jsjkx.190600169
[2]	薛艳, 武淑红, 王耀力. 基于SPIN的G语言系统模型的验证 Verification of G Language System Model Based on SPIN 计算机科学, 2018, 45(6A): 536-540.
[3]	徐文华,张育平. 基于航电系统架构模型的安全性分析工具的设计与实现 Design and Implementation of Safety Analysis Tool Based on Avionics System Architecture Model 计算机科学, 2016, 43(Z11): 536-541. https://doi.org/10.11896/j.issn.1002-137X.2016.11A.121
[4]	仵志鹏黄志球王珊珊曹德建. 一种基于故障扩展SysML活动图的安全性验证框架研究 Research on Framework of Safety Verification Based on Fault-extended SysML Activity Diagram 计算机科学, 2015, 42(7): 222-228. https://doi.org/10.11896/j.issn.1002-137X.2015.07.048
[5]	王飞,沈国华,黄志球,马琳,刘畅,李海峰,廖莉莉. 一种结合线性时序逻辑和故障树的软件安全验证方法 Method Combining Linear Temporal Logic and Fault Tree for Software Safety Verification 计算机科学, 2015, 42(12): 71-75.
[6]	敬超,常亮,古天龙. 基于SPIN的无线传感器网络安全协议建模与分析 Using SPIN to Model and Analyze Security Protocol in Wireless Sensor Network 计算机科学, 2009, 36(10): 132-136.
[7]	段风琴李祥. Petri网性质的线性时序逻辑描述与Spin检验计算机科学, 2006, 33(5): 287-289.
[8]	. 软件安全核的可信性问题计算机科学, 2006, 33(1): 170-174.
[9]	杨仕平熊光泽桑楠. 安全关键系统高可信保障技术的研究计算机科学, 2003, 30(5): 97-101.