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

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

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

北京航空航天大学可靠性与系统工程学院, 北京 100191

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

详细信息

中图分类号: TP 311.5; N 941.5
计量
- 文章访问数: 3059
- HTML全文浏览量: 148
- PDF下载量: 660
- 被引次数: 0
出版历程
- 收稿日期: 2010-05-14
- 网络出版日期: 2012-01-30

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

School of Reliability and Systems Engineering, Beijing University of Aeronautics and Astronautics, Beijing 100191, China

摘要

摘要: Petri网是形式化的系统建模方法,以严格的数学基础来保证系统的正确构建,但在支持复杂软件建模和自动化验证方面存在不足.扩展了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.
- software safety /
- software engineering /
- Petri net /
- model checking

HTML全文

参考文献(1)

[1] Leveson N G.Software safety:why,what,and how [J].ACM Computing Surveys,1986,18(2):125-163[2] 刘克,单志广,王戟,等."可信软件基础研究"重大研究计划综述[J].中国科学基金,2008(3):145-151Liu Ke,Shan Zhiguang,Wang Ji,et al.Overview on major research plan of trustworthy software[J].Science Foundation in China,2008(3):145-151(in Chinese)[3] 袁崇义.Petri网原理与应用[M].北京:电子工业出版社,2005:51-75Yuan Chongyi.The principle and application of Petri net[M].Beijing: Electronics Industry Press,2005:51-75(in Chinese)[4] 姚洪英,范铁生,苏红丽,等.基于Petri网的分布式实时多媒体同步模型[J].沈阳工业大学学报,2004,26(1):96-98Yao Hongying,Fan Tiesheng,Su Hongli,et al.A distributed realtime multimedia synchronic model based on Petri net[J].Journal of Shenyang University of Technolgy,2004,26(1):96-98(in Chinese)[5] Cicirelli F,Furfaro A,Nigro L.An approach to protocol modeling and validation[C]//39th Annual Simulation Symposium.CA:IEEE Computer Society,2006:1-8[6] Franck C,Olivier H R.Structural translation from time Petri nets to timed automata[J].Journal of Systems and Software,2006,79(10):1456-1468[7] Bell D G,Brat G P.Automated software verification & validation: an emerging approach for ground operations[C]//Aerospace Conference,2008 IEEE.NY:IEEE Press,2008:1-8[8] Heitmeyer C L,Archer M M,Leonard E I.Applying formal methods to a certifiably Secure software system[J].Software Engineering,IEEE Transactions on, 2008,34(1):82-98[9] Li Zhen,Liu Bin,Ma Ning,et al.Formal testing applied in embedded software[C]//8th International Conference on Reliability,Maintainability and Safety.Washington,DC:IEEE Computer Society,2009,2:1-5[10] Ma Ning,Bao Xiaohong,Li Zhen,et al.Verification of safety-critical software requirement based on Petri-net model checking[C]//Supplemental Proceedings 20th International Symposium on Software Reliability Engineering.Washington,DC:IEEE Computer Society,2009[11] 李震,刘斌,殷永峰,等.基于扩展Petri网的安全关键软件需求模型检验[J].沈阳工业大学学报,2011,33(1):113-120Li Zhen,Liu Bin,Yin Yongfeng,et al.Requirement model checking of safety-critical software based on expanded Petri net [J].Journal of Shenyang University of Technology,2011,33(1):113-120(in Chinese)[12] 古天龙.软件开发的形式化方法[M].1版.北京: 高等教育出版社,2005:47-51Gu Tianlong.Formal methods of software development[M].1st ed.Beijing:Higher Education Press,2005:47-51(in Chinese)[13] 沈胜宇.模型检验的反例解释[D].长沙: 国防科学技术大学计算机学院,2005:1-7Shen Shengyu.Explaining counterexample of model checking[D].Changsha:School of Computer,National University of Defense Technology,2005:1-7(in Chinese)[14] Roberto C,Alessandro C,Charles A J,et al.NuSMV 2.4 user manual[EB/OL].Italy,Trento: CMU and ITC-irst,2005[2009].

施引文献

资源附件(0)

访问统计