当前,各国越来越重视空天地网络信息系统（GASNIS）的建设。GASNIS是以空中平台,包括空间站、高中低轨道的卫星、平流层的气球、有人或无人驾驶的飞行器;以及地面平台、包括地面站点或地面移动终端;水域平台,包括海洋观测船舶或有其他特殊任务的船舶为载体所组成。GASNIS是实时获取,传输和处理相关信息为主要任务的网络信息系统。其发展涉及到国家的政治,经济,军事以及民生等各个重要领域。GASNIS是一个复杂的典型移动通信系统。其本身的拓扑结构不断变化,同时用户提交的任务需求复杂多样,这样导致大量用户进程在一个拓扑结构变化着的系统中海量并发移动,加之其传输速率还会受到空间或地表物理环境的影响,都增加了系统的复杂性。为了充分利用系统资源,提高系统服务质量,我们需要对GASNIS中的任务进行合理的调度。任务调度所关注的问题主要集中在系统中各任务的执行顺序以及系统资源有限的前提下,实现任务与资源高效耦合所需的对任务和资源进行的定性与定量分析。任务的执行顺序的实质就是按照任务的权重对任务进行排序,而对任务和资源进行定性定量的分析,实际上是基于调度对象和调度环境被清晰界定和描述的基础上,对任务的资源需求及系统环境的资源供给在时空上进行性质和数量上的分析。为了更好的调度GASNIS任务,也就是说为了提高调度的响应速度以及调度的合理性。需要做好两方面的工作。第一,需要研究适应并行环境的排序算法以提高调度的响应速度;第二,研究合适的工具描述GASNIS任务调度,并在此基础上对系统任务调度进行分析和验证。针对第一方面的问题:本文提出了多种并发排序算法,以解决任务调度时按照任务权重来排序的问题。按照被排序元素存储方式的不同,本文提出的排序算法分为两类:一类是针对链表式存储元素提出的基于链表式存储元素的并发排序算法,另一类是针对索引式存储元素提出的基于索引式存储元素的并发排序算法。在针对链表式存储元素的排序算法中常规算法效率都比较低,本文利用并发特性提出的基于链表式存储元素的排序算法在长度为n的链表中抽取m个元素进行排序,最多需要2n-m次的元素比较就可以完成元素排序。在针对基于索引存储的元素进行排序时,本文提出了筛选排序算法的思想,在筛选排序算法的基础上,结合并发的思想提出了并发筛选排序算法和并发筛选插入排序算法。并发筛选排序在资源足够尤其是有相应的硬件支持下,所需的时间非常少,假设两个元素之间的比较需要的时间为t1,n个1并发累加的时间为t2,那么不论元素的多少,在并发率达到100%的情况下,理论上排序所需时间为t1+t2。并发筛选插入排序的时间相对略长一些,但是所需的资源要少一些。为了使这些算法能直接应用于GASNIS的任务调度中,本文对这些算法都进行了形式化描述、推导及验证。这些并发排序算法不但适应于GASNIS的任务调度环节,也适应于其他需要排序功能的计算环境。针对第二方面的问题:本文在seal演算的基础上对其语法和语义做了量化描述方面的扩展,建立了量化seal演算。具体的扩展如下:1)针对seal演算缺乏对进程和seal量化描述的问题,本文提出了资源量化的思想,即提出对seal标签和进程名字在描述时的量化扩展。其中seal标签的含义从一个单独的域标识名字,变成一个名字加资源供给函数矩阵的序偶对。而进程名字含义是从一个简单的名字变成一个名字加上资源需求函数矩阵的序偶对。这样就可以从seal的资源供给和进程的资源需求的角度分析和考察GASNIS,弥补了seal演算无法对系统进行量化描述的缺陷。2)针对进程运行的位置问题,本文提出了位置量化的思想,即更加细化进程的位置描述,首先,扩充了seal演算中“移动”的思想,提出了允许进程移动的规则,解决了实际系统中尤其是只需要移动系统中部分进程的时候,难以用seal移动进行模拟的问题。其次,针对特殊资源与位置绑定的问题,提出了允许进程位置的锁定和解锁的规则,解决了进程分类和资源分类后特殊进程与资源匹配的安全性问题,也就是说锁定后的进程运行过程中不能随意被移动,除非调度系统将其解锁。第三,针对seal演算中,seal移动后,被移动的seal内部进程以及与该seal相关进程的位置上标指示有可能出现混乱的问题提出了进程上标地点的修改规则,使得seal移动更灵活,适应面更广泛。3)针对复制算子和部分并发操可能导致的资源无节制使用问题,本文提出了并发和复制量化的思想,即提出了并发算子和无限复制算子的约束规则,增加了并发算子和无限复制算子的上标,以限制进程最大并发数量,以及允许并发算子和无限复制算子上标的修改来适应seal中资源的变化,实现资源使用控制的描述,以提高资源使用率和系统执行效率。4)针对seal演算中,缺乏进程中间状态的描述,导致调度时缺乏对系统资源的检测和控制的问题,本文提出了过程量化的思想,即扩充了τ的含义,增加了中断操作的描述。首先,采用τ来表示内部动作或相关进程运行的中间状态,解决了进程在处于调度中间状态的描述问题。进程执行中间状态的引入也意味着量化seal演算对时间控制描述的引入,这一点对任务调度的分析非常重要。其次中断描述可以使量化seal演算更好更全面的来描述系统。通过采用量化seal演算对系统描述分析有助于我们在设计早期可以发现系统中不一致、不完全和二义性以及系统中存在的逻辑错误等问题;在设计中期方便建立简单的仿真系统,模拟大量任务出入资源动态变化的系统,验证海量进程在拓扑结构动态变化的节点群中并发移动并执行;在系统设计后期方便分析和预估系统效能,追踪系统的漏洞方便对系统错误的分析、维护以及系统的评估。论文最后对移动通信系统形式化描述方法研究工作进行了总结,并提出了进一步量化研究、图形化描述方法研究以及建立形式化描述框架等需要继续研究的问题。