计算机科学 ›› 2016, Vol. 43 ›› Issue (5): 150-156.doi: 10.11896/j.issn.1002-137X.2016.05.028
陈光颖,黄志球,陈哲,阚双龙
CHEN Guang-ying, HUANG Zhi-qiu, CHEN Zhe and KAN Shuang-long
摘要： DO-333是对机载软件安全性标准DO-178C关于形式化方法的补充,为机载软件开发过程中形式化方法的使用提供指导。模型检验作为一种形式化方法,可以应用于对软件需求和设计阶段制品的严格验证。基于DO-333,使用模型检验对飞控系统中襟缝翼控制单元不同阶段的软件制品进行验证与分析,判断其是否满足DO-178C的相关验证目标并提供证据支持。首先,对控制单元中襟翼与缝翼必须互斥更新的高级需求进行规约和验证；其次,对单个机翼控制逻辑的低级需求进行规约和验证。通过以上验证与分析,分别为标准中关于高级和低级需求的验证目标提供证据。文中展示了模型检验在一个机载软件认证中的应用实例,该工作将为机载软件的安全性保障和适航认证提供技术支持。
| [1] RTCA.DO-178C,Software Considerations in Airborne Soft-ware[S].December 2011 [2] Xu B F,Huang Z Q,Hu J,et al.Model-Driven safety dependence verification for component-based airborne software supporting airworthiness certification[J].Acta Aeronautica et Astronautica Sinica,2012,3(5):796-808(in Chinese) 徐丙凤,黄志球,胡军,等.面向适航认证的模型驱动机载软件构件的安全性验证[J].航空学报,2012,33(5):796-808 [3] Huang Zhi-qiu,Xu Bing-feng,Kan Shuang-long,et al.Survey on Embedded Software Safety Analysis Standards,Methods and Tools for Airborne System[J].Journal of Software,2014,25(2):200-218(in Chinese) 黄志球,徐丙风,阚双龙,等.嵌入式机载软件安全性分析标准,方法及工具研究综述[J].软件学报,2014,5(2):200-218 [4] RTCA.DO-333,Formal Methods Supplement to DO-178C andDO-278A[S].December,2011 [5] Souyris J,Wiels V,Delmas D,et al.Formal verification of avioni-cs software products[M]∥FM 2009:Formal Methods.Springer Berlin Heidelberg,2009:532-546 [6] Moy Y,Ledinot E,Delseny H,et al.Testing or Formal Verification:DO-178C Alternatives and Industrial Experience[J].Software,IEEE,2013,30(3):50-57 [7] Miller S P,Whalen M W,Cofer D D.Software model checking takes off[J].Communications of the ACM,2010,53(2):58-64 [8] The Scade Website.http://www.esterel-technologies.com/products/scade-suite [9] Bochot T,Virelizier P,Waeselynck H,et al.Model checkingflight control systems:The Airbus experience[C]∥31st International Conference on ICSE Companion 2009.2009:18-27 [10] Laurent O.Using formal methods and testability concepts in the avionics systems validation and verification(v&v) process[C]∥2010 Third International Conference on Software Testing,Verification and Validation(ICST).IEEE,2010:1-10 [11] Cofer D,Miller S.DO-333 Certification Case Studies[M]∥NASA Formal Methods.Springer International Publishing,2014:1-15 [12] Chen Z,Gu Y,Huang Z,et al.Model checking aircraft controller software:A case study[J].Software:Practice and Experience,2013,45(7) [13] Holzmann G J.The SPIN model checker:Primer and reference manual[M].Reading:Addison-Wesley,2004 [14] Baier C,Katoen J P.Principles of model checking[M].Cambridge:MIT press,2008 [15] Harel D.Statecharts:A visual formalism for complex systems[J].Science of Computer Programming,1987,8(3):231-274 [16] Mikk E,Lakhnech Y,Siegel M,et al.Implementing statecharts in PROMELA/SPIN[C]∥Proceedings 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques,1998.IEEE,1998:90-101 [17] Latella D,Majzik I,Massink M.Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker[J].Formal Aspects of Computing,1999,11(6):637-664 [18] Dong Wei,Wang Ji,Qi Zhi-chang.Slicing UML Statecharts for Model Checking[J].Acta Electronica Sinica,2002,30(12):2084-2089(in Chinese) 董威,王戟,齐治昌.UML Statecharts的切片模型检验方法[J].电子学报,2002,0(12):2084-2089 |
| No related articles found! |
|
||
首页