面向航天器系统级测试的虚拟测试方法及应用

doi:10.7527/S1000-6893.2016.320768

Abstract

Abstract:

As a complex system, the verification of design and interface implementation of spacecraft is an effective way to increase its reliability. In this paper a virtual test method, which is a fusion approach on the combination of automata-based model checking theory and systems engineering theory, is proposed. An automaton of window tree model (WTM) based on multi-tree to describe the system behavior as a system-model is used on one hand, and a state transition graph (STG) based on automaton to describe design correctness as a specification is used on the other hand. An automaton-based model checking mechanism is proposed to build the foundation of the virtual test method. Moreover, the two main aspects of the method, including the design correctness verification and the interface implementation verification, are defined. Finally, a case study is followed to illustrate the technical approaches of virtual test method, the modelling process of a complex system as well as the verification process in a virtual test platform (VTP), which implements the method. The VTP is composed of three main features of the virtual test configuration, the virtual test execution as well as the virtual test evaluation.

Key words: virtual test method, state transition graph, model checking, window tree model, test case generation, virtual test platform

CLC Number:

V423
TP311

WUNIRI Qiqige, LI Xiaoping, YANG Fan, MA Shilong, WANG Huamao. A virtual test method for satellite system level verification and case study[J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2017, 38(7): 320768-320768.

References

[1] THOMPSON K. Three phases of testability[C]//Aircraft Design, Systems and Operations Conference. Reston: AIAA, 1988: 4454.
[2] WANG G G. Definition and review of virtual prototyping[J]. Journal of Computing & Information Science in Engineering, 2002, 2(3): 232-236.
[3] MAGNUSSON P S. The virtual test lab[J]. Computer, 2005, 38(5): 95-97.
[4] BEZIN Y, FUNFSCHILLING C, KRAFT S, et al. Virtual testing environment tools for railway vehicle certification[J]. Proceedings of the Institution of Mechanical Engineers. Part F: Journal of Rail & Rapid Transit, 2015, 229(6): 221-249.
[5] EVANS P L, CASTELLAZZI A, JOHNSON C M. A multi-disciplinary virtual prototyping design tool for power electronics[C]//8th International Conference on Integrated Power Systems (CIPS). Berlin: VDE, 2014: 1-7.
[6] HUANG T, KONG C W, GUO H L, et al. A virtual prototyping system for simulating construction processes[J]. Automation in Construction, 2007, 16(5): 576-585.
[7] AUWERAER H V D, DONDERS S, MAS P, et al. Breakthrough technologies for virtual prototyping of automotive and aerospace structures[M]. Belgium: Springer Netherlands, 2008: 397-418.
[8] DONATI A, MARTINEZHERAS J A, NUNES P, et al. Virtual reality for monitoring spacecraft thermal subsystem. concept & prototype[C]//Space OPS 2004 Conference, 2004: 120.
[9] 陈宗基, 黄浩东, 秦旭东. 飞行控制系统虚拟原型技术[J]. 航空学报, 2002, 23(5): 441-447. CHEN Z J, HUANG H D, QIN X D. Virtual prototyping for flight control systems[J]. Acta Aeronautica et Astronautica Sinica, 2002, 23(5): 441-447 (in Chinese).
[10] 依然. MSC软件助力航天七〇二所进行虚拟测试[J]. 航空制造技术, 2013(1): 22. YI R. MSC software supports on the virtual test in 702 Institute[J]. Aeronautical Manufacturing Technology, 2013(1): 22 (in Chinese).
[11] HEITMEYER C, ARCHER M, LEONARD E, et al. Applyingformal methods to a certifiably secure software system[J]. IEEE Transactions on Software Engineering, 2008, 34(1): 82-98.
[12] BAIER C, KATOEN J P. Principles ofmodel checking[M]. Massachusetts: The MIT Press, 2008: 271-287.
[13] CLARKE E M, WING J M. Formalmethods: State of the art and future directions[J]. ACM Computing Surveys, 1996, 28(4): 626-643.
[14] GLUCK P R, HOLZMANN G J. Using SPIN model checking for flight software verification[C]//Aerospace Conference Proceedings, 2002(1): 105-113.
[15] CARCENAC F, BONIOL F. Verification of an avionic system using timed model checking[C]//International Symposium on Leveraging Applications of Formal Methods (ISoLA), 2004: 335-342.
[16] MOTA A, SAMPAIO A. Model-checking CSP-Z: Strategy, tool support and industrial application[J]. Science of Computer Programming, 2001, 40(1): 59-96.
[17] MANNA Z, BJØRNER N S, BROWNE A, et al. An update on STeP: Deductive-algorithmic verification of reactive systems[M]. Tool support for system specification, development and verification. Vienna: Springer, 1999: 174-188.
[18] VARDI M Y, WOLPER P. An automata-theoretic approach to automatic program verification (preliminary report)[C]//Symposium on Logic in Computer Science, 1986: 322-331.
[19] 蒋屹新, 林闯, 曲扬, 等. 基于Petri网的模型检测研究[J]. 软件学报, 2004, 15(9): 1265-1276. JIANG Y X, LIN C, QU Y, et al. Research on model-checking based on Petri nets[J]. Journal of Software, 2004, 15(9): 1265-1276 (in Chinese).
[20] 李睿, 连航, 马世龙, 等. 基于形式化方法的航空电子系统检测[J]. 软件学报, 2015, 26(2): 181-201. LI R, LIAN H, MA S L, et al. Avionics system testing based on formal methods[J]. Journal of Software, 2015, 26(2): 181-201 (in Chinese).
[21] GROSS J, REICHWEIN A, BOCK D, et al. Anexecutable unified product model based on UML to support satellite design[C]//AIAA SPACE 2009 Conference & Exposition. Reston: AIAA, 2013.
[22] 连航. 面向安全苛刻系统可信性验证的检测方法关键技术研究[D]. 北京: 北京航空航天大学, 2013: 25-45. LIAN H. Research onkey technology of test method for credibility validation of safety-critical system[D]. Beijing: Beihang University, 2013: 25-45 (in Chinese).
[23] DUARTE E P, ZIWICH R P, ALBINI L C P. A survey of comparison-based system-level diagnosis[J]. ACM Computing Surveys, 2011, 43(3): 194-218.
[24] 尹宝林. 离散数学[M]. 北京: 高等教育出版社, 1998: 159-206. YIN B L. Discrete mathematics[M]. Beijing: Higher Education Press, 1998: 159-206 (in Chinese).
[25] BIAFORE B. Visio 2007bible[M]. Hoboken: John Wiley & Sons, 2007: 53-59.

A virtual test method for satellite system level verification and case study

PDF (PC)

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics

Comments

[1]	. Design and simulation of omnidirectional compliant docking joint for space non-cooperative target [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 0, (): 0-0.
[2]	ZHANG Bainan, QI Faren, XING Tao, LIU Yang, WANG Wei. Model based development method of manned spacecraft: Research and practice [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2020, 41(7): 23967-023967.
[3]	ZHANG Junhui, TONG An, WU Na, LIU Yinghua. Thermally-induced vibration of a solar sail in earth orbit [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2019, 40(11): 223135-223135.
[4]	WANG Bo, YE Dong, SUN Zhaowei, TANG Shengyong, CHEN Xin. Hierarchical planning for on-orbit self-reconfiguration of modular reconfigurable satellites [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2019, 40(9): 322912-322912.
[5]	ZHANG Qian, CAI Jianguo, DING Yifan, FENG Jian. Design of fold-development program for film reflective surface structures [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2018, 39(S1): 722268-722268.
[6]	LI Xiufeng, GAO Lingfei, WANG Haopan. Lightweight design of bracket for supporting gas cylinder based on structural optimization method [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2017, 38(12): 221267-221267.
[7]	ZHANG Xiaochen, XIA Xinlin, LIN Chaoguang, WANG Zhenfeng, TAN Heping. Effect of thermal radiation on thermal evaluation of hypersonic vehicle radomes [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2017, 38(10): 120916-120916.
[8]	MU Shuai, BU Huijiao, ZHANG Jin, LUO Yazhong. Re-planning method for space station pop-up missions [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2017, 38(7): 320793-320793.
[9]	PAN Lixin, YANG Jiayong, WANG Man, KONG Bin. Cabin environment design and application for hypersonic vehicle [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2016, 37(S1): 46-52.
[10]	LI Baojiang, SHAO Jiming, WANG Changhuan, HUANG Peng. Key technologies and solutions for large extensible door of re-entry space vehicle [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2016, 37(S1): 8-15.
[11]	LI Bo, YANG Yi. Optimization for structure efficiency of a deployable spaceborne truss with flat panel antennas [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2015, 36(12): 3853-3860.
[12]	JIA Guanghui, DUAN Xiao. Enhanced collaborative optimization modeling method of BLE about honeycomb sandwich panel [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2015, 36(7): 2260-2268.
[13]	JIA Guanghui, LI Xuan, OUYANG Zhijiang. Outlier identification from impact experimental data of honeycomb sandwich panel [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2015, 36(2): 548-554.
[14]	LI Shuang, JIANG Xiuqiang. Review and prospect of decelerator technologies for Mars entry [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2015, 36(2): 422-440.
[15]	JIN Jian, HOU Yongqing. Unsteady Simulation Analysis on Air Environment Parameters Control of Manned Spacecraft [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2014, 35(11): 2970-2978.