Verification And Simulation Of Earth Observation Mission On Space-Air-Ground Integrated Networks Based On STeC

Space-Air-Ground integrated network (SAGIN) is a safety-critical system with a large interconnection of air, space, ground and sea nodes. This network is het-erogenerous, whose reliability and dependability should be highly concerned. Earth observation mission is one of the most basic and important applications based on SAGIN. In order to ensure the reliability and dependability of the system, formal methods of modelling, simulation and verification should be applyed. Compared with other formal modelling languages, the Spatio-Temporal Consistency language (STeC) is more suitable to model earth observation missions of SAGIN application-s, bacause the STeC stresses spatio-temporal information and the spatio-temporal consistency.Firstly, this paper instantiates the specification language of real time systems-the STeC into the Domain-STeC, helping the Domain-STeC apply to SAGIN. Besides, the earth observation missions are modelled in two application scenarios.Secondly, model checking techniques are used to verify some important prop-erties of the system. One part of the verification is to do some preliminary model checking by the STeC tool, including lexical analysis, snytax analysis and spatio-temporal consistency checking. The other part is to verfiy properties in the UPPAAL tool after transforming STeC models to Timed Automata.Thirdly, this paper develops a simulation and controlling tool of earth ob-servation missions by re-developing the astronautics domain simulation software STK (Satellite Tool Kit) with the Domain-STeC. This tool translates Domain-STeC statements to STK control commands, and controls STK. Consequently, Domain-STeC statements are used to simulate system actions successfully, and processes of earth observation missions can be shown in STK dynamically.Lastly, this paper introduces the concept of the spatio-temporal curve based on spatio-temporal points in the STeC, describing the region coverage problems related to the task scheduling in earth observation missions. In this paper, the mission scheduling problem is also discussed under three simple circumstances.