机载分区操作系统形式化建模及验证研究

彭 寒，曹国震，吴晓葵

(西安航空学院 a.计算机学院；b.教务处，西安 710077)

0 引言

综合模块化航空电子架构(Integrated Modular Avionics，IMA)已成为当今航空、航天计算机的主流架构，其主要目标是实现分区操作系统，支持多个系统的时间分区和空间分区，以达到最大的资源利用率，减轻机载设备重量，减小飞机体积。机载分区操作系统为应用程序提供时空隔离的保障，从而实现故障隔离，避免故障传播，并为不同安全级别的分系统提供物理上的隔离机制。为实现分区操作系统的标准化，美国航空无线电公司提出了机载分区操作系统实现规范——ARINC 653标准，旨在规定分区操作系统和机载应用程序之间的接口，以支持机载安全关键系统的开发认证和验证。ARINC 653标准经过不断的改进和完善，已经覆盖了分区操作系统的核心服务、扩展服务、文件系统、测试验证标准等各个方面。以ARINC 653标准为依据的各种分区操作系统也已得到了广泛应用，例如，VxWorks653、INTEGRITY-178B，LynxOS-178，PikeOS和开源软件POK及 Xtratum。

分区操作系统作为机载系统的重要基础软件，对其安全性、可靠性有着严苛的要求。由于分区操作系统的复杂性，其安全性往往难以通过测试和仿真来保证，根本原因在于软件工程中的需求分析、设计和验证通常采用非形式化语言来完成，而这种方式存在很大的二义性、模糊性，缺乏严格的数学证明。对于安全关键的机载分区操作系统，需要一种严格的、可靠的、实用的方法实现对复杂系统的管理。因此，在各种航空软件安全性规范(如DO-178C)中，已经明确提出了要采用形式化方法对嵌入式系统进行建模和验证。本文在国内外机载分区操作系统形式化建模及验证研究工作的基础上进行了分析总结，指出了当前该领域存在的问题，并提出了新的发展思路。

1 分区操作系统形式化建模与验证研究现状

分区操作系统的形式化建模通常是根据建模者的经验，先设计抽象规约，然后逐步精化为底层模型，最终得到最贴近具体实现的精化模型。当前分区操作系统的形式化建模的研究包括分区操作系统的内核建模研究和分区操作系统规范的建模研究。

1.1 分区操作系统内核建模

Craig[1]使用自动化的建模与验证工具Z Notations 设计并精化了一个较为完整的操作系统的内核，并证明了可以将其直接转换为C语言的可执行代码；而后，又进一步设计和精化了一个分区操作系统的内核，该内核提供了分区操作系统的大部分的功能。Craig使用定理证明方法对几个内核属性进行了基本的验证，Craig设计的分区操作系统的形式化规约是一个较为完整的规约，其精化的级别已经达到了可以直接转换为C代码或者Ada代码的程度。但是Craig的设计中没有建立分区内进程的模型，另外，对于硬件设备的建模较为简略，其形式化规约和正确性证明都是完全靠人工完成的。

Velykis在Craig研究的基础上，考虑了更多的安全性需求， 使用自动化的建模与验证工具Z Notations完成了分区操作系统的进一步的规约和验证[2]，使用Z / Eves自动定理证明器对其形式化规约进行了验证，消除了Craig的模型中的语法错误，并验证了其API的可行性和健壮性，其改进的分区操作系统的形式化模型是完全使用定理证明器自动证明的。但是，Velykis的形式化规约中没有涉及分区隔离方面的证明，其改进的的形式化模型侧重于分区操作系统内核中的核心数据结构，例如进程表、队列和调度程序，主要是改进了 Craig的调度器模型，并将调度器的某些行为属性(如调度器死锁分析)从非形式化的需求转换为数学不变量来完成了证明。而对于其他组件，如消息传递或内存管理，则没有使用自动证明。

Critical软件公司的Andre使用形式化建模语言—B语言设计了一个安全的分区操作系统内核(secure partitioning kernel ,SPK)的形式化模型。其研究成果首先是完整的开发了SPK的顶层模型，完成系统的架构设计，并用ProB[3]工具进行了仿真和验证。顶层的SPK抽象模型由内存管理、调度、内核通信、流策略、时钟模型等组成。而后，经过验证的顶层模型可以精化为完全形式化的精化SPK，并最终精化到可以从其自动生成C代码的级别，这个精化过程是在Atelier B工具的协助下完成的。

Kawamorita 等人也应用B语言开发了安全的嵌入式设备上的分区操作系统内核OS-K，并在Intel的IA-32架构上搭建了该操作系统的原型[4]。Kawamorita使用B语言作为形式化模型的开发工具，并用Spin工具验证了该模型的属性，同时，他使用B4free工具自动验证了模型的正确性和一致性。最终的分区操作系统内核提供了几个核心的功能：分区管理、分区间通信、分区间通信的访问控制、内存管理、定时器管理、处理器调度、设备驱动程序操作和中断处理的I/O中断同步。

Phelps等人使用Alloy语言设计了一个安全的分区操作系统的安全策略的形式化模型和顶级规约，并用分析工具验证了该规约的一致性。该规约精化了分区间信息流策略模型，并且使用状态转换系统建立了两个相互连接的分离的子系统，初始化时的子系统和运行时子系统。

Martin等人使用形式化规约开发软件SPECWARE开发了MASK分区操作系统，并进行了三次精化[5]，其抽象规约主要涉及内核数据结构的规约，而最终的底层规约被手工翻译成C源代码。

为了保证Xenon分区操作系统的信息流安全性，Freitas和McDermott使用Circus建模语言建立了Xenon分区操作系统的形式化模型[6]。Murray 等人用Isabelle/HOL建模语言完成了对安全的分区操作系统内核seL4的建模和验证，他们将seL4的规范用于验证分区操作系统的信息流安全性，规范中定义了基于分区的轮转调度策略，给每个分区分配了固定的时间窗口。欧盟EURO-MILS项目以PikeOS操作系统的精确建模和安全策略建模为目标，用Isabelle/HOL建模语言设计了一个通用的分区操作系统CISK(Controlled Interruptible Separation Kernel)的形式化模型，该模型包含了分区操作系统的几个方面，例如中断、分区之间的上下文切换和控制，其规约较为详细，适用于工业系统的形式化验证。Sanan等人在基于欧洲航天局的IMA for Space项目中，用 Isabelle / HOL建模语言构建了通用的分区操作系统内核的功能模型和安全模型。该规范使用ARINC 653作为功能需求，为了服务于最终的软件实现，也涉及到了硬件虚拟化、CPU定时器和内存管理的模型。赵永望等人使用Isabelle / HOL建模语言设计了ARINC 653兼容的分区操作系统的顶层模型，其中考虑了ARINC 653的分区管理、分区调度和通信服务。

1.2 分区操作系统规范建模

由于分区操作系统规范的内核接口规范中规定了内核需要为应用程序提供的核心服务，对分区操作系统规范的建模需求也日渐迫切，因为形式化的分区操作系统接口模型能够支持对分区应用程序的形式化建模与验证。York大学的Gomes 用Circus建模语言建立了针对IMA系统的ARINC 653规范的形式化模型，Camara 等人对运行在ARINC 653兼容的分区操作系统之上的应用程序进行了建模和验证[7]。北京航空航天大学的赵永望等人使用Event-B建模语言建立了ARINC 653第1部分的57项服务的系统功能的形式化模型，他们使用Event-B建模语言中的精化结构将ARINC 653抽象模型逐步精化，并将ARINC 653的服务要求转换为了底层模型。赵永望利用Event-B的逻辑推理的能力证明了该规范的三个隐藏的错误和不完整之处，是一个将Event-B建模语言用于复杂系统建模与验证的很好的范例。

虽然目前已有对分区操作系统的形式化建模的研究，但是还没有直接从某个分区操作系统的形式化模型直接生成可执行代码的报告。

2 分区操作系统的形式化验证

分区操作系统的形式化验证通常是从已有的操作系统代码中抽象出形式化模型，并验证这个抽象模型的各种属性。分区操作系统的形式化验证主要包括对时间隔离能力和空间隔离能力的验证，其中空间隔离能力指的是数据的隔离，也就是数据存储和数据通信的分离，即不能有非法的、不安全的访问和分区间的故障传播。分区的时间隔离能力则确保了共享资源为分区中的软件提供的服务不会受到其他分区中的软件的影响，包括计算资源的性能、调度资源的速率、延迟、抖动和持续时间。

2.1 空间隔离能力验证

Baumann 等人在一个航空电子项目的子工程中用VCC验证工具验证了PikeOS分区操作系统源代码的所有系统调用功能，也就是内核提供给应用程序的核心服务的正确性。他们提出了顶层抽象模型和底层实现的操作系统及应用程序构成的系统之间的模拟关系定理，并识别出了为保证分区操作系统内核的整体正确性而需要所有组件所具备的属性。因为建立在PikeOS分区操作系统源代码上的安全关键系统依赖于空间分离机制的正确实现，所以对它的验证必须考虑内存隔离的正确性。因此，Baumann等人使用VCC工具对PikeOS分区操作系统的关键组件，即内存管理器进行了源代码的级别的验证。

Richards对格林希尔公司的商业化分区操作系统INTEGRITY-178B进行了安全性验证[8]，其验证考虑了五个要素：(1)描述系统相关安全属性的形式化规约；(2)系统功能性接口的形式化表示；(3)系统高层设计的半形式化表示和抽象表示；(4)系统低层设计的半形式化的、详细的表示；(5)用来表示上述四个要素对之间的对应关系的模型。该系统被建模为状态转换系统，它接收系统的当前状态以及任何外部输入作为输入，并产生新的系统状态以及任何外部输出。Richards采用这种方式验证了INTEGRITY-178B的高层模型信息流安全性，系统的低层设计采用ACL2定理证明器建模，并保证了ACL2模型与C代码的对应性。

基于ARM的嵌入式分区操作系统PROSPER的内核由150行汇编代码和600行C代码组成，Dam通过证明抽象规约和内核二进制代码之间的相互模拟关系，对PROSPER的信息流安全性进行了形式化验证，其系统模型仅考虑分别在两个独立的特殊ARMv7机器上执行的两个分区，分区间通过异步消息传递进行通信，最终验证了除了通过指定的通信通道之外，分区之间不会有任何直接或间接地影响。具体做法是确保除了通过显式使用预先指定的通道来实现通信外，分区间无法通过读/写其他分区的内存、寄存器的内容来访问其它分区。

2.2 时间隔离能力验证

时间隔离需要用分区操作系统的调度器来实现，因为它负责将处理器时间分配给分区。根据ARINC 653标准，时间分离需要两级调度器，分别为分区级调度器和进程级调度器。

霍尼韦尔动态执行操作系统(Dynamic Enforcement Operating System，DEOS)是一个基于微内核的实时操作系统，通过在进程级别提供空间隔离和在线程级提供时间分区来支持灵活的IMA应用程序。NASA与霍尼韦尔合作，将DEOS的调度内核的核心部分包含10个类，超过1000行的C++代码翻译成Promela，并在Spin模型检测工具中进行了验证[9]。他们使用两种方法来分析DEOS内核中的时间隔离属性。第一种方法是建立程序变量的断言以识别潜在的错误。如果模型检查器发现了断言背离，则可以仿真所报告的错误的执行路径，并且可以确定这个路径是否真的是错误的执行路径。第二种方法是使用LTL表达的活性属性Idle Execution，其形式为(beginperiod->(！endperiod U idle))。这个活性属性表示如果系统中有时间松弛(即主线程没有100%的CPU利用率)，则空闲线程应该在每个最长的周期内运行，这是时间隔离的必要条件。该系统的大小和复杂性限制了它们一次只能分析一个配置。为了克服这个局限性，Ha等人使用定理证明的方法将DEOS的验证推广到任意配置，利用PVS定理证明器来分析DEOS调度器。他们使用离散时间状态转换系统对PVS中的调度器的操作和DEOS的执行时间线建模，时间隔离属性被建模为状态集合上的谓词，并被证明适用于所有可达到的状态，整个理论模型共有1648行PVS代码和212个引理。除了时间隔离不变量的归纳证明之外，他们还使用基于特征模型的技术来模拟状态转换系统并确定归纳不变量，这种技术对于渐增复杂度的系统的增量式的定理证明非常适用。

Asberg等人使用时间任务自动机对WindRiver的分区操作系统VxWorks进行建模，并使用Times工具对其进行了验证。他们使用时间任务自动机建立了全局调度器、分区内本地调度器和事件处理程序的模型，用事件处理程序模型将全局调度器和分区个数的变化解耦。Asberg用时间计算树逻辑TCTL建模了分区内局部调度器和全局调度器应满足的安全性需求，例如“当分区处于活动状态时，分区内任务就绪队列中优先级最高的任务应始终是服务器当前正在运行的任务”。

2.3 讨论

通过对国内外分区操作系统形式化建模与验证技术研究现状的分析，我们可以发现，大多数对空间隔离能力进行的建模和验证都采用了定理证明的方法，原因在于模型检查方法由于其状态空间爆炸问题无法完整地验证操作系统的所有可能执行路径，并且很难用属性建模语言(如LTL和CTL)表达空间隔离属性。反之，验证时间隔离属性时，通常会使用模型检验方法，这是因为在各种模型检查器中可以很方便地表达时间属性，例如UPPAAL工具中的时间自动机。

3 现有建模及验证研究中存在的问题

虽然国内外研究人员已在分区操作系统建模及验证方面做了一定的工作，但是这些研究目前尚存在下述问题。

3.1 验证工作的不充分性

目前分区操作系统验证的工作通常是对已有的操作系统代码的“设计后验证”，所验证的模型仅仅是实际系统的一个抽象，只能体现系统的可能行为，而不是全部行为。这种方法最大的问题在于必须保证抽象出来的形式化模型与原来的源代码的行为是一致的，而事实上，无论这个抽象过程是自动的还是人工的，都无法避免不一致性。因此，这些验证工作是不充分的。

3.2 建模与验证方法的单一性

目前已有的分区操作系统建模及验证方法主要侧重于建模或者验证系统的某个方面的属性，很少能够完整地覆盖多个方面的属性建模和验证需求。例如，Event-B、B、Z等基于数据精化的建模语言主要注重于保证模型精化的一致性，而无法对各种时态逻辑属性进行验证。时间自动机、状态转换系统等工具可以很方便的建模和验证模型的行为特性，而对于数据精化方面的支持则比较弱，缺乏同时考虑数据精化特性和行为属性的形式化模型和验证研究。

3.3 缺乏对交互环境的建模与验证

当前的分区操作系统的形式化模型并没有区分“环境”和“系统”，基本上都是将环境和系统放到一起，构成一个封闭的系统。所谓“环境”就是会和操作系统产生交互的系统，如硬件系统和应用软件。现有的研究成果或者是没有考虑这些因素，或者是将这些因素作为了分区操作系统模型的一部分，混淆了系统所处的环境模型和系统本身的模型，这些模型对于验证规范和标准是可行的，但对于需要根据模型生成最终代码的工程师来说则是不可接受的。

4 分区操作系统建模及验证的新思路

针对当前分区操作系统建模及验证的研究工作中存在的问题，本文提出以下三种新的思路，以期对未来研究工作有所借鉴。

4.1 从“设计后验证”到“Correct-by-Construct”方法

传统的形式化方法只考虑了软件寿命周期的需求规约阶段和最终的测试验证阶段，而没有控制中间的设计和实现过程。Correct-by-Construct方法是近年来学界所提倡的新的、更科学的形式化方法。其含义为“构建即正确”，即软件的正确性应该是通过正确的“设计(构建)”来保证的，而不是通过验证来保证。Correct-by-Construct方法能够从需求规约开始，逐步精化规约模型，得到设计模型，直到生成最终的实现代码，并保证整个精化过程的正确性。对于安全关键的机载分区操作系统来说，必须采用这种方法“构建”出正确的分区操作系统。

4.2 从规约模型到契约模型

现有的分区操作系统模型未能区分系统模型和系统所处的“环境”的模型，完整的建模分区操作系统和其所处的“环境”的模型会让模型的规模变得极为复杂也是不现实的。因此，可以采用契约式设计与验证的思路，建立系统和环境的“契约”，有效地分离系统模型和环境模型，即定义系统和环境之间的接口。只要分区操作系统满足这个契约，就是可行的实现方案。在实际操作的过程中，可以建立底层硬件应该满足的行为的契约，甚至是分区操作系统的底层支撑操作系统所提供的接口模型作为分区操作系统的环境模型。

4.3 组合运用多种形式化建模方法

形式化建模语言因其专用性的特点，很难同时考虑系统的多方面的属性建模与验证。例如，某些建模语言主要擅长建模系统的行为方面的属性，而另一些建模语言则专注于时间属性的建模。为应对这个问题，研究人员通常会根据实际需求对某些形式化建模语言进行扩充，使其能够表达更多方面的属性。但事实上是不存在能够表达系统所有方面属性的形式系统的，而且很多形式系统中有大量不需要的语法元素。一种比较灵活的且更为现实的做法是根据实际的系统建模与验证需求，组合运用多种形式化方法，这样，建模者只需要选择合适的形式系统用来满足建模和验证需求，就可以将研究重点转向系统模型的构建、精化和属性验证上。

5 结语

本文通过分析国内外关于机载分区操作系统建模及验证方面的研究成果，指出了其研究工作中存在着验证工作不充分性、建模与验证方法单一性、缺乏对交互环境的建模与验证等问题，并针对这些问题，提出了从“设计后验证”到“Correct-by-Construct”、从规约模型到契约模型、组合运用多种形式化建模三种新的研究方法及解决方案，为进一步开展机载分区操作系统建模及验证工作提供了指南。