关键词：
嵌入式实时系统
动态加载
可变任务调度
形式化验证
集成开发环境
摘要：
航天器是安全关键的实时系统,任务截止期的错失可能导致严重后果。随着航天技术的发展,航天任务越来越复杂,空间计算机从单核发展到了多核,从封闭式系统发展为可扩展开放式系统,使得任务可以并行运行和动态加载,增强了系统算力,提高了系统可扩展能力。空间嵌入式实时操作系统Space OS作为航天器功能实现最重要的载体,因此,对其提出了更高的要求,需要操作系统功能进行进一步扩展以满足要求。然而,系统的进一步扩展带来了处理器核数、任务数和任务类型的变化,增加了系统的不确定性。为了确保系统的实时性、可靠性和易用性,研究空间嵌入式实时操作系统在处理器核数变化、任务数变化和任务类型变化情况下的可变任务调度、形式化验证和开发工具具有重大的理论价值和实际意义。
通过研究,本文取得了如下研究成果:
（1）针对单核处理器中间歇（Sporadic）任务动态加载时的可调度性分析问题,提出了精确布尔干扰分析方法EBIA（Exact Boolean Interference Analysis）。首先考虑了任务释放抖动和共享资源访问阻塞情况,对任务的干扰时间进行了分析,得到一个更加紧凑的可调度性判定充分条件,然后结合响应时间分析方法得出了精确布尔干扰分析方法。实验表明,EBIA的可调度性分析效率大幅度优于其它方法,且随着任务数的增加,效率优势进一步扩大。例如任务数为20时,其运行时间开销降低了76%。
（2）针对单核处理器中固定点（Fixed-point）任务和间歇（Sporadic）任务动态加载时的可调度性分析问题,提出了虚拟周期分析方法VPA（Virtual Period Analysis）。首先根据任务时间特性分配优先级,然后虚拟化所有固定点任务为一个间歇任务,对此间歇任务周期进行缩减并计算出其最差虚拟执行时间,最后按单调速率方法的利用率上界公式判定任务集的可调度性。VPA可对n个任务进行快速可调度性判定,时间复杂度仅为O（n2）。在我国空间站计算机进行了对比验证,实验表明判定效率优于现有可调度性判定方法,当任务数为20时,运行时间开销降低了41.8%,可调度率提高了5.7%。
（3）针对多核处理器中间歇（Sporadic）任务的多核分组DM（Deadline Monotonic）调度和加速因子分析问题,提出了分组截止期首次优先调度方法PDM-FFD（Partitioned Deadline Monotonic First-Fit Decrease）。首先通过对任务干扰时间的分析,提出了一种更为紧凑的可调度性判定方法。然后任务按照其相对截止期以非递减顺序排序,采用First-Fit策略选择处理器核分配任务,并在各处理器核上采用DM调度策略。最后通过上述可调度性判定方法来判定任务的可调度性。证明了PDM-FFD的加速因子为3-（3Δ+1）/（m+Δ）,时间复杂度为O（n2）+O（nm）,其中n为任务数,m为处理器核数,Δ为任务集相关因子。该加速因子严格小于3-1/m,优于已有多核分组调度算法FBB-FFD。实验表明,PDM-FFD的可调度率优于其它方法,且随着处理器核数的增加,可调度率优势进一步扩大。例如处理器核数为4时,其可调度率提高了18.5%。
（4）针对多核处理器中固定点（Fixed-point）任务和间歇（Sporadic）任务动态加载时的多核分配问题,提出了虚拟利用率最坏优先分配方法VU-WF（Virtual Utilization Worst Fit）。构造了一个用于满足固定点任务执行请求的虚拟延期服务器VDS（Virtual Deferral Server）,并推导了任务集的一个可调度性分析公式。然后结合VDS的容量计算特性,提出了任务分配方法VU-WF,其核心是按照处理器核的虚拟利用率从小到大顺序选择核进行任务分配。实验表明,VU-WF算法整体性能更优,不仅具有较高的可调度率和较好的负载均衡性,同时具有最低的运行时开销。在4核处理器中,与其它同样可调度性的算法对比时,负载均衡率提高了73.9%,而运行时开销降低了38.3%。
（5）针对嵌入式实时操作系统任务调度模块的正确性保证问题,提出了基于定理归纳的形式化验证方式,并以空间嵌入式实时操作系统Space OS中的任务调度模块为对象进行了验证。采用需求—设计—实现三层验证框架和Coq定理证明工具对任务调度模块的需求层、设计层和实现层进行了建模和性质验证。其中在设计层发现了一个设计缺陷并对其流程图和代码进行了修正,修正后的设计和代码通过了性质验证。需求层、设计层、实现层均通过验证,证明了任务调度模块代码实现的正确性,提高了系统可靠性。
（6）针对嵌入式实时操作系统软件开发流程复杂、可变任务调度技术难以应用问题,设计和实现了一款支持可变任务调度的新一代易用集成开发环境NE Studio（New Ea
