TY - GEN
T1 - Modeling and Verification of Space-Air-Ground Integrated Networks on Requirement Level Using STeC
AU - Yang, Zhihua
AU - Xiao, Bo
AU - Chen, Yixiang
N1 - Publisher Copyright:
© 2015 IEEE.
PY - 2015/10/26
Y1 - 2015/10/26
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84958169070
U2 - 10.1109/TASE.2015.8
DO - 10.1109/TASE.2015.8
M3 - 会议稿件
AN - SCOPUS:84958169070
T3 - Proceedings - 2015 International Symposium on Theoretical Aspects of Software Engineering, TASE 2015
SP - 131
EP - 134
BT - Proceedings - 2015 International Symposium on Theoretical Aspects of Software Engineering, TASE 2015
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - International Symposium on Theoretical Aspects of Software Engineering, TASE 2015
Y2 - 12 September 2015 through 14 September 2015
ER -