基于Event-B的SpaceOS2操作系统任务管理需求形式化建模与验证

谭彦亮，杨 桦，乔 磊

(北京控制工程研究所，北京100190)

0 引言

操作系统是计算机系统的重要组成部分，管理着系统的硬件资源，是应用程序得以正确运行的基础.操作系统的可靠依赖于内核的可靠，尤其像航天器这种安全攸关的系统，对嵌入式操作系统有极高的可靠性、安全性、正确性要求，因此对操作系统内核进行验证是有必要的.

形式化方法可以帮助分析系统描述不一致、不明确或不完整的部分，通过逻辑推理可以验证模型是否满足需求规约，已成为公认的提高软件质量、增强系统可靠性的有效方法.其基本过程是用形式化语言对系统进行描述，建立系统的形式化模型，这称为形式化规约，之后采用模型检测、定理证明等形式化验证方法对模型进行验证，保证模型的正确性.

采用形式化方法来验证操作系统正确性由来已久，早在1980年，美国加州大学洛杉矶分校的Walker等［1］就对Unix的安全内核进行了形式化描述与验证工作，Bevier［2］建立了内核形式模型，文献［3］对操作系统规约进行了形式化描述.澳大利亚NICTA在2004年对操作系统内核L4开展了形式化验证工作并发布了新一代嵌入式操作系统seL4，项目负责人Klein等［4］宣称嵌入式安全操作系统seL4是第一个使用正规机器检测证明(formal machinechecked proof)的通用操作系统，按照软件可信度量标准CC标准的技术评价指标，seL4已经超越了EAL-7级水平.

当前对操作系统的形式化研究工作主要集中在对模型的描述与对其性质的验证上，这在NICTA Workshop关于L4内核的多篇论文中都有具体体现.

航天操作系统SpaceOS是由北京控制工程研究所研制的星载计算机嵌入式操作系统，在多个航天型号任务上得到了实际应用.其中SpaceOS2是第二代星载计算机操作系统，已经成功应用在探月工程嫦娥三号巡视器“玉兔号”月球车上.

本文使用Event-B［5］形式化方法对嵌入式操作系统SpaceOS2形式化地建立了一个任务需求的模型，需求提出的任务约束性质在Rodin［6］平台上得到了验证.

1 Event-B简介

Event-B是一种基于状态的形式化方法，其数学理论基础是集合论和谓词逻辑，常用于系统级的建模与分析.基于Eclipse的Rodin平台为Event-B提供了形式化建模环境与自动化验证的工具，同时有多种插件可以方便地验证证明.

1.1 Event-B 模型

Event-B的模型是通过抽象状态机(ASM，abstract state machine)来定义的，ASM使用变量来表示模型的状态，定义事件来对其状态进行操作.ASM通过自动机(machine)和场景(context)两个组件来构造一个完整的模型，图1说明了两个组件之间的关系，自动机需要引用场景的定义.

在自动机组件中，系统变量在VARIABLES中声明，其约束在INVATIANTS里定义，并且需要在事件Initialisation中对变量进行初始化赋值.在场景组件中，可以自定义一些数据类型如集合，在CONSTANTS声明一些常量，并且在AXIOMS提出对集合和常量的约束作为公理.

系统的行为是依靠一系列的原子事件EVENTS来实现的，一个事件定义为如下形式:

图1 Event-B模型组成关系图Fig.1 Composition relation for Event-B model

其中，lv是事件可能用到的局部变量，g是事件发生的前条件，R是对变量的赋值操作.Event-B中事件的执行必须满足前提条件g的约束.

1.2 Event-B 常用符号

Event-B的模型描述中经常使用到的一些运算符号，除了基本的交并集合运算外，其他运算如表1所示.

?

1.3 Event-B 验证机理

自动机和场景中可以定义定理，其中在场景中的形式为T(d，c)，自动机中的形式为T(d，c，v).证明义务确保了提出定理的是可证的.在场景里定义的定理生成如下证明:

在自动机里定理生成的证明形式如下:

为了证明一个描述的正确性，需要保证模型一直保持着不变式I(d，c，v).这里的不变式可以是对变量的类型约束、取值约束，还可以是系统性质.

例如模型中的一个事件ei满足各种条件约束，则有下式成立:

式中，A是各个公理的合取，I是各不变式的合取，gi是事件ei的前提条件，BAi是事件ei的前后断言，d表示各集合，c表示各常量，v和v'分别表示事件执行前后的变量值.它表述的意义是事件ei执行某个操作后，改变了系统变量v的状态，状态改变后的v'仍要满足对变量v的约束条件，这是证明的普遍形式，Event-B模型正是靠证明来保证模型的正确性.

2 任务管理需求的形式化模型

嵌入式系统通常是建立在一个嵌入式操作系统内核之上的，由内核提供任务调度和中断处理操作.任务管理决定了操作系统的实时性能，它涉及到的内容包括任务状态迁移，任务控制块，内核中各种队列，调度算法等.任务管理实现的核心和基础是任务状态和迁移时序，任务运行状态的迁移和任务队列决定了调度器的实现.

SpaceOS2的任务管理要求任务具有7种状态，支持64个优先级，优先级采用静态分配.任务调度采用最高优先级的抢占式调度策略，同优先级任务采用时间片轮转的方式，可使重要任务尽快得到执行，实现快速响应.

2.1 模型对象

本文的建模思想是使用集合与集合之间的关系来描述任务的状态变迁，这其中需要用到任务、任务状态集、任务状态转换关系、任务变迁时序控制等对象.

对象1.任务，基本的任务控制块TCB属性包括状态、优先级、时间片等.

使用集合Tasks表示任务类型，声明一个任务t时可以描述为t∈Tasks.任务申请内存空间之后才被加入到任务集合中，为了表示是否已得到申请内存，设置一个函数isTCB∈Tasks→BOOL，只有映射到TRUE的任务才是被认为分配了内存等资源后创建成功的任务.这些创建成功的任务记为TCBid.

设置任务状态集，TaskStatus={executing，ready，delay，block，suspend，suspend_delay，suspend_block};设置任务优先级Priority，它是自然数的一个子集;用任务与各属性的之间的函数映射关系来表示TCB属性，包括状态tskStatus，优先级tskPrio，延迟时间片个数delayTicks，剩余时间片个数leftTicks.其映射关系的约束条件是一个任务只有一个状态、优先级、延迟时间、剩余时间片，是多对一的函数映射.

对象4.任务迁移时序，通过设置一些变量标志来作为任务执行的时序条件.

createFlag=1表示可以创建任务，创建完成后把标志createFlag置0.当需要触发创建任务操作的时候就把标志置为1.其他标志还包括删除任务标志deleteFlag，延时任务标志delayFlag，恢复任务标志resumeFlag，重启任务标志restartFlag，调度标志scheduleFlag，任务剩余时间片清零标志clearTickFlag，更新最高优先级就绪任务标志updateHPrioFlag.

这些标志的类型都是整数类型NAT，可以根据需要赋值为 0，1，2 等.

2.2 模型行为

操作系统对任务管理提出的功能要求包括以下行为操作:创建任务、删除任务、挂起任务、恢复任务、延时任务、调度任务，通过控制任务的状态变迁和对任务集合的操作来实现任务管理.下面以任务调度为例进行介绍.

任务调度需要做的是按照某一调度策略从就绪任务中选择一个任务运行，将它的状态设为运行态.目前的嵌入式实时操作系统通常采用的调度策略是基于优先级的抢占式调度与时间片轮转相结合的调度策略调度操作需要分为3种不同情况:

1)当前任务进行自删除、延时、阻塞、自挂起等操作时，主动放弃CPU使用权，此时只需从就绪态任务集中选择最高优先级的任务设为执行态即可.在将当前任务改变状态加入相应状态集的同时，需要将current状态设为none，将scheduleFlag状态设为1，此时触发以下操作:

2)就绪态任务集中有新的任务加入，此时触发调度.首先选择最高优先级的任务与正在运行的任务进行优先级比较，如果就绪任务优先级高，则进行切换.当有新任务进入就绪就绪任务集时，就将scheduleFlag状态设为2，并将最高优先级就绪任务比当前任务优先级高作为进行任务切换的一个前提条件，因此有以下操作:

3)二者优先级相同，则当前任务与最高优先级任务互换，并将最高优先级任务的时间片剩余时间设为1.与第二种情况相比需增加一个前提条件:当前任务剩余时间片为0.此外增加了一个操作Clear-Tick，用来表示当前任务执行了1个时间片后，剩余执行时间清零，开始执行下一个同优先级就绪任务，因此有以下操作:

在就绪态任务集状态发生变化时，最高优先级任务HPrioTask有可能会发生改变，此时应及时更新.

3 模型的形式化验证

Rodin平台对Event-B产生的证明义务有很好的自动化证明的支持，并且有多种插件帮助证明过程如ProB、SMT求解器等，可以在交互证明时提供帮助.

在不变式中可以加入断言语句表示系统性质，例如一个任务只能对应一个任务状态.

这些性质与系统对其他变量的约束一样，当状态发生改变时，系统会生成相应的证明义务，要求进行验证.

图2 ProB对模型的检验结果Fig.2 Model checking result by ProB

从图2可以看到，经过ProB的模型检验，任务管理模型没有发生死锁，也没有不变式违反情况发生，说明模型是正确的.

之后通过交互式证明器给出显式的证据来让用户相信系统模型的正确性.这一证明过程在插件SMT的帮助下很方便的证明系统生成的所有证明义务.统计结果如图3所示.

图3 证明义务的统计Fig.3 Statistics on proof obliations

利用Rodin平台上的插件ProB对模型可能存在的死锁、不变式违反情况等问题应用模型检验技术进行了检测，利用定理证明技术对功能需求涉及到的证明义务及非功能需求的定理性质进行了逻辑推理证明.验证结果表明任务需求模型不存在死锁情况，所有事件都有得到运行的机会;模型检验没有发现不变式违反情况.Event-B模型是依靠变量状态改变前后始终保持不变式来保证模型的正确性的.

4 结论

本文对航天嵌入式操作系统SpaceOS2内核的任务管理模块，应用形式化方法Event-B建立了一个初级模型，该模型描述了内核任务管理的特性，包括任务在不同状态之间的变迁、事件执行条件约束、任务调度算法等.并利用Rodin平台提供的交互式定理证明工具验证来内核形式化模型的正确性.结果表明模型满足了需求的规约，在需求阶段针对任务管理模块提出的功能及性质要求是正确的.

［1］WALKER B J，KEMMERER R A，POPEK L.Specification and verification of the UCLA Unix security kernel［J］.Communications of the ACM，1980，23(2):118-131.

［2］BEVIER W.A Verified operating system kernel［D］.Austin:University of Texas，1987.

［3］BIRRELL A D，GUTTAG J V，HORNING J J，et al.Synchronisation primitives for a multiprocessor:a formal specification［J］.ACM SIGOPS Operating Systems Re-view，1987，21(5):94-102

［4］KLEING，ELPHINSTONE K.SeL4:formal verification of an OS kernel［C］//Jeanna Neefe，SOSP'09 Proceedings of the ACM SIGOPS 22ndsymposium on Operating Systems Principles. New York:ACM Press，2009:207-220.

［5］ABRIALJ R.Modeling in Event-B:system and software engineering［M］.Cambridge:Cambridge University Press，2010:12-64.

［6］ABRIALJ R，BUTLER M，HALLERSTEDE S，et al.Rodin:an open toolset for modeling and reasoning in E-vent-B ［J］.International Journal on Software Tools Technology Transfer，2010，12(6):447-466.