留言板

尊敬的读者、作者、审稿人, 关于本刊的投稿、审稿、编辑和出版的任何问题, 您可以本页添加留言。我们将尽快给您答复。谢谢您的支持!

姓名
邮箱
手机号码
标题
留言内容
验证码

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

李震 刘斌 陆民燕 殷永峰

李震, 刘斌, 陆民燕, 等 . 基于扩展Petri网的除冰软件安全需求建模和验证[J]. 北京航空航天大学学报, 2012, 38(1): 64-68,105.
引用本文: 李震, 刘斌, 陆民燕, 等 . 基于扩展Petri网的除冰软件安全需求建模和验证[J]. 北京航空航天大学学报, 2012, 38(1): 64-68,105.
Li Zhen, Liu Bin, Lu Minyan, et al. Modeling and verification of de-icing software safety requirement based on expanded Petri net[J]. Journal of Beijing University of Aeronautics and Astronautics, 2012, 38(1): 64-68,105. (in Chinese)
Citation: Li Zhen, Liu Bin, Lu Minyan, et al. Modeling and verification of de-icing software safety requirement based on expanded Petri net[J]. Journal of Beijing University of Aeronautics and Astronautics, 2012, 38(1): 64-68,105. (in Chinese)

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

基金项目: "十一五"重点预研课题(51319070101); 航空科学基金资助项目(20095551025); 国家自然科学基金资助项目(70971056); 机载软件工程化研究专题(DY09Z11926)
详细信息
  • 中图分类号: TP 311.5; N 941.5

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

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

     

  • [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].http://nusmv.irst.itc.it/
  • 加载中
计量
  • 文章访问数:  2833
  • HTML全文浏览量:  113
  • PDF下载量:  656
  • 被引次数: 0
出版历程
  • 收稿日期:  2010-05-14
  • 网络出版日期:  2012-01-30

目录

    /

    返回文章
    返回
    常见问答