Modeling and Verification of Space-Air-Ground Integrated Networks on Requirement Level Using STeC

This paper introduces a domain Spatio-Temporal Consistency (STeC) language for the application domain of space-air-ground integrated networks. The STeC language is taken as the foundation of modeling our systems, bacause it works well on specifying real-time systems concerning not only the time characteristic but also the location characteristic and the consistency between them. In this paper, a domain-STeC language is devised and applied to model satellite observation processes. We use two tools to check and verify this STeC model, the syntax and spatio-temporal consistency were checked in STeC tool, and after being transformed into timed automata model, some further verification can be finished in UPPAAL tool. It shows that the instantiated STeC approach is suitable for modeling and verifying space-air-ground integrated networks on the requirement level. This work helps to ensure the spatial-temporal consistency in that application domain, and increases the reliability and dependability of our system.