航天器测试需求描述及其自动生成

高世伟; 吕江花; 乌尼日其其格; 孟祥曦; 马世龙

doi:10.13700/j.bh.1001-5965.2014.0762

航天器测试需求描述及其自动生成

doi: 10.13700/j.bh.1001-5965.2014.0762

北京航空航天大学计算机学院, 北京 100191

基金项目: 国家自然科学基金(61300007); 中央高校基本科研业务费专项资金(YWF-15-GJSYS-106,YWF-14-JSJXY-007); 软件开发环境国家重点实验室自由探索基金(ZX2015ZX-09,SKLSDE-2014ZX-06)

详细信息

作者简介:
高世伟(1983—),男,山东德州人,博士研究生,ge89@163.com

通讯作者:
吕江花(1975—),女,山东日照人,讲师,jhlv@nlsde.buaa.edu.cn,主要研究方向为软件自动化、形式化方法.

中图分类号: TP273⁺.5;V219
计量
- 文章访问数: 994
- HTML全文浏览量: 57
- PDF下载量: 683
- 被引次数: 0
出版历程
- 收稿日期: 2014-12-04
- 修回日期: 2015-03-06
- 网络出版日期: 2015-07-20

Spacecraft test requirement description and automatic generation method

School of Computer Science and Engineering, Beijing University of Aeronautics and Astronautics, Beijing 100191, China

摘要

摘要: 航天器作为一个典型的安全苛刻系统,其可信性研究需求迫切,支持可信性评估的数据来自于航天器测试用例的执行,而航天器测试需求是测试用例生成的重要依据.在实际应用中,对航天器这类复杂系统,面临测试需求庞杂、测试需求编制周期长、人工经验编制方式难以保证测试需求的充分性、完备性及可复用性等问题.针对这些问题,通过分析航天器组织结构特点,建立航天器形式化模型,基于航天器测试任务流程,给出了航天器静态测试需求和动态测试需求形式化描述规范,并给出航天器测试需求自动生成方法,保证了测试需求的充分性和完备性,提高了测试需求复用性,与人工编制方式相比,缩短了测试需求编制周期.最后设计并实现航天器测试需求生成应用系统,验证所提出方法的有效性.
- 安全苛刻系统 /
- 可信性 /
- 测试需求 /
- 测试任务流程 /
- 航天器
Abstract: Spacecraft as a typical safety-critical system, its trustworthiness study is very urgent. The evaluation and verification for spacecraft depends on the data obtained from the execution of spacecraft test cases. Moreover, spacecraft test requirement is the important basis for test case generation.In practical application, such complex system of spacecraft is faced with problems of the complexity for the spacecraft test requirement, long preparation period for the test requirement, and difficulty in assuring the adequacy, completeness, and reusability of test requirement using artificial experience. To solve these problems, the spacecraft formalized model was constructed by analyzing the characteristics of the spacecraft structure.The formalization specification of spacecraft static test requirements and dynamic test requirements were given based on spacecraft testing task flow. And the corresponding automatically generation methods for spacecraft testing requirements were proposed. The adequacy and completeness of spacecraft test requirement are ensured, and the reusability of test requirement is enhanced. Compared with the artificial establishment way, the period of the compiled test requirements is shorten. Finally, the application system for spacecraft test requirement generation is designed and implemented, which validates the effectiveness of the proposed method.
- safety critical system /
- trustworthiness /
- test requirement /
- test task flow /
- spacecraft

HTML全文

参考文献(24)

[1]	吕江花, 马世龙, 李先军, 等.安全苛刻系统自动化测试的形式化语义模型[J].软件学报, 2014, 25(3): 489-505. Lü J H, Ma S L, Li X J.et al.Formal semantics model for automatic test of safety critical systems[J].Journal of Software, 2014, 25(3): 489-505(in Chinese).
[2]	Lv J H, Ma S L, Li X J.et al.A high order collaboration and real time formal model for automatic test of safety critical systems[J].Frontiers of ComputerScience, 2015.DOI: 10.1007/s11704-015-2254-y.
[3]	Wilhelm H, Reussner R.Toward trustworthy software systems[J].Computer, 2006, 39(4): 91-92.
[4]	刘克, 单志广, 王戟, 等.可信软件基础研究重大研究计划综述[J].中国科学基金, 2008(3): 145-151. Liu K, Shan Z G, Wang J, et al.Overview on major research plan of trustworthy software[J].Bulletin of National Natural Science Foundation of China, 2008(3): 145-151(in Chinese).
[5]	郑志明, 马世龙, 李未, 等.软件可信性动力学特征及其演化复杂性[J].中国科学(F辑: 信息可信), 2009, 52(9): 1651-1657. Zheng Z M, Ma S L, Li W.et al.Dynamical characteristics of software trustworthiness and their evolutionary complexity[J].Science China Series F-Information Sciences, 2009, 52(9): 1651-1657(in Chinese).
[6]	郑志明, 马世龙, 李未, 等.软件可信复杂性及其动力学统计方法[J].中国科学(F辑: 信息可信), 2009, 52(8): 1328-1334. Zheng Z M, Ma S L, Li W.et al.Complexity of software trustworthiness and its dynamical statistical analysis methods[J].Science China Series F-Information Sciences, 2009, 52(8): 1328-1334(in Chinese).
[7]	Knight J C. Safety critical systems: Challenges and directions[C]//Proceedings of the 24rd International Conference on Software Engineering.Piscataway, NJ: IEEE Press, 2002: 547-550.
[8]	王庆成. 航天器电测技术[M].北京: 中国科学技术出版社, 2007: 48-133. Wang Q C.Electrical test technology for spacecraft[M].Beijing: China Science and Technology Press, 2007: 48-133(in Chinese).
[9]	杨占才, 周一鸥, 刘金甫.测试需求描述方法综述[J].测控技术, 2009, 28: 270-273. Yang Z C, Zhou Y O, Liu J F.Summarization of test requirements description methods[J].Measurement Control Technology, 2009, 28: 270-273(in Chinese).
[10]	Lansdowne C A, McCartney P, Gorringe C.Experimental applications of automatic test markup language(ATML)[C]//Proceedings of 2012 IEEE Autotestcon.Piscataway, NJ: IEEE Press, 2012: 318-323.
[11]	Smith A, Wanigaratne A.Applications of ATML test results and intrastage to facilitate intelligent data analysis[C]// Proceedings of 2012 IEEE Autotestcon.Piscataway, NJ: IEEE Press, 2012: 200-203.
[12]	高猛. 实时嵌入式软件系统测试需求建模研究[J].航天控制, 2010, 28(5): 64-69. Gao M.Research on system-testing requirement modeling for real-time embedded software[J].Aerospace Control, 2010, 28(5): 64-69(in Chinese).
[13]	沈剑乐, 王林章, 李宣东, 等.一个基于UML顺序图的场景测试用例生成方法[J].计算机科学, 2004, 31(8): 179-184. Shen J L, Wang L Z, Li X D, et al.An approach to generate scenario test cases based on UML sequence diagrams[J].Computer Science, 2004, 31(8): 179-184(in Chinese).
[14]	杨波, 吴际, 徐珞, 等. 一种软件测试需求建模及测试用例生成方法[J].计算机学报, 2014, 37(3): 522-538. Yang B, Wu J, Xu L, et al.An approach of modeling software testing requirements and generating test case[J].Chinese Journal of Computers, 2014, 37(3): 522-538(in Chinese).
[15]	侯超凡, 吴际, 刘超. 基于测试需求的互操作性测试用例生成方法[J].计算机科学, 2014, 41(11): 162-168. Hou C F, Wu J, Liu C.Interoperability test case generation based on testing requirements[J].Computer Science, 2014, 41(11): 162-168(in Chinese).
[16]	赵瑞峰. 基于办公自动化的卫星自动测试方法的设计和实现[D].上海: 上海交通大学, 2010. Zhao R F.Design and implementation of satellite automatic test method based on office automation[D].Shanghai: Shanghai Jiaotong University, 2010(in Chinese).
[17]	Esteve M, Katoen J, Nguyen VP, et al.Formal correctness, safety, dependability, and performance analysis of a satellite[C]//Proceedings of the 34th International Conference on Software Engineering, ICSE.Piscataway, NJ: IEEE, 2012: 1022-1031.
[18]	Peng Z G, Lu Y, Miller A, et al.Formal modelling and quantitative analysis of satellite navigation systems[J].Computing Research Repository, 2014: 1402.5599.
[19]	Fischer P M, Ludtke D, Schaus V, et al.A formal method for early spacecraft design verification[C]//Proceedings of 2013 IEEE Aerospace Conference. Piscataway, NJ: IEEE Press, 2013: 1-8.
[20]	Nguyen V Y. Trustworthy spacecraft design using formal methods[D].Chemnitz: Technische Universität Chemnitz, 2012.
[21]	Bozzano M, Cimatti A, Katoen J P, et al.Safety, dependability and performance analysis of extended AADL models[J].The Computer Journal, 2011, 54(5): 754-775.
[22]	Hudak P, Hughes J, Peyton J, et al.A history of Haskell: being lazy with class[C]//Proceedings of the third ACM SIGPLAN Conference on History of Programming Languages.New York: ACM, 2007.
[23]	Pike L, Niller S, Wegmann N.Runtime verification for ultra-critical systems[C]//Proceedings of 2nd Conference on Runtime Verification.Berlin, Heidelberg: Springer, 2012: 310-324.
[24]	Yu D, Ma S. Design and implementation of spacecraft automatic test language[J].Chinese Journal of Aeronautics, 2011, 24(3): 287-298.