AWS FreeRTOS 是一款实时操作系统，用于在 IoT 设备上运行，使这类设备可以与 AWS 服务轻松、可靠地进行交互。Over the Air (OTA) 更新功能可以快速、可靠地更新装有安全修补程序的设备。OTA 库是 OTA 设备上运行的完整 IoT 功能的一部分，能够让客户知悉可用的更新、下载更新、检查自己的加密签名并应用这些签名。
OTA 系统架构
下图显示的 OTA 系统端到端架构略有简化。在 AWS 端，存在一个作业服务器，可跟踪现场 IoT 设备的状态。也就是说，它会跟踪设备是否处于活动状态、运行的供应商软件版本、是否需要更新等。此外，还有文件服务器，即 AWS S3 存储桶，可用于保存要发送给设备的更新。在 IoT 设备端，存在 OTA 库，用于跟踪设备状态、处理来自作业服务器的传入请求、管理从文件服务器传输到设备的数据、应用更新以及将相关信息重新报告给 Job 服务器。OTA 应用是开发人员的应用程序代码，而 OTA PAL 是 OTA 库与特定于设备的硬件之间的接口。设备与服务器通过 MQTT 和/或 HTTP 网络进行通信。
OTA 系统是一种复杂的软件，可在设备和通信出现任何故障的情况下，可靠、安全地执行固件更新--- ，从而使所有设备保持相同状态---。OTA 系统的核心在于错综复杂的分布式协议（即 OTA 协议），该协议可协调所涉及的不同代理的执行情况。
OTA 协议验证
除了针对作业服务器或 OTA 库等个体代理的单元测试外，我们还为整个系统编写了广泛的端到端测试。与我们或多或少可通过代码了解控制流程的顺序系统不同，分布式系统为 OTA 系统提供了多个异步执行代理，例如硬件设备、网络、AWS 服务等，因此会导致出现无法预料的情况。实际上，单独代理的执行交错繁多，几乎不可能将所有情况考虑周全。
这是验证分布式系统时所面临的众所周知的问题。在 AWS，我们一直在使用形式化方法（特别是进行模型检测时）来提高分布式系统的质量水平。早在 2011 年，我们便对 AWS 的多个分布式协议进行了模型检测 [1]。
考虑到 OTA 协议是 FreeRTOS 的核心，为了获得比使用标准测试更高的代码质量，我们决定使用形式化方法来验证 OTA 协议。特别地，我们使用了模型检测来彻底探索 OTA 协议的模型，并发现了棘手的极端情况。
模型检测
形式化方法利用数学逻辑和各种搜索技术来推断程序是否正确。模型检测是该领域有名的技术，它从程序描述和正确性属性开始，彻底探索了程序的所有可能行为，直到检查每个此类行为是否满足该属性。如果出现任何违规行为，系统会向用户报告并提供导致故障的线索，从而为用户提供准确且可操作的反馈。由于已经过模型检测的系统往往质量更高且缺陷明显更少，因此硬件行业和软件行业都会使用此类系统来验证关键设计 [2][3]。
一般而言，分布式系统太大，无法直接使用模型检测进行验证。标准做法是创建一个系统模型，来捕获系统的核心行为并针对协议级别的错误分析该行为。此方法已成功应用于硬件和软件行业，用于设计复杂的分布式系统 [1][5]。---包括 Tla +、SPIN、P ---在内的几个模型检查器已被证明适用于此任务。我们已使用 P [4]。
OTA 协议建模
第一步是从实现中提取协议模型，该模型足够小，可进行形式化分析，并且足够丰富，可展示反映实际情况的行为。我们的目标是捕获详细的核心协议，并精确分析 OTA 系统中最难以测试的方面。
为此，我们保留了特定于协议的详细信息，例如代理发送的消息类型以及各种代理的协议状态机，并抽取出与核心协议无关的所有详细信息。分布式系统的详细程度可通过消息包含的详细信息数量来衡量。为了详细说明这种差异，作业服务器发送到 OTA 库的实际作业文档是采用 UTF-8 编码的 JSON ，其中包含大约 20 个字段。在我们的模型中，我们简化了作业信息，仅包含 4 个简化的字段，即作业 ID、作业状态、更新版本以及指示 http 使用情况的标志，如下所示：
enum JobStatus {
EMPTY = 0,
PENDING = 1,
INPROGRESS = 2,
SELFTEST = 3
}
type job = (
id: int,
status: JobStatus,
version: int,
http: bool
);
