符合实时AUTOSAR OS的形式化设计和验证方法

汽车开放系统架构（AUTOSAR）是一套文档，为汽车软件的实现提供指导。操作系统软件规范（SWS_OS）对符合 AUTOSAR 标准的操作系统的接口和功能需求进行了标准化。仅仅实现所需的接口并不足以证明符合 AUTOSAR 标准，重要的是要表明接口之间的交互满足 SWS_OS 中概述的功能需求。

关键的汽车应用依赖于底层操作系统的正确实现。操作系统的设计和开发遵循 AUTOSAR SWS_OS，该标准对所有符合 AUTOSAR 的操作系统的应用程序编程接口（API）及其背后的功能行为进行了标准化。

通常，这些需求由专家进行解释，然后专家根据自己的知识和专业技能来实现操作系统。然后，通过一系列测试用例对实现进行测试，以证明实现与 SWS_OS 中的规范是一致的。然而，要通过形式化证明来表明实现确实遵循这些规范，仍然是一项具有挑战性的任务。

本文介绍了一种用于形式化规范和验证给定实现是否符合 SWS_OS 规范的方法。我们的方法包括形式化定义功能需求，并使用形式化推理来证明实现符合这些需求。我们已将此方法应用于一个广泛使用的实时操作系统（RTOS），通过确保其满足必要的功能特性，来证明其符合 AUTOSAR 标准。

SWS_OS 按模块组织，每个模块都规定了所需的 API 和功能需求。这使得实现包含一个大型代码库，通常用 C 语言编写，用于满足功能需求并实现每个模块所需的 API。此外，API 之间是相互依赖的，即满足特定功能需求需要一系列 API 调用。

我们方法的主要贡献是形式化操作系统的预期行为。所谓预期行为，是指导致满足给定功能需求状态的 API 调用序列。API 调用序列是参与功能需求的 API 规范的结果。操作系统的预期行为在 Dafny 中被编码为一个引理。然后，使用 Dafny 定理证明器，我们表明各种 API 的抽象之间的交互满足所需的功能需求。

在整篇文章中，为了可读性或受篇幅限制，省略了 Dafny 实现的细节。在这种情况下，符号（§）表示可以在网上找到详细信息。

API 规范是使用形式化推理技术从 API 中导出的一阶逻辑公式的抽象。这些规范是 API 实际实现的等效表示。由于这些抽象与 C 代码等效，因此功能需求得到满足的证明可以直接扩展到 C 代码。

运行在符合 AUTOSAR 标准的操作系统之上的汽车应用由一组任务组成，这些任务实现了应用的预期逻辑。这些任务具有明确的属性，如周期、优先级、可能使用的共享资源、响应的事件等。SWS_OS 规定了一个任务状态机，描述了任务的各种状态以及这些状态之间的转换，如图 1 所示。

图1：任务状态机

图 1 中转换的标签是参与任务管理的 API。此外，SWS_OS 要求任务必须具有固定的优先级，并且必须按优先级顺序执行，即在准备执行的任务（处于就绪状态的任务）中，优先级最高的任务将执行。这是实现必须遵守的重要安全属性。

例如，最初在系统启动时，所有任务都处于挂起状态。根据配置，一个或多个任务被激活并转换到就绪状态。在这些任务中，优先级最高的任务转换到运行状态。此外，稍后可能会激活另一个优先级高于当前运行任务的任务。这个新任务会导致抢占，此时之前运行的任务转换到就绪状态，而新任务转换到运行状态。此外，当前运行的任务可以等待事件。在这种情况下，任务转换到等待状态。当任务收到相关事件时，它再次转换到就绪状态，等待转换到运行状态的机会。当任务完成其执行时，任务终止并转换到挂起状态。

任务可能还需要以互斥的方式使用共享资源，如数据结构、公共变量、通信接口等。SWS_OS 要求在单核系统中使用最高锁定协议（HLP）来管理对共享资源的访问。HLP 是优先级上限协议（PCP） 的一种变体，其中任务的优先级在请求共享资源时立即提高到共享资源的上限优先级。任务也可以以嵌套方式获取多个共享资源，如图 2 所示。

图2：共享资源嵌套示例

任务可以使用的共享资源数量必须在设计时确定。共享资源的上限优先级等于被配置（或有资格）访问该共享资源的最高优先级任务的优先级。SWS_OS 规定了 GetResource 和 ReleaseResource API，用于获取和释放共享资源。需要注意的是，嵌套的共享资源必须按照与获取顺序相反的顺序释放。如果嵌套共享资源的释放顺序与获取顺序不相反，将导致无效的系统状态。

有了本节介绍的相关背景信息，我们现在将描述我们的方法。论文的其余部分安排如下：在第 3 节中，我们将介绍我们的方法。在第 4 节和第 5 节中，我们将把我们的方法应用于一个广泛使用的符合 AUTOSAR 标准的实时操作系统。我们将形式化 SWS_OS 的需求，然后将形式化推理的思想应用于实时操作系统中相关 API 的实现。最后，我们在第 6 节和第 7 节中分别讨论了该方向的一些相关工作，并提出了该工作的一些未来方向。

我们的方法包括 3 个步骤，如下所述。

1. SWS_OS 的形式化：在这一步中，我们分析 SWS_OS，以形式化功能需求并确定与功能需求相关的 API。这一步有几个成果。首先，导出一阶逻辑中的公式，该公式以数学方式表示功能需求。其次，我们提出引理来检查规范的一致性。

功能需求由一个或多个 API 实现。此外，功能需求独立于这些 API 的实现。这一步使我们能够形式化 API 调用或一系列 API 调用必须满足的系统不变量。

为了检查系统不变量的形式化是否正确，我们确定系统不变量的特征属性。我们将这些属性作为引理提交给 Dafny 定理证明器。现在，规范的强度由定理证明器能够自动证明的引理数量决定。我们利用这一思想来加强系统不变量的形式化，使定理证明器能够自动证明所需的引理。然而，并非所有规范都是如此。如果定理证明器无法自动证明规范的特征属性，我们需要使用 Dafny 提供的断言技术来证明引理。

2. 实现的抽象：在这一步中，我们将源代码形式化，并导出参与满足不变量的相关 API 的抽象。确定相关 API 相对容易：SWS_OS 规定了相关的 API。然而，挑战在于证明抽象与源代码是等效的。

我们使用最强后置条件（SP）演算来导出抽象。对于给定的语句 α 和前置条件 P，最强后置条件 SP (α) P 是一个命题，描述了在满足 P 的任何前置状态中执行 α 所产生的状态集。该演算提供了一组公理，允许我们执行符号执行。语句或函数（即一系列语句）的 SP 的重要属性是，SP 是给定初始前置条件的充分且必要的后置条件。

我们将 SP 演算应用于 API，以抽象地推理 API 中每个语句的效果，而无需关注实现细节。该演算给出一个命题，该命题是 API 中每个语句的后置条件的合取。需要在此提及的是，到目前为止，我们是手动将 SP 演算应用于给定的 API。然而，自动化这一步是可能的，我们已经在朝着这个方向努力。

3. 系统不变量的保持：我们方法的步骤 1 的分析导出了一个必须在时间上保持不变的命题。在步骤 2 中，我们导出了参与满足功能需求的相关 API 的抽象。在这一步中，我们表明 API 调用或一系列 API 调用保持了系统不变量。

为了证明系统不变量得到保持，我们必须表明，如果在系统不变量成立的状态下调用第 i 个时间步的 API，那么在第 (i+1) 个时间步，API 调用或一系列 API 调用会导致一个新的状态，其中系统不变量得到保持。这被称为不变性引理。

为了自动证明不变性引理，有必要确定建立不变性的 API 调用序列。这个调用序列是符合规范的系统的确切行为。例如，如图 1 所示，转换到就绪状态的任务必须明确处于挂起或等待状态。此外，当一个任务转换到就绪状态并进入就绪队列时，可能会出现该任务导致抢占的情况，在这种情况下，必须调用调度程序。这一步使我们能够识别这样的序列，从而证明 API 满足规范。

我们考虑 EB tresos®AutoCoreOS的实现，这是 Elektrobit GmbH 开发的在汽车行业中广泛使用的操作系统。在本文的其余部分，我们将其简称为 AutoCoreOS。AutoCoreOS 配备了一个配置和生成工具 EB tresos®Studio，用于设置任务、资源、调度表等。

在本文中，我们将形式化 AutoCoreOS 中实现的任务状态机和单核资源管理协议 HLP。由于 SWS_OS 的存在，识别与任务管理和任务状态机相关的所需 API 虽然不容易，但还是可行的。然而，这一步可以使用方法实现自动化。AutoCoreOS 有许多可选的调试和运行时功能。这些功能，如调试跟踪、与旧应用程序兼容的遗留代码等，可以使用 Tresos 软件进行配置。我们假设这些选项被禁用，因为它们不影响我们的分析。

我们还假设对 API 的调用是原子的，即每个 API 要么执行完成，要么根本不执行。这些 API 被实现为内核系统调用。为了确保这些系统调用是原子的，通常的技术是在进入系统调用时禁用中断，然后在退出系统调用之前重新启用中断。为简单起见，我们假设对内核数据结构的修改是原子的。

AutoCoreOS 还允许多个相同任务的实例（或激活）。这意味着例如，一个已经处于运行状态的任务可以再次被激活。然而，任务实例的数量上限在设计时是可配置的，我们假设这个上限是 1。

考虑到这些假设，我们现在将我们的方法应用于 AutoCoreOS。

4.1 任务控制块

任务是一个可执行实体，与应用程序的其他任务一起实现应用程序的预期逻辑。SWS_OS 规定了任务的定义。我们使用这个规范在 Dafny 中导出一个任务数据类型，如下所示。

应用程序中的任务集在设计时确定，不会改变。我们通过将任务的数学集定义为常量来反映这一规范。该规范还定义了两种类型的任务：必须最终终止的基本任务和可能进入等待状态并等待事件的扩展任务。

清单 1：任务数据类型

清单 1 中的 Task 数据类型指定了任务控制块的字段（§）。任务 ID 和优先级在设计时使用 Tresos 配置工具进行配置。任务的类型（扩展或基本）也在设计时配置。如果任务的类型是扩展的，我们可以选择性地配置该任务将响应的事件。任务控制块中的 events 字段是事件 ID 和布尔值之间的映射，指示特定事件是否已设置。

任务结构的一个重要字段是任务的上下文。任务的上下文是一组 CPU 寄存器，如程序计数器、栈指针等，它们保存任务的当前执行环境。根据底层硬件架构，任务上下文的管理可能有很大差异。在这项工作中，我们不涉及验证的硬件级方面，因此我们将任务的上下文抽象为一种未解释的数据类型。然而，我们指定这种抽象数据类型可以进行比较（==），并且不是基于堆的（new）。

AutoCoreOS 定义了与任务相关的两种数据结构：一种静态结构，用于保存任务的静态生成配置；另一种动态结构，用于保存执行任务所需的运行时信息。例如，任务的排队优先级在设计时使用 Tresos 静态定义，而任务的上下文是动态的，在运行时会发生变化。

此外，AutoCoreOS 有两种不同的任务类型：基本任务和扩展任务。基本任务不能调用 WaitEvent 系统调用来进入等待状态，必须最终调用 TerminateTask 系统调用来转换到挂起状态。另一方面，扩展任务可以进入等待状态，可能终止也可能不终止。

4.2 就绪队列

SWS_OS 规定，处于就绪状态的任务必须按优先级顺序执行。然而，该规范没有描述必须使用什么算法来实现这一点。解决这一规范的有效方法是在 Dafny 中实现一个优先级有序数组或序列。Dafny 中的序列是一种不可变的数据类型，表示一个有序列表。我们将就绪队列（处于就绪状态的任务队列）指定为 Dafny 中的一个序列。我们还在式 1 中指定该序列是按优先级排序的。

任务状态机的一个重要系统不变量是按优先级排序执行。我们可以使用我们对就绪队列的形式化来形式化这个系统不变量。为了指定这个系统不变量，我们观察到在任何给定时间，就绪队列可能为空，也可能不为空。如果就绪队列为空，则所有任务都处于挂起或等待状态。

如果就绪队列不为空，则它必须是排序的，就绪队列中的任务处于就绪状态，并且队列头部的任务是当前运行的任务。

我们要验证的系统不变量是式（2）和式（3）的析取（∨）。在本文后面，我们将这个析取称为 validSM。

AutoCoreOS 的就绪队列使用基于优先级的链表，确保任务始终按优先级排序，优先级最高的任务在头部，准备运行。当一个任务被激活时，它被放置在该列表的正确位置。我们的形式化与 AutoCoreOS 的方法在功能上是等效的，因为两者具有相同的循环不变量和终止条件。由于我们不比较内存效率或性能，这种功能等效性就足够了。然而，为了有效地推理基于链表的算法，我们需要使用 Dafny 中的动态帧概念来解决帧问题。

任务的数量在设计时配置并固定。因此，链表的长度是固定的。AutoCoreOS 将就绪队列实现为一个长度等于任务数量的数组。对于每个任务，相应任务结构中的 “next” 指针指向就绪队列中的下一个索引，下一个更高优先级的任务在该索引处入队。实现通过跟随每个任务节点的 “next” 指针来解析就绪队列。

通过在 Dafny 中将就绪队列形式化为一个序列，我们确保最高优先级的任务始终在索引 0 处，并且随着我们在序列中向上移动，优先级降低。这如图 3 所示。

图3：链表和Dafny序列之间的等价性

AutoCoreOS 提供了一个 API，用于将新激活的任务入队到就绪队列中。使用我们的抽象，我们在 Dafny 中实现了一个类似的方法。Dafny 方法使用 requires 和 ensures 子句来表示前置条件和后置条件。这里，前置条件确保在插入新任务之前就绪队列是排序的，后置条件保证插入后仍保持排序。

SWS_OS 规定只能有一个运行中的任务，并且该任务是所有处于就绪状态的任务中优先级最高的。我们的规范遵循这一点，我们通过在 Dafny 中提出一个引理来证明这一点（§）。这表明我们的规范与 SWS_OS 一致，确实是对规范的正确解释。

4.3 ActivateTask 系统调用

如图 1 所示，ActivateTask 函数将任务从挂起状态转换到就绪状态。ActivateTask 函数还根据任务的优先级将其入队到就绪队列中。ActivateTask 在 validSM 成立的状态下被调用。我们首先使用 SP 演算导出 ActivateTask 的抽象。我们展示了实现的规范化版本，其中所有可选代码段都被删除（td 指向任务控制块）。

清单 2：AutoCoreOS 的 ActivateTask 函数摘录

我们关注的是避免导致错误状态的语句序列。我们的目标不是证明存在导致系统调用失败并使操作系统进入未定义状态的序列。我们的意图是表明，如果系统调用中的语句序列无错误地终止，那么该系统调用将保持系统不变量。对于 ActivateTask 系统调用，该条件确保了任务在被激活之前必须处于挂起状态。该条件的 “else” 部分是导致错误状态的语句序列。

清单 3：为 ActivateTask 导出 SP

如清单 3 所示，我们使用 SP 演算导出 ActivateTask 函数的 SP。在清单 3 中，State 和 Prio 是抽象函数，分别表示任务的状态和优先级。这些抽象函数使我们能够推理表达式的效果，而不必担心实现细节。我们得到 ActivateTask 的 SP 为：

赋值后变量的值用 “′” 符号表示。式（4）是 C 代码的抽象。这个命题清楚地表明了 ActivateTask 无错误完成后所期望的结果。换句话说，该命题表示了函数的行为。

以类似的方式，我们导出任务状态机中涉及的每个系统调用的抽象。这些系统调用在工件中有进一步的解释（§）。

4.4 不变性引理

我们在式（1）和 validSM 中有我们的规范，以及我们系统调用的抽象，例如式（4）。现在我们准备导出一系列系统调用，这些调用导致 validSM 的不变性。

我们基于思想形式化任务状态机。我们在 Dafny 中定义一个数据类型来表示任务状态机，如下所示。字段的完整描述可以在工件中找到（§）。

清单 4：状态机数据类型

SMState 数据类型指定了任务状态机。该数据类型指定了任务与其各自状态之间的映射、当前运行的任务以及当前运行任务的上下文。通过任务状态机的这种规范，我们能够跟踪每个任务的状态。我们还能够推理当前运行任务的状态转换及其上下文。

任务的状态被编码为另一种数据类型：

清单 5：任务状态

根据状态机数据类型重写式（4），我们将 ActivateTask 系统调用形式化为：

这里，状态机的新状态表示为 sm′。函数 enqueueTask 使用我们对就绪队列的形式化，将任务插入到就绪队列的适当位置。很明显，式（4）与式（5）在语义上是等效的。任务状态机中涉及的其他系统调用也有类似的表示（§）。

现在，我们能够证明，当任务在状态机的各种状态之间转换时，系统不变量得到保持。在这方面，我们首先提出不变性引理（§）。

引理 4.1：每当状态机在系统不变量有效的状态下被调用，并且任务转换到新状态时，系统不变量在新状态中得到保持。

显然，仅式（5）本身不能满足这个引理。这是因为入队的任务可能具有比当前位于队列头部（因此正在运行）的任务更高的优先级。在这种情况下，在控制权交还给应用程序之前会发生抢占。当任务终止并从队列中移除，或者当任务因收到正在等待的事件而被激活时，也会出现类似情况。我们在这里展示了导致基本任务不变性的步骤序列。

我们展示了 AutoCoreOS 中实现的任务调度程序的抽象。任务调度程序从 AutoCoreOS 的硬件特定上下文管理部分调用。由于我们已经抽象了任务的上下文，因此我们在这里不考虑上下文管理。然而，我们指定，如果在激活系统调用完成后，更新后的就绪队列的头部与当前运行的任务不同，则上下文管理器调用调度程序。此外，AutoCoreOS 中的上下文管理确保，如果更新后的就绪队列的头部与当前运行的任务相同，则恢复该任务（图 4）。

图4:ActivateTask的不变性

在我们的抽象中，我们在两个不同的谓词中指定了这种行为（§）。任务 t 是被激活的新任务。我们在这里展示了在 OS_Dispatch 系统调用中 AutoCoreOS 实现的调度函数的抽象。

任务调度程序在 ActivateTask 系统调用完成后获得的状态中被调用。状态机的最终状态是式（5）和式（6）的合取。这种行为是 ActivateTask 和 OS_Dispatch 系统调用规范的结果。此外，在 AutoCoreOS 中也观察到了相同的行为。这意味着在激活的任务导致抢占的情况下，AutoCoreOS 保持 validSM 系统不变量。

在 Dafny 中编码这样的 API 调用序列并非易事。在清单 4 中，状态机数据类型中的 cs 字段将任务映射到其状态。这可以被视为每个任务都有自己的图 1 中的状态机实例。因此，我们引入了两个类型函数：Trace：N⁺→SMState 和 Schedule：N⁺→Task，以将时间步映射到任务状态机的状态和任务（§）。由于每个任务都有自己的状态机实例，这两个类型函数允许我们建模任务集中随机任务在状态之间的转换。

清单 6：不变性引理

在引理中，Transitions 是一个谓词，如果任何一个转换成立，则返回 true（§）。所有可能的转换都编码在这个谓词中。

如我们所见，我们使用我们的方法正式指定了任务状态机，并证明了实现的抽象始终遵循规范。由于实现的抽象与实际实现等效，我们得出结论，实际实现也遵循规范。

我们现在继续讨论 HLP 的规范，然后抽象 AutoCoreOS 中的实现。

我们在第 2 节中描述了 HLP，现在应用我们的方法来指定和验证 AutoCoreOS 中的实现。基于 SWS_OS 中共享资源的规范，我们在 Dafny 中创建了一个资源数据类型。SWS_OS 还指定了资源相对于有资格访问该资源的任务集的状态。资源可以处于两种不同的状态：已获取或已释放。此外，共享资源集在设计时静态定义，并且在操作系统的整个生命周期中保持不变。这些要求在 Dafny 中形式化如下：

清单 7：资源数据类型

共享资源的上限优先级等于所有有资格访问该共享资源的任务中的最高优先级。HLP 通过资源的上限优先级保证互斥。然而，共享资源管理协议的实际功能需求独立于实现。我们接下来指定互斥属性。

5.1 互斥

互斥属性规定，如果一个有资格的任务已获取共享资源，则不允许其他有资格的任务获取相同的共享资源。对于给定的资源（假设为 Resource 类型的 res），这个属性可以形式化如下（§）。

由于我们将共享资源管理协议视为状态机，式（7）表示该协议的系统不变量。为了验证我们的互斥规范是否正确，我们在 Dafny 中提出了一个引理（§）。该引理假设存在两个任务，它们都有资格访问给定的共享资源，并且都已获取该共享资源。如果互斥属性的规范是正确的，那么这意味着我们假设中的两个任务实际上是同一个任务。鉴于我们规范的强度，定理证明器能够自动证明情况确实如此。

5.2 释放顺序

一个任务可能以嵌套方式获取了多个共享资源。HLP 规范要求共享资源的释放顺序与获取顺序相反，即最后获取的嵌套共享资源最先释放。这一规范促使使用类栈机制来跟踪共享资源的嵌套。

我们在 Dafny 中使用序列形式化栈。我们实现了栈的特征操作 —— 入栈和出栈操作。此外，这一规范需要我们在第 4 节中已经形式化的更新后的任务结构。我们向任务结构添加了一个序列，其中序列的每个元素都是一个共享资源。每当任务获取共享资源时，该共享资源就被压入该序列；每当任务释放共享资源时，该共享资源就从该序列中弹出。更新后的任务结构如下所示。

清单 8：更新后的任务结构

清单 9：资源栈管理函数

5.3 HLP API

我们将 HLP 指定为状态机。我们指定了另一种类似于 SMState 的数据类型，以跟踪获取共享资源并最终释放它的任务的状态转换（§）。

清单 10：资源状态管理器

如图 2 所示，与该协议相关的有 2 个 API：GetResource 和 ReleaseResource。我们现在使用我们方法的第 2 步来分析这些 API，从 AutoCoreOS 的实现中导出抽象。

重要的是要注意，与共享资源管理相关的 API 是 C 函数。这意味着任务要获取或释放共享资源，必须处于运行状态。根据任务状态机的规范，系统中只能有一个运行中的任务，此外，我们还假设进入系统调用时中断被禁用，这意味着只有当前运行的任务可以获取或释放共享资源。因此，对于 HLP，要求任务状态机处于有效状态（validSM）。

我们在这里展示了获取（式（8））和释放（式（9））共享资源的抽象。

AutoCoreOS 使用基于链表的栈来跟踪对 GetResource 的嵌套调用。我们已经在图 3 中展示了链表和 Dafny 序列之间的等效性。我们的栈抽象与 AutoCoreOS 中的实现是等效的，因为前置条件和后置条件是相同的。此外，如果任务在未先调用 GetResource 的情况下调用 ReleaseResource，将导致错误。AutoCoreOS 会检查最后获取的锁是否是正在释放的锁。我们将锁定序列规范为栈，确保这种行为在我们的抽象中得到反映。

5.4 HLP 的不变性引理

类似于任务状态机的不变性引理，我们必须表明，当任务在共享资源状态机的各种状态之间转换时，式（7）的不变性得到保持。在这种情况下，我们使用另一个类型函数来跟踪资源状态机的状态，该函数返回每个时间步的共享资源状态机的状态（§）。

HLP 的不变性引理表明，如果有资格的任务获取或释放共享资源，式（7）将保持不变。此外，它还指出，调用 GetResource 或 ReleaseResource 系统调用的任务是当前执行的任务。鉴于我们的规范的强度和相关系统调用的抽象，Dafny 定理证明器自动证明了这个引理。

HLP 的一个重要属性是，每当任务获取共享资源时，任务的优先级会提高到共享资源的上限优先级。这确保了需要相同共享资源的任务之间的互斥。然而，这并不影响任务按优先级顺序执行。任何优先级高于当前获取的共享资源的上限优先级的任务都可能导致抢占。不变性引理还确保，当任务在 validSM 和式（7）成立的状态下调用共享资源状态机时，转换后，validSM 和式（7）仍然成立。

通过我们的方法，我们（1）正式指定了 HLP 共享资源管理协议，（2）导出了 AutoCoreOS 中实现的 API 的抽象，（3）证明了实现始终遵循规范。

Fengwei Xu等人提出了一个用于抢占式操作系统内核的实用验证框架，该框架将 API 实现的正确性建模为其抽象规范的上下文精化。他们将其方法应用于 μC/OS-II，以验证重要属性，如无优先级反转。作者将内核正确性建模为具体实现和抽象规范之间的上下文精化。作者提供了一种规范语言，用于定义操作系统内核的高级抽象模型，并开发了一种程序逻辑，用于具有多级中断的并发内核代码的精化验证。使用 Coq 定理证明器的自动策略实现验证自动化。

我们的工作不同之处在于从具体实现中导出抽象的方式。作者开发了一种用于抽象操作系统内核的规范语言，而我们使用 SP 演算来导出抽象。使用上下文精化方法，作者证明了具体实现和抽象之间的等效性。相比之下，我们使用更直接的方法，通过 SP 演算对给定系统调用中的每个表达式的效果进行推理，以导出一阶逻辑中的公式。

Batista Ribeiro 等人使用形式化建模工具 UPPAAL 来正式验证可作为验证组合应用程序基础的操作系统模型。作者将 UPPAAL 模型分为三层：应用程序、内核接口和操作系统模型。作者还引入了抽象任务的概念，以涵盖所有可能的任务行为，并确保操作系统模型针对所有可能的场景进行了验证。

一个局限性在于操作系统模型不能保证实现的正确性，必须验证从操作系统模型到 C 代码的完整路径。我们通过使用 SP 演算证明具体实现与我们在数学模型中使用的抽象之间的等效性，克服了这一局限性。

形式化推理技术，如谓词转换器（例如 SP 演算）也使用。该论文提出了一种名为 Strongarm 的新技术，该技术使用符号执行和谓词转换器来推断 API 方法的简洁后置条件。该技术应用于流行的 Java 库，以推断比使用传统 SP 演算导出的规范更小的简洁规范。

我们的方法使用传统的 SP 演算，但没有将导出的规范简化为更简洁的形式。这促使我们研究类似的技术，这些技术可能有助于在不丢失实现语义的情况下获得更简洁的实现抽象。

IronFleet 框架使用 Dafny 证明了机械验证实际分布式系统实现与简单的集中式规范相匹配的可行性。IronFleet 是第一个机械验证实际分布式协议和实现的活性属性的系统。它包括三个主要组件：Dafny（一种具有验证意识的编程语言）、IronRSL（一种用于分布式系统的高级规范语言）和 IronFleet 工具（一套用于管理和验证系统规范的实用程序）。这个全面的框架能够提供严格的正确性保证，提高分布式系统的可靠性。

尽管 IronFleet 框架提供了严格的正确性保证，但正确性并不是绝对的，而是依赖于几个假设。此外，即使使用自动化工具，验证也需要大量的开发工作。此外，该框架侧重于验证用验证友好的语言新编写的代码，而不是验证现有代码。

我们展示了如何将我们的方法应用于现有代码。此外，开发工作最少，因为给定系统调用的 SP 可以非常快速和高效地制定。尽管我们尚未实现自动 SP 生成器，但我们在这方面取得了很大进展。此外，我们所做的假设并不严格，而是反映了真实的系统。例如，我们关于系统调用是原子的假设也体现在 AutoCoreOS 中，该系统在进入系统调用时禁用中断，并在退出时重新启用中断。

我们借鉴了几个想法。Leino 指定了一个票务系统，并使用 Dafny 验证了活性和互斥性。然而，该规范并不是具体实现的表示。票务系统被指定为状态机。Leino 使用抽象过程，并还指定了各种可以表示实际实现的 “API”。实际上，简单的票务系统可能不足以用于复杂的操作系统，如 EB tresos AutoCore OS。

我们使用该方法将 AUTOSAR 中的任务调度和共享资源管理指定为状态机。然而，我们参考具体的实现，并验证该实现是否符合规范。使用不变性引理的想法是我们方法的主要动机。

Matias 等人使用 Dafny 来指定和验证 FreeRTOS 的实现。该规范是基于 FreeRTOS API 文档和现有的 Z 模型创建的，该实现是现有 FreeRTOS 代码库中的代码和仅根据 Dafny 规范构建的代码的混合体。Dafny 代码捕获了数据结构、算法和调度程序操作，并记录了所需的行为和约束。然而，没有讨论系统不变量以及所实现的 API 符合系统不变量的证明。

在本文中，我们提出了一种分析 AUTOSAR 规范并表明操作系统的给定实现符合这些规范的方法。我们对 SWS_OS 的分析产生了一阶逻辑公式形式的规范。这些公式表示独立于实现的系统不变量。尽管我们是根据对 SWS_OS 的理解手动导出这些公式的，但 Dafny 定理证明器自动证明了特征引理，表明我们对规范的解释是正确的。

我们使用 SP 演算导出实现的抽象。这种抽象是另一个一阶逻辑公式，其中每个合取项表示所考虑的 API 的每个语句的最强后置条件。因此，该抽象与实现等效。

我们不考虑导致错误状态的实现部分，因为达到这种状态意味着系统不变量已经被违反。我们的重点是避免错误状态的控制流。然而，仅避免错误状态并不足以保证系统不变量得到满足。相反，对于未达到错误状态的控制流，我们使用不变性引理证明实现满足系统不变量。

在提供的工件中，我们还为每个引理添加了一个 “错误” 引理。错误引理试图证明我们对规范的形式化的错误结论。例如，在清单 6 中的不变性引理中，如果 validSM 及其否定都成立，则形式化将是错误的。如果出现这种情况，则要么我们对规范的形式化和 / 或对实现的抽象是不正确的。这使我们能够自信地得出结论，我们的抽象和形式化方法是正确的。

我们提出的方法侧重于符合 AUTOSAR 标准的实时操作系统。然而，形式化推理方法可以扩展到其他标准，如 POSIX。SP 演算独立于底层实时操作系统，我们可以以本文中介绍的相同方式对符合 POSIX 标准的实时操作系统的给定 API 的语句效果进行推理。差异可能源于其他标准的不同功能（或非功能）需求。

我们方法中一个重要的缺失环节是自动生成最强后置条件。由于我们必须分析的代码库相对较小，因此这不是一个问题。然而，AutoCoreOS 有许多直接或间接涉及 SWS_OS 的许多功能需求的 API。手动分析和导出每个 API 的抽象将是难以处理的。因此，需要一种自动生成最强后置条件的方法。在这方面，我们正在开发一种使用 Z3 和 Python 编写的最强后置条件生成器。该生成器将能够使用 SP 演算为复杂的代码构造（如循环、条件、函数调用等）生成最强后置条件。

我们也没有考虑操作系统的硬件级方面。例如，AutoCoreOS 具有复杂的上下文切换机制，其中 outgoing 任务的上下文寄存器被保存，incoming 任务的上下文寄存器被加载。根据硬件平台，上下文切换机制可能会有所不同。因此，我们在 Dafny 中将任务的上下文抽象为抽象数据类型。这使我们能够使用任务上下文的简单比较和更新，而无需硬件级细节。然而，硬件级形式化规范和验证超出了本文的范围。
我们还旨在识别和形式化与 AutoCoreOS 的安全性和一致性相关的更多功能需求，例如在多核设置中。正在进行的工作旨在用多核设置中的重要功能需求扩展本文。这将需要形式化多核系统的重要方面，如核间共享资源管理，并表明相关 API 满足这些需求。