Paper Info
Title
Modeling and Verification of Space-Air-Ground Integrated Networks on Requirement Level Using STeC
Abstract
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.
Year
DOI
Venue
2015
10.1109/TASE.2015.8
International Symposium on Theoretical Aspects of Software Engineering
Keywords
Field
DocType
requirement level,domain spatio-temporal consistency language,application domain,systems modeling,real-time systems,time characteristic,location characteristic,domain-STeC language,satellite observation processes,STeC model checking,STeC model verification,STeC tool,timed automata model,UPPAAL tool,space-air-ground integrated networks modeling,space-air-ground integrated networks verification,system reliability,system dependability,safety-critical system
Satellite,Dependability,Computer science,Automaton,Air ground,Real-time computing,Satellite observation,Software,Application domain,Syntax
Conference
Citations 
PageRank 
References 
1
0.36
8
Authors
3
Name
Order
Citations
PageRank
Zhihua Yang110.36
Bo Xiao251.78
Yixiang Chen372.53