| With the rapid development of space industry in China,especially the launched of Key Scientific and Technological Projects such as Manned space projects,Lunar exploration projects and High-resolution earth observation systems,the role and position of software in spacecraft are becoming more and more important,The number,scale,and complexity of software on spacecraft have increased dramatically,software systems have become increasingly large and difficult to control,and national space missions urgently need software to be more dependable.This paper studies the key technologies of the construction and verification of GF-2 satellite control software,so it has very important theoretical significance and application value.The main contributions in this paper are as follows:1.Aiming at the problem of ambiguity in natural language description of software requirements of GF-2 satellite control software,a formal requirements modeling language SPARDL for space embeded control software is proposed,which is implemented through strict syntax and semantic definitions an accurate specification description of the working mode requirements in the control software;a property description language based on interval sequential logic is proposed,and a property description template suitable for engineering applications is developed;an algorithm for generating a simulation program from the SPARDL model is designed by co-simulation with the satellite environment model enables analysis and inspection of software requirements;2.Aiming at the dependability design of GF-2 satellite control software,firstly,the key factors that affect the dependability of the satellite on-board embedded control software and the software dependability guarantee model are proposed.By taking various guarantee methods in various stages of software development,so as to systematic ensure the dependability of the software;on this basis,for the real-time nature,single-particle upset effect,and software updating onboard、operating system and 1553 B bus communication and other key issues of the GF-2 satellite control software,respectively proposed and implemented the corresponding dependability design methods and technologies;3.Aiming at the test of the GF-2 satellite control software relies heavily on the target hardware environment,making it difficult to find software errors as early as possible.A simulation technology for target processor and input / output interface chips is proposed,the rapid construction of the virtual simulation test environment has been achieved;for the problems of complex control software functions,multiple working modes,and difficult system testing,a semi-physical and all-physical system test environment has been designed and implemented,and a flight-like test method based on satellite flight procedures is proposed,and designed a checklist of the test content of the flight-like,tested the GF-2 satellite control software;GF-2 satellite is China’s first civilian optical remote sensing satellite with a spatial resolution better than 1 meter.The satellite was successfully launched and has been running in orbit stably so far.It has completely changed the main high-resolution earth observation data reliance on imports.By applying a series of methods and techniques proposed in this paper,the dependability of control software was met,and no software quality problems occurred during the satellite’s operation in orbit.The satellite won the first award for Scientific and Technological Progress of National Defense in December 2018.The research results of this paper have been applied in the development of spacecraft on-board control software including Manned space projects,Lunar exploration projects and Beidou navigation system,etc.With the successful development and operation of these spacecraft control software,these research results will surely provide scientific support and strong guarantee for the smooth implementation of the national space mission. |