北京航空航天大学学报 ›› 2012, Vol. 38 ›› Issue (1): 64-68,105.

• 论文 • 上一篇    下一篇

基于扩展Petri网的除冰软件安全需求建模和验证

李震, 刘斌, 陆民燕, 殷永峰   

  1. 北京航空航天大学 可靠性与系统工程学院, 北京 100191
  • 收稿日期:2010-05-14 出版日期:2012-01-30 发布日期:2012-01-13
  • 作者简介:李 震(1977-),男,江苏兴化人,博士生,现为江苏科技大学电子信息学院讲师,justlz@163.com.
  • 基金资助:

    "十一五"重点预研课题(51319070101); 航空科学基金资助项目(20095551025); 国家自然科学基金资助项目(70971056); 机载软件工程化研究专题(DY09Z11926)

Modeling and verification of de-icing software safety requirement based on expanded Petri net

Li Zhen, Liu Bin, Lu Minyan, Yin Yongfeng   

  1. School of Reliability and Systems Engineering, Beijing University of Aeronautics and Astronautics, Beijing 100191, China
  • Received:2010-05-14 Online:2012-01-30 Published:2012-01-13

摘要: Petri网是形式化的系统建模方法,以严格的数学基础来保证系统的正确构建,但在支持复杂软件建模和自动化验证方面存在不足.扩展了Petri网的形式语义,区别定义了状态型和数值型库所,区别定义了变迁的激发和抑制状态,引入了无前置、一元和组合判断规则,同时根据形式化定义将模型自动转换为检验程序实施安全性验证.最后给出了以上方法在典型安全关键软件-除冰系统上的应用,过程和结果表明扩展的模型和方法增强了Petri网对复杂软件系统的建模能力,提高了软件的安全性,从模型到验证代码的自动转换解决了完善模型时人工修改相应代码的工作量和因此而引入人为错误的重复工作量的问题.

Abstract: As a formal method, Petri net can ensure the correct construction of system but lacks the ability of modeling complicated system and automatic verification. Firstly, the formal semantics of Petri net was expanded, the place of state and numeric were distinctively defined, the transition state of fired and inhibitory were distinctively defined, the non-precondition, unitary precondition and composite precondition were introduced, and the model was transformed into verification program to implement the safety verification according to formal definitions. And then, the effectiveness of this methodology was illustrated with an application in an aircraft de-icing system which is a typical safety-critical system. The process and result show that the expanded model and methodology enhance the ability of Petri net to model complicated software system, improve the software safety, and the automatic transform from model to codes settle the workload of rewrite corresponding code manually and the meaningless faults introduced by that when the model should be modified.

中图分类号: 


版权所有 © 《北京航空航天大学学报》编辑部
通讯地址:北京市海淀区学院路37号 北京航空航天大学学报编辑部 邮编:100191 E-mail:jbuaa@buaa.edu.cn
本系统由北京玛格泰克科技发展有限公司设计开发