基于SPARCv8的实时嵌入式操作系统的异常管理验证
Verification of Real Time Operating System Exception Management Based on SPARCv8
-
摘要: 1.研究背景(Context)：
航天器等安全关键系统是典型的嵌入式系统，具有多任务并发、中断频发等特点，操作系统是其最基础的软件，构建一个正确的操作系统是保障航天器系统高可信运行的关键。同时，异常管理作为操作系统最底层的功能负责引导系统控制流的突变来响应处理器状态中的某些变化，异常控制流发生在计算机系统的层次，硬件检测到的事件会触发控制突然转移到异常处理程序，内核通过上下文切换将一个用户任务转移到另一个用户任务。因此，异常管理的正确性是整个操作系统正确性的基础。然而，现有的OS验证项目要么不对异常管理进行建模，要么使用基于抽象层的建模方法来验证异常管理的正确性，这些方法隐藏了机器底层的细节元素，如寄存器、内存堆栈等，无法在汇编层上保证该模块的正确性。
2.目的(Objective)：
我们研究的目的是通过基于严格数学推理的形式化方法对运行在航天器上的操作系统的异常管理模块进行建模与验证，针对嵌入式操作系统内核验证中存在的需求到代码的一致性验证、完整系统的统一验证、底层模块验证及高效可信工具四个问题开展理论、方法和工具的研究，实现对航天器嵌入式微内核操作系统SpaceOS的全面验证，为航天器系统的在轨稳定运行打下基础。
3.方法(Method)：
在之前的研究工作中，我们使用了一种高层抽象的方法对异常管理模块需求层的正确性进行了验证。本篇论文基于之前工作的基础，对异常管理的设计层与代码层开展形式化验证工作。我们提出了一种基于霍尔逻辑的验证框架EMS，首先对异常管理涉及的系统基本元素进行数学描述，然后将系统处理异常事件的流程划分为了六个阶段建立状态迁移模型，最后给出前置条件和后置条件来验证该模块的功能正确性。所有的形式化和证明都在交互式定理证明器Coq中实现。
4.结果(Result)：
以实际运行在北斗三号卫星上的SpaceOS为载体，我们使用EMS框架成功验证了该实时嵌入式操作系统异常管理模块的功能正确性。
5.结论(Conclusions)：
本篇论文是对我们验证思想的探索与实现，我们的思想是针对工程应用中的实际操作系统进行形式化验证，为了全面保证操作系统内核的可信性，将分层次地对内核进行抽象描述和建模，模型将涵盖内核实现过程中的需求、设计和实现各阶段。在各抽象层上进行关键性质的形式化规范和验证，确保系统模型满足系统需求；在不同的层次之间进行精化和一致性验证，一致性验证包括模型的一致性，也包括性质的一致性验证。逐层精化的最后，要进行模型和代码的一致性验证。如果不同模型间或者模型代码之间存在差异，则将差异带入高层模型，再自上而下进行迭代证明，直到不存在差异。Abstract: 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.
下载: