空天地一体化网络是基于空天地异构网络和来自空、天、地面以及海中的节点互连的网络,是安全攸关的系统,网络的可靠性和可信性是非常重要的问题。地球观测任务是基于空天地一体化网络的基础且关键的应用,而基于地球观测应用场景对该网络进行建模、仿真和验证研究则可以帮助确保系统的正确性和可靠性。相对比其他形式化建模语言,STeC语言由于其强调时间、空间及时空一致性信息,使得其更加适合应用于空天地一体化网络中地球观测任务的建模。首先,本文对实时系统规范语言STeC进行适当和必要的领域化,使其可以应用在空天地一体化网络领域中,使用该Domain-STeC完成对系统中两种场景下的地球观测任务的建模。其次,利用模型检测对系统性质进行验证分析。使用STeC工具对模型进行初步检查：包括词法、语法分析、时空一致性分析；并将模型转换成时间自动机模型,在UPPAAL中进行多种性质验证。再次,基于STeC语言和航天仿真工具STK进行二次开发,开发地球观测任务仿真控制工具,该工具除了提供对STK工具的基本控制功能之外,可以将STeC语言翻译成STK控制命令,使用STeC语句实时动态仿真任务中各智能体的行为,并在STK工具中图形化地动态显示任务执行过程。最后,基于STeC语言中的时空点概念引入时空曲线概念,使其能够描述地球观测任务中任务调度相关的区域覆盖问题,并探讨了三种简单情况下的任务的规划调度问题。