oss

F Prime 为飞行软件配上类型化线束,时钟仍由任务方掌握

11 条来源 9 条一手来源 已翻译 2026年9月7号

正文
NASA 的“机智号”火星直升机停在火星的岩石地表,蒙尘的太阳能板与两组旋翼出现在“毅力号”火星车的镜头中。

2023 年 4 月 16 日,“毅力号”的 Mastcam-Z 相机从约 23 米外拍下火星上的“机智号”。这架飞行器运行 F Prime;照片标示出可复用框架与围绕它开发的任务专用应用之间的区别。摄影:NASA/JPL-Caltech/ASU/MSSS。[7][9]

人们很容易把 F Prime 误解成一套经火星任务验证的 C++ 代码,以为它能让嵌入式项目就此成为“飞行软件”。它更具分量的产物是一副带类型约束的软件线束。FPP 模型为组件、组件交互所经的端口,以及连接具体实例的拓扑命名。生成代码再把这些声明变成软件接口与部署设施。拓扑规定了谁可以调用谁;一次调用能否赶在物理系统需要结果之前结束,则要另行证明。

在 F Prime 4.3.0 中,这一区别格外清楚。2026 年 8 月发布的这个版本开始用 FPP 系统为部署建模,增加了速度更快、内存效率更高的直接端口调用选项,也扩展了被动速率组中的时序观测能力。这些改进切实增强了框架用于架构描述和测量的工具。任务采用的频率、线程优先级、队列深度、处理器、最坏情况工作负载,以及对过期传感器数据的响应,仍由具体任务决定并验证。[4]

把经常混在一起的三份契约分开,系统便更容易检查:模型契约让接口与连线可供核查;执行契约决定端口处理函数在哪里运行;时间契约把一次时钟节拍变成受调度的工作。F Prime 帮助工程师明确写下三者。组装后的系统在自身环境中是否足够安全,最终仍需任务方拿出证明。

火星履历提供参照,鉴定仍须另行完成

F Prime 也写作 F′,由 NASA 喷气推进实验室于 2013 年设计,2017 年以开源形式发布。在“机智号”之前,它已经用于 ISS-RapidScat 仪器和 ASTERIA 立方星。NASA 将它描述为面向小型航天器与仪器的多任务可复用框架,提供指令处理、遥测、参数和序列执行等通用服务。[7]

“机智号”让这段技术传承变得具体。这架小型直升机采用商用级计算硬件,在地球人员无法即时控制的情况下飞行,而任何测试舱都无法完整复现它所处的环境。[11] 任务发射前,运行负责人 Tim Canham 在一次采访中说,制导环路以 500 赫兹运行,图像特征则以 30 赫兹处理。他也谨慎划定了自主飞行的范围:地球端给出规划轨迹,机载软件负责让直升机保持在轨迹上;所需传感器数据一旦失常,机载软件可以中止飞行。[8]

这些数字属于“机智号”的任务要求,不能视作 F Prime 赋予的默认值。框架给出一套架构,让可复用服务与项目专用控制代码可以组合起来。气动模型、传感器融合节奏、Snapdragon 板卡验证,以及传感器失效后以着陆作为安全响应,均由项目自行确定。开源仓库因而证明了采用这些构件的框架已有飞行经历;任何新用户接入的系统仍需取得自己的鉴定依据。

封面照片再次划出了这条界线。镜头中的实体硬件已经在火星度过两年:太阳能板覆着尘土,旋翼暴露在大气中;这架飞行器透过并不完美的传感器与执行器采取行动,软件同时受制于功耗与时间。[9] F Prime 能让软件架构清晰可读。端口以外的物理世界仍归任务方处理。

契约一:FPP 把架构变成构建输入

F Prime 把应用拆成组件。每个组件负责一段范围明确的行为,并公开类型化端口;组件之间的访问应经过已声明的通道。拓扑创建组件实例,并连接类型相容的输出端口与输入端口。常规部署通常把这份拓扑编译进一个二进制文件;组件声明的指令、遥测通道、事件和参数则共同写入地面系统数据字典。[1][2]

FPP 全称 F Prime Prime,是编写这些声明的建模语言。它的工具链执行语义检查,并生成 C++、JSON 等目标产物。生成的组件基类包含面向框架的衔接代码,开发人员从中派生类,再实现任务行为。除了省去样板代码,模型本身也成为可审查的源文件。代码审查者能够看出传感器组件发出哪一种类型、哪些具名接收方获准接收数据,以及部署采用哪个具体实例,运行时发现对端的过程也由此省去。[3]

静态、类型化的连线消除了多类含混之处。端口类型不匹配可在生成或构建阶段报错,问题不至于留到飞行中表现为畸形数据包。接口改名或移除会造成清晰可见的集成断点。仿真部署可以替换面向硬件的组件,同时保留同一份端口契约。F Prime 对自身架构的介绍提到,“机智号”的开发过程使用了 11 个拓扑,最后汇聚成飞行部署,使共享组件能够在不同测试环境中运行。[1]

类型一致所保证的范围有意保持狭窄。两个端口可以一致约定传递的值是 32 位整数,却仍会在单位、参考系、数据新鲜度、饱和处理上各持不同约定,也会对零值究竟表示“有效读数”还是“传感器不可用”作出不同解释。拓扑可以证明指令有路可达,却无法证明接收方正处于合法运行状态。生成代码会忠实保留已声明的契约;缺失的部分仍需工程团队补全。

4.3.0 版本也说明了同一点。部署拓扑如今需要标记为 deployment,FPP system 则在模型中标识这项部署。该版本还允许生成的直接端口调用避开一部分调用开销。[4] 两项变化都把已构建系统的更多内容纳入显式工具管理。同步调用链是否够短、异步队列里的数据是否够新、直接调用是否安全,仍需逐项审查。要回答这些问题,审查者需要阅读第二份契约。

契约二:端口决定工作在哪里执行

“端口”听来像消息通道,但输入端口的种类同时包含一项执行决策。同步(synchronous)输入端口的行为与普通函数调用相似:处理函数立即在调用组件的线程上运行,并且可以返回数据。互斥保护型(guarded)输入端口同样采用同步方式,但进入该组件的所有此类调用共用一把互斥锁。异步(asynchronous)输入端口把调用按顺序放入接收组件的队列,无法在同一次调用中返回结果。[2]

组件补足了这项选择的另一半。被动(passive)组件既没有线程,也没有队列,工作在调用方的执行环境里运行。主动(active)组件两者兼有,并在自己的线程上分派异步工作;它的同步输入端口与互斥保护型输入端口仍然在调用者线程上运行。队列型(queued)组件有队列却没有线程,队列必须由某项同步活动有意排空,通常就是一次速率驱动调用。[2]

这套词汇让延迟由谁承担变得可供检查。把缓慢的设备操作放在同步端口之后,调用者就会继承这段延迟。加入互斥保护型端口,设计便有了互斥访问,也随之引入争用或重入死锁的风险。把工作移到异步输入端口,调用者得以继续执行,系统同时要面对队列容量、溢出策略、顺序、服务速率,以及数据从产生到使用经过多久等问题。“主动”这一标签也不会自动带来隔离,因为一个同步输入端口仍可进入另一个组件看似受保护的调度时段执行。

因此,“这些组件已经解耦了吗?”只能作为起点。审查真正需要追问的是:“这次调用在哪里执行,什么会阻塞它,信息在等待期间会发生什么?”F Prime 当前的设计指南主要把有硬截止期限的周期工作放在同步的速率驱动通路,把事件驱动工作放在异步通路,把后台工作放在优先级较低的异步通路。指南也提醒,实际设计可以偏离这些模式,同时需要说明偏离的理由。[2][10]

契约三:速率组把节拍变成义务

嵌入式软件要周期性地读取传感器、更新控制器、收集遥测并检查健康状态。F Prime 用速率组(rate group)表达这类节奏。系统提供的时钟源驱动 RateGroupDriver;配置好的分频因子产生频率较低的节拍;主动或被动速率组组件再按规定顺序调用与之相连的 Sched 端口。[5]

被动速率组在时钟调用方的执行环境中运行。它的子项依次执行,关键路径很容易描述,但某个耗时过长的处理函数会拖延后续所有工作。主动速率组以异步方式接收节拍,并唤醒自己的线程。时钟源受到的阻塞随之减少,各组则在操作系统调度下竞争处理器时间;与此同时,分派抖动进入系统,线程优先级也成为时序论证的一部分。按顺序发送调用,并不保证所有子项工作都以同样顺序完成:当某个成员的 Sched 输入端口采用异步方式时,主动子组件会在自己的队列中收到这项工作,积压甚至会延续到发起它的速率组分派结束之后。[2][5]

新周期在上一轮分派完成前到达时,主动速率组会检测到一次滑移并发出警告。这项告警本身无法显示主动子组件队列里已经积压的未完成工作。现有的被动速率组遥测可以给出整轮用时、逐端口用时和高水位值;4.3.0 又扩展了这组测量能力。[2][4][5] 这些信号能把未满足的假设变成操作人员看得见的证据,因此很有价值。它们记录的是已经发生的执行。标称台架测试中表现正常的高水位记录,距离冷态硬件、最大总线流量、满队列、错误日志与恢复动作同时出现时的最坏情况执行证明,仍有明显差距。

“机智号”公开披露的 500 赫兹制导环路让时序压力有了具体尺度:一个周期只有 2 毫秒。公开访谈没有说明该环路对应哪一个 F Prime 速率组,因此这项数据不能解读为拓扑事实。[8] 任何设计若把此类工作分配到速率组通路,F Prime 都能传递节拍,并明确显示每一条调度连线。任务方仍需在实际处理器上为完整通路编制时间预算,其中包括同步被调用方、锁、缓存效应、驱动程序、中断,以及主动组件带来的干扰。频率降低只会改变数值,验证义务保持不变。

测试拓扑保留接口,物理现实仍需另行验证

明确的连线既让飞行部署便于审查,也让替换组件变得实用。项目可以把仿真总线或仿真传感器接到飞行驱动程序使用的端口上,在工作站中测试组件逻辑,并随着硬件到位继续保留面向任务的接口。F Prime 会生成与组件各个端口一一对应的测试工具,记录输出端口、事件、遥测和指令响应的历史,并为测试给出参数值与时间值。它自己的测试指南把这类单元测试与集成系统测试分开,并要求测试能够追溯到组件需求。[6]

这是一套有力的开发循环,其中的接缝仍要清楚可见。输出类型正确的模拟传感器未必能重现总线仲裁、DMA 行为、时序抖动、电气复位,也未必能重现设备在状态位有效时返回旧样本的情形。桌面拓扑往往拥有充裕内存,其调度器也与目标 RTOS 不同。即使组件代码覆盖率很高,组合后的系统实际到达过哪些状态仍不能由此确定;F Prime 指南也明确区分了行覆盖率与状态覆盖率、路径覆盖率。[6]

“机智号”团队广泛使用仿真,随后又在真空舱测试实体原型,找出模型与飞行器之间的差异。有些条件依旧无法同时复现,其中包括火星大气与火星重力,于是团队把经过验证的部分重新组合进仿真环境,并反复施加扰动。[11] 值得借鉴的经验正在这里:可复用架构降低了建立多个如实反映特定条件的测试环境的成本,每个测试环境仍只覆盖物理现实的一部分。

引入试点真正应该证明什么

当团队需要静态组合的嵌入式系统、重视自动生成的指令与遥测设施,且运行实践足够成熟,能够自行承担时序和故障分析时,F Prime 最为合适。一项有用的试点应选取一条真实的“传感器到执行器”或“传感器到下行链路”通路,教程成功构建只能算作起点。

第一,审查者应当能够沿 FPP 拓扑追踪这条通路,并把每次跨组件调用标为同步、互斥保护型或异步。部署还应记录每个主动实例的队列深度、栈大小和优先级;如设置 CPU 亲和性,也应一并记录;同时写明工作无法入队时采用的策略。对于每条同步调用链,时间预算应涵盖在原调用者线程上运行的所有下游处理函数。

第二,团队应在目标级硬件上运行预定的速率组,覆盖标称、峰值和有意注入故障的三类输入。记录整轮及逐端口高水位值、队列占用量或溢出事件、指令延迟,以及数据从产生到使用的时长。随后刻意叠加这些棘手条件:缓慢设备与最大遥测流量同时出现,在周期工作期间下达恢复指令,以及让故障通路的日志量超过标称运行水平。

第三,告警只是起点,试点还要明确错过时限后的安全响应。速率组滑移之后,可以保持上一次输出、进入安全状态、重启一个组件、复位处理器或停止执行器;具体选择来自系统危害分析。队列已满时,也需要确定丢弃最新数据、最旧数据或不丢弃任何数据,哪一种做法符合安全要求。框架无法从软件形态推断物理后果。

最后,鉴定工作必须列出接受鉴定的确切技术栈:F Prime 版本、FPP 工具版本、生成产物、编译器及其标志、操作系统抽象层、平台软件包、板级支持、项目组件、配置和硬件。飞行履历附着于经过测试的组合及其流程,不会从公开仓库传递到另一架飞行器。

F Prime 的开源成就,其分量也正落在“这段代码飞过火星”之外。它给工程师一套共同语言,用来描述那些常常藏在 C++ 中的接缝:拓扑说明谁能通信,端口种类说明处理函数在哪里运行,速率组说明工作何时被请求。这些关系显现之后,任务方就能测量、测试并论证余下的风险。带类型约束的软件线束之所以有价值,正因为它标出了框架止步之处。

来源

  1. F Prime 项目,“强大的软件架构”——概述组件、端口、拓扑、部署、执行类型,以及“机智号”的测试拓扑。
  2. F Prime 4.3.0 用户手册,“核心构件:端口、组件与拓扑”——介绍类型化连接,以及同步、互斥保护型、异步、被动、队列型和主动等执行语义。
  3. F Prime 项目,F Prime Prime(FPP)用户指南,3.3.0 版——介绍建模目标、语义检查,以及 C++/JSON 生成。
  4. NASA F Prime 维护团队,F Prime v4.3.0 发布说明——介绍 FPP 系统建模、直接端口调用、速率组测量、配置变更和安全加固。
  5. F Prime 4.3.0 参考文档,“速率组调度功能”——介绍时钟分频、主动/被动分派、周期超时检测、配置与时序遥测。
  6. F Prime 4.3.0 用户手册,“F′ 中的单元测试”——介绍生成的组件测试工具、需求追踪、端口历史记录及行覆盖率的局限。
  7. NASA,“认识驱动 NASA‘机智号’火星直升机的开源软件”——介绍 F Prime 的起源、开源发布、飞行履历、通用服务和复用范围。
  8. Evan Ackerman,“NASA 如何设计出可在火星自主飞行的直升机”,IEEE Spectrum——有关“机智号”硬件、循环频率、规划轨迹和机载自主范围的独立采访。
  9. NASA Science,“‘机智号’在火星的两年”——Mastcam-Z 照片的日期、距离、尺寸、说明,以及 NASA/JPL-Caltech/ASU/MSSS 署名。
  10. F Prime 4.3.0 用户手册,“选择组件、端口与指令类型”——介绍周期工作、事件驱动工作和后台工作模式及其执行取舍。
  11. Evan Ackerman,“‘机智号’首席飞行员讲解如何在火星驾驶直升机”,IEEE Spectrum——介绍仿真验证、真空舱测试、无法消除的环境差距和反复扰动试验。
Previous 一份 LUT 在改变任何像素之前,就越过了 OpenColorIO 的信任边界 Next 坦克在成为图像之前,先是一个问题

Recommended In oss

Matched by subject and format