期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

基于改进Petri网的可信软件模型验证和测试研究

Verification and Testing of Dependable Software Model Based on Improved Petri Net
下载PDF
导出
摘要 软件被广泛应用到安全关键领域,这对软件可信性的验证和测试提出了严苛的要求.形式化方法以其严格的数学基础保证软件系统的正确构建.Petri网利用库所和变迁支持异步、并发、分布式系统建模,但是缺少对库所和变迁类型的描述,不能满足软件系统复杂的具体行为特征.模型检验工具具有自动化验证和反例生成功能,但是调试和建模能力不够.文章扩展Petri网以更好的支持软件系统的行为建模和分析,建立模型和验证工具的自动化转化机制,对软件系统进行模型检验,利用反例功能获得失效场景路径,指导测试用例生成,最后给出了定时器示例和机载发动机软件的典型实例应用. 软件被广泛应用到安全关键领域,这对软件可信性的验证和测试提出了严苛的要求.形式化方法以其严格的数学基础保证软件系统的正确构建.Petri网利用库所和变迁支持异步、并发、分布式系统建模,但是缺少对库所和变迁类型的描述,不能满足软件系统复杂的具体行为特征.模型检验工具具有自动化验证和反例生成功能,但是调试和建模能力不够.文章扩展Petri网以更好的支持软件系统的行为建模和分析,建立模型和验证工具的自动化转化机制,对软件系统进行模型检验,利用反例功能获得失效场景路径,指导测试用例生成,最后给出了定时器示例和机载发动机软件的典型实例应用.
作者 李震 刘斌 殷永峰 李晓勋
机构地区 北京航空航天大学可靠性与系统工程学院
出处 《计算机研究与发展》 EI CSCD 北大核心 2010年第S1期273-279,共7页 Journal of Computer Research and Development
基金 国家"十一五"重点预研课题基金项目(51319070101) 航空科学基金项目(20095551025) 机载软件工程化研究专题基金项目(DY09Z11926)
关键词 可信软件 PETRI网 验证 软件测试 模型检验 dependable software Petri verification software testing model checking
分类号 TP3 [自动化与计算机技术—计算机科学与技术]
  • 相关文献

参考文献13

  • 1刘克,单志广,王戟,何积丰,张兆田,秦玉文.“可信软件基础研究”重大研究计划综述[J].中国科学基金,2008,22(3):145-151. 被引量：136
  • 2单锦辉,姜瑛,孙萍.软件测试研究进展[J].北京大学学报（自然科学版）,2005,41(1):134-145. 被引量：134
  • 3林闯,刘婷,曲扬.一种不确定时段的扩展时段时序逻辑:时间Petri网模型表示和线性推理[J].计算机学报,2001,24(12):1299-1309. 被引量：13
  • 4Bell D G,Brat G P.Automated software verification&validation:An emerging approach for ground operations. IEEE Aerospace Conference . 2008
  • 5Zhenyu Chen,Conghua Zhou,Decheng Ding.Automatic Abstraction Refinement for Petri Nets Verification. High-Level Design Validation and Test Workshop,2005.Tenth IEEE International .
  • 6Heitmeyer C L,Archer M M,Leonard E I,et al.Applying for-mal methods to a certifiably secure software system. IEEETrans.on Software Engineering . 2008
  • 7Cicirelli,F.,Furfaro,A,,Nigro,L.An approach to protocol modeling and validation. 39th Annual Simulation Symposium . 2006
  • 8Li Zhen,Liu Bin,Ma Ning,Yin Yongfeng.Formal Testing Applied in Embedded Software. 8th International Conference on Reliability, Maintainability and Safety . 2009
  • 9F. Cassez,O. H. Roux.Structural translation from time Petri nets to timed automata. The Journal of Systems and Software . 2006
  • 10Ma Ning,Bao Xiaohong,Li Zhen,Haifeng Li.Verification of Safety-Critical Software Requirement Based on Petri-Net Model Checking. 20th International Symposium on Software Reliability Engineering.Supplemental Proceedings . 2009

二级参考文献56

  • 1赵元聪,朱三元.面向对象软件测试的认识[J].计算机应用与软件,1996,13(3):1-4. 被引量：19
  • 2宫云战 刘海燕 万琳 等.软件测试性的分析与设计技术研究[A]..2000年全国测试学术会议(CTC2000)[C].北京,2000.271-274.
  • 3邵维忠 王立福 梅宏 等 见:杨芙清 何新贵主编.面向对象的软件测试--方法研究及系统设计[A].见:杨芙清, 何新贵主编.软件工程进展[C].北京: 清华大学出版社,1996.115-122.
  • 4Tracey N J. A Search-Based Automated Test-Data Generation Framework for Safety-Critical Software: [PhD thesis]. Department of Computer Science, University of York, 2000.
  • 5Korel B, Al-Yami A M. Assertion-Oriented Automated Test Data Generation. In: Proceedings of the 18^th International Conference on Software Engineering,Berlin:1996. 71-80.
  • 6Korel B, Al-Yami A M. Automated Regression Test Generation. In: Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, Beach:1998. 143-152.
  • 7Weyuker E J. The Applicability of Program Schema Results to Programs. International Journal of Computer Information Sciences, 1979, 8(5): 387-403.
  • 8Ramanmoorthy C V, Ho S-B F, Chen W T. On the Automated Generation of Program Test Data. IEEE Transactions on Software Engineering, 1976, SE-2 (4): 293-300.
  • 9Kung D, Suchak N, Gao J, et al. On Object State Testing. In: Proceedings of COMPSAC'94, 1994. 222-227.
  • 10Goodenough J B, Gerhart S L. Toward a Theory of Test Data Selection. IEEE Transactions on Software Engineering, 1975, SE-3 (6): 156-173.

共引文献280

计算机研究与发展
2010年 第S1期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部