实时多任务操作系统优先级反转与预防

实时多任务操作系统相对于其他操作系统而言,需要有更快的对外部事件的反应能力。因此,选择一种合适的任务调度算法非常重要。本文分析了时间片轮转的优先级抢占任务调度算法,以及控制共享资源访问的信号量机制。如果多个任务访问共享资源,可能会导致优先级反转。最后,提出了解决优先级反转的途径：优先级继承。试验证明,该方法行之有效。     

实时系统优先级反转研究*

在实时多任务操作系统中,由于外部事件需要有快速的反应能力,选择一种合适的任务调度算法非常重要。如果多个任务访问共享资源时,可能会导致优先级的反转问题。对此给出了目前经常采用的两种解决此问题的方法。分析了它们可能存在的不足,重点分析了优先级继承,并对它作了进一步改进。通过测试证明,该方法行之有效。     

一种有限优先级的静态优先级分配算法

静态优先级调度在实时系统中得到了广泛应用.然而,静态优先级调度受到系统支持的优先级个数的限制.当任务的个数大于优先级个数时,需要将多个任务映射到同一个优先级.针对优先级个数有限的情况,给出了在截止期限大于周期时任务可调度的充分必要条件,并提出了基于有限优先级的静态优先级分配算法(AGP).AGP算法对于基本任务集合是最优的静态优先级分配算法.其最优性表现在,所需的优先级个数最小,并且若采用AGP算法不可调度某个任务集,则采用其他静态优先级分配算法也不可调度该任务集.模拟结果表明,AGP算法的可调度性要远远大于常量法.AGP算法对于解决在嵌入式实时系统中任务的优先级分配问题具有重要意义.     

在μC/OS-II中消除优先级反转

使用实时内核,优先级反转是实时系统中出现最多的问题。为了防止这种现象的发生,内核必须能够自动变换任务的优先级,目前比较有效的方法有优先级继承和优先级顶置等。而作为一个优秀而应用广泛的实时内核,μC/OS-II没有防优先级反转的机制。基于此,首先分析了优先级反转及解决方法,然后提出如何对μC/OS-II的调度算法进行扩展,使其支持优先级顶置协议,从而良好解决了该实时系统中的优先级反转问题,提高了系统的实时性能。     

μC/OS-Ⅲ任务调度器在Coq中的验证

以μC/OS-Ⅲ内核中的任务调度器为研究对象,选取调度相关的核心代码,验证调度器代码满足优先调度最高优先级任务的性质。基于分离逻辑与SCAP验证理论,利用Coq辅助证明工具,通过定义机器模型、操作语义、逻辑断言以及推导规则构建验证框架。在验证框架中,定义内核数据结构和内核相关性质的逻辑描述,模块化地对内核代码进行推理。验证结果表明,μC/OS-Ⅲ任务调度器满足可靠性要求,并且可以通过机器的自动检查。     

基于阻塞调度的优先级反转解决策略

目前通常采用优先级上限协议解决策略,但该协议的系统资源利用率较低。针对该问题,深入分析了优先级反转的必要条件并提出了一种新的阻塞调度算法,能有效的避免优先级反转和检测死锁现象,同时具有较高的资源利用率和较广的适用范围。     

在μC/OS-Ⅱ中消除优先级反转

使用实时内核,优先级反转是实时系统中出现最多的问题。为了防止这种现象的发生,内核必须能够自动变换任务的优先级．目前比较有效的方法有优先级继承和优先级顶置等。而作为一个优秀而应用广泛的实时内核,μC／OS-Ⅱ没有防优先级反转的机制。基于此,首先分析了优先级反转及解决方法,然后提出如何对μC／OS—Ⅱ的调度算法进行扩展．使其支持优先级顶置协议,从而良好解决了该实时系统中的优先级反转问题．提高了系统的实时性能。     

复杂内核数据结构程序形式化验证

操作系统内核作为软件系统的基础组件, 其安全可靠是构造高可信软件系统的重要环节, 但是, 在实际的验证工作中, 操作系统内核中全局性质的不变式定义, 复杂数据结构程序的形式化描述和验证仍存在很多困难. 本文针对操作系统内核中满足的全局性质, 在代码层以函数为单位, 用全局不变式进行定义, 并在不同的函数中进行形式化验证, 从而证明各个函数符合操作系统内核的全局性质; 针对操作系统内核中经常使用的复杂数据结构程序, 本文通过扩展形状图理论, 提出一种使用嵌套形状图逻辑的方法来形式化描述复杂数据结构程序, 并对该方法进行了正确性证明, 最终成功验证操作系统内核中关于任务创建与调度, 消息队列创建与操作相关的代码.     

RTOS优先级反转问题分析

本文从RTOS的多任务和实时性特点出发,介绍了优先级反转问题,分析了发生优先级反转的基本原因．介绍了防止优先级反转的两种基本方法：优先级极限法和优先级继承法,并对两种方法进行分析和比较,在此基础上,提出了改进方法：优先级交换法。     

嵌入式操作系统SolCS中优先级反转问题研究

研发一个嵌入式实时操作系统时需要解决很多任务与共享资源之间的关系问题.介绍了优先级反转问题的理论模型,详细分析和比较了解决优先级反转问题的常规方案--优先级继承协议和优先级天花板协议.重点针对一个自主研发的嵌入式实时操作系统SolCS,提出了一种新的优先级反转问题解决方案并应用于其中,获得一个强实时能力的嵌入式操作系统.     

基于Linux任务优先级的实时性改进的研究

针对嵌入式系统对嵌入式操作系统的要求,本文分析了基于Linux任务优先级的调度策略中实时性能的不足,提出了一种嵌入式Linux任务调度模型,将任务的相对截止期和空闲时间这两个特征参数结合起来,综合设计任务的优先级,而且任务的优先级由相对截止期和空闲时间惟一确定,从而提高任务调度的成功率,增强了系统的实时性能。     

Verification of Real Time Operating System Exception Management Based on SPARCv8

Exception management,as the lowest level function module of the operating system,is responsible for making abrupt changes in the control flow to react to exception events in the system.The correctness of the exception management is crucial to guaranteeing the safety of the whole system.However,existing formal verification projects have not fully considered the issues of exceptions at the assembly level.Especially for real-time operating systems,in addition to basic exception handling,there are nested exceptions and task switching by exceptions service routine.In our previous work,we used high-level abstraction to describe the basic elements of the exception management and verified correctness only at the requirement layer.Building on earlier work,this paper proposes EMS(Exception Management SPARCv8),a practical Hoare-style program framework to verify the exception management based on SPARCv8(Scalable Processor Architecture Version 8) at the design layer.The framework describes the low-level details of the machine,such as registers and memory stack.It divides the execution logic of the exception management into six phases for comprehensive formal modeling.Taking the executing scenario of the real-time operating system SpaceOS on the Beidou-3 satellite as an example,we use the EMS framework to verify the exception management.All the formalization and proofs are implemented in the interactive theorem prover Coq.     

Verifying the Implementation of an Error Control Code

This document describes how the FORTE STE-based formal verification system was used to verify the RTL implementation of an error control code. The error control code considered is linear: its encoder and decoder proceed by matrix multiplication. Although that function is in essence combinational, its implementation in a high-performance microprocessor is done in a pipelined fashion. The additional state elements introduced by the pipelining quickly push an SMV-style model checker to its capacity limits. With the case-study presented in this document, we show that an STE-style model checker is better suited for this problem. We present two instances of the ECC verification problem. For the first we were able to combine an encoder and a decoder into one model for verification. For the second, such a combination was not possible and we resorted to verifying properties of a matrix that we extracted from the implementation.     

基于Event-B的航天器内存管理系统形式化验证

内存管理系统位于操作系统内核的最底层,为上层提供内存分配和回收机制.在航天器这类安全攸关的关键系统中,其可靠性和安全性至关重要,必须要考虑到强实时性、有限空间限制、高分配效率以及各种边界条件约束.因此,系统通常采用较为复杂的数据结构和算法来管理内存空间,同时需要采用非常严格的形式化方法来保证航天器这类安全攸关系统的高可信性.对复杂内存管理系统的形式化验证也会较之前的验证工作带来更多难题,主要体现在：内存管理模块中的复杂数据结构的形式化描述;操作的规范语义;行为的建模;内部函数的规范及断言定义与循环不变式的定义;实时性验证等方面.本文拟针对这些问题,深入分析实际的航天器操作系统内存管理系统的特性;探索基于分层迭代的语义描述与验证的一般性方法与理论,并应用这些理论方法,来验证一个具有实际应用的航天嵌入式操作系统的内存管理系统.本文研究成果有望被直接应用于我国新一代的航天器系统上.     

DBox:宏内核下各种设备驱动程序的高性能安全盒

越来越多和宏内核操作系统中使用的设备驱动程序相关的漏洞被发现,这些漏洞严重危害操作系统的安全性和可靠性.现有的解决方案无法既能为操作系统内核提供强有力的保护又能达到与原生系统相近的性能.在本文中,我们提出了一个称为DBox的驱动程序隔离框架解决方案同时考虑系统的安全性和性能.DBox为设备驱动程序提供了一个基于虚拟化的安全容器,使得驱动程序和主机系统有效隔离,并通过通用I/O交互接口实现对多种设备驱动的支持.我们通过对EPT页表和IOMMU地址翻译表的修改,创建了一块基于连续物理内存的共享内存,实现了硬件设备、驱动程序和主机系统内核之间的高性能通信基础.我们通过多核并行化、高效消息传递、零拷贝和批量数据传输等机制深度优化了I/O性能,在大多数情况下DBox中的驱动程序都可以达到与原始内核相同的性能.在DBox中添加新驱动程序支持无需修改驱动程序代码,使得DBox方案在现实环境中易于采用.我们在DBox中实现了四个常见驱动程序类别(NIC,块设备,UART和输入设备),经过实验表明,TCP/UDP吞吐量、往返时延、块设备吞吐量、串口吞吐量、串口往返时延及键盘响应时间的性能下降均在5%以下.     

Verifying functions in online stock trading systems

Temporal colored Petri nets, an extension of temporal Petri nets, are introduced in this paper. It can distinguish the personality of individuals (tokens), describe clearly the causal and temporal relationships betwee nevents in concurrent systems, and represent elegantly certain fundamental properties of concurrent systems, such as eventuality and fairness. The use of this method is illustrated with an example of modeling and formal verification of an online stock trading system. The functional correctness of the modeled system is formally verified based on the temporal colored Petri net model and temporal assertions. Also, some main properties of the system are analyzed. It has been demonstrated sufficiently that temporal colored Petri nets can verify efficiently some time-related properties of concurrent systems, and provide both the power of dynamic representation graphically and the function of logical inference formally. Finally. future work is described.     

一种实时操作系统的进程优先级检索算法研究

进程调度是影响操作系统实时性的一个重要的因素,而很多主流操作系统(如:Linux)都是采用基于优先权的进程调度算法,该调度算法就是遍历就绪队列中的所有进程,找出优先级最高的进程,并交给处理器执行。通常情况下,该算法的时间复杂度为O(n),而这样的时间复杂度不能很好地满足实时系统的要求。该文将对一种新的进程优先级检索方法进行研究分析,并给出该方法时间复杂度的分析过程。     

公钥Kerberos协议的认证服务过程的建模与验证

公钥Kerberos协议是目前广泛使用的一类认证协议。本文使用安全协议验证工具SPVT对公钥Kerberos协议（PKINIT）的认证服务过程进行了形式化的建模与验证。SPVT自动地检测出PKINIT存在一个中间人攻击,该攻击可使攻击者假冒密钥发布中心和终端服务器,骗取用户信任,窃取重要数据。本文首次使用验证工具检测出公钥Kerberos协议的攻击,该攻击的自动检测对大型复杂协议的自动验证具有重大意义。借助于SPVT,人们能尽早发现协议缺陷。这充分说明,SPVT能够对大型复杂安全协议进行建模与验证,是一个有效的协议验证工具。     

一种异构多核处理器嵌入式实时操作系统构架设计

由于异构多核处理器和多处理器系统及同构多核处理器的构架存在很大差别,应用于多处理器系统的分布式结构以及应用于同构多核系统的主从式结构操作系统不能解决异构多核处理器的实时调度和效率问题。对异构多核处理器的特点及发展趋势进行了研究,提出了一种适用异构多核处理器的多主模式实时操作系统构架。这种构架将通信总线中的多主模式引入多核操作系统构架中,采用对称式结构及组件模式设计操作系统模型,使多核处理器中每个内核都可以作为主核实现对资源、任务的实时管理,提高系统性能,同时可以解决主从式操作系统存在的由于处理器核增多而带来的主内核不能满足系统性能要求的瓶颈问题。通过这种单一构架模型可以进行灵活配置,以适应不同结构及功能要求的处理器内核,降低操作系统开发难度。     

操作系统汇编级形式化设计和验证方法

由于系统的巨大规模,操作系统设计和实现的正确性很难用传统的方法进行描述和验证.在汇编层形式化地对系统模块的功能语义进行建模,提出一种汇编级的系统状态模型,作为汇编语言层设计和验证的纽带.通过定义系统状态模型的合法状态和状态转换函数来建立系统状态模型的论域,并以此来描述汇编层的论域.通过验证汇编层的功能模块的正确性来保证汇编语言层设计的正确性,达到对系统功能实现的正确性验证.同时,使用定理证明工具Isabelle/HOL来形式化地描述这一系统状态模型,基于这一形式化模型,在Isabelle/HOL中验证系统模块的功能语义的正确性.以实现的安全可信OS（verified secure operating system,简称VSOS）为例,阐述了所提出的形式化设计和验证方法,说明了这一方法的可行性.