一句话总结

本文提出了一种面向容错电动汽车架构的形式化模型与部署计算方案，该方案计算混合关键性软件组件到执行节点的有效放置与重新部署，隔离故障硬件以维持故障运行行为，并在执行资源减少时形式化分析功能可用性。

核心贡献

• 提出了一种面向电动汽车的容错软硬件架构形式化模型，明确表征了混合关键性软件组件及其故障运行安全需求。
• 提出了一种基于约束的方法，用于计算有效的初始部署与故障驱动的重新部署方案；当执行节点隔离导致执行资源减少时，该方法会自动停用低优先级组件。
• 建立了一种形式化的设计时分析框架，用于量化系统降级程度并确定硬件故障后保持运行的确切功能子集，并通过汽车领域案例研究验证了其适用性。

引言

现代汽车系统日益依赖软件来提供安全关键功能，这些功能即使在发生随机硬件故障时也必须维持故障运行行为。传统汽车架构难以满足此要求，因为专用的电子控制单元和僵化的通信总线阻碍了系统级重构，而现有的容错方法通常假设静默故障模型、固定硬件配置或有限的冗余复制，且未解决混合关键性约束问题。作者利用形式化系统模型与基于SMT的约束求解技术，实现了混合关键性软件组件在执行节点间部署与重新部署的自动化。该方法通过软件冗余分配确保故障运行功能，并在硬件节点故障时自动降级低优先级功能，使设计人员能够在设计阶段形式化验证系统降级与功能可用性。

方法

作者采用了一种专为汽车软硬件集成设计的模块化、可扩展系统架构，该架构以冗余且容错执行框架为核心。整个系统由中央平台计算机（CPC）与一组负责物理传感与驱动的周边智能聚合体组成。CPC 聚合了多个被称为双工控制计算机（DCC）的中心执行节点。DCC 之间通过冗余交换式以太网链路互联，构成强健的通信骨干网。智能聚合体包含集成机电系统（如具备转向、制动和阻尼功能的轮毂电机），并直接与 DCC 连接。该架构实现了简化的硬件与网络结构，具备可扩展的执行节点集，并支持基于以太网等工业标准的统一通信系统。系统设计支持运行时环境（RTE），能够并行执行安全关键与非安全关键软件，确保购车后新软件与传感器即插即用的能力。

部署模型围绕车辆系统的形式化定义构建，涵盖功能特性、应用软件架构、执行硬件架构与配置信息。应用软件架构由应用软件组件（ASWC）组成，这些组件被划分为 ASWC 集群，每个集群包含具有相同汽车安全完整性等级（ASIL）与故障运行需求的 ASWC。执行硬件架构由中心执行节点（DCC）与周边智能聚合体节点构成。配置信息定义了 ASWC 集群如何部署至执行节点，分为主动部署（执行中）与被动部署（驻留内存）。该部署方案通过聚焦集群而非单个 ASWC 来降低复杂度，因为共享数据传输延迟等需求的集群表现出更强的绑定关系。

部署过程受一组约束条件支配，以确保配置的有效性，包括时间预算限制、用于冗余的电源多样性以及故障运行需求。每个 ASWC 由最坏情况执行时间（WCET）、ASIL、故障运行等级与最小容错时间（minFTT）等属性定义。车辆的故障恢复时间（FRT）决定了从节点部署为热备或冷备，其依据是 minFTT 与 FRT 的比较结果。部署计算被建模为算术模型，可使用 Z3 等 SMT 求解器进行求解。该模型确保满足所有约束条件，例如不超出时间预算，以及主从实例正确分配至不同电源。

发生节点隔离时，系统会重新配置部署以维持功能运行。平台可用性图（PAG）用于建模存活中心执行节点状态之间的转换。转换后部署的有效性通过算术约束来保证，这些约束维持 ASWC 到集群的映射关系，并防止对先前分配进行不必要的更改。每个 ASWC 集群具有指示热备从节点需求与存在情况，以及主节点存在情况的属性。ASWC 集群的停用顺序通过最大化活跃实例的优先级总和来确定，优先级最低的集群将首先被停用。优先级由集群的 ASIL 与故障运行等级推导得出。这确保了在资源受限时，关键功能得以保留，而非关键功能则被牺牲。