芝能智芯出品
随着汽车智能化和自动驾驶技术的快速演进，失效运行（Fail-Operational）架构已成为实现L4/L5级自动驾驶的核心技术挑战。
基于TTTech Auto提出的系统性分析方法，深入探讨失效运行架构的设计逻辑、安全目标分解及验证流程，研究发现该架构通过冗余与多样性设计、安全决策逻辑以及形式化验证技术，实现了从传统失效安全（Fail-Safe）到失效运行的跨越。
系统性分析方法在硬件/软件失效概率评估、单点故障识别及依赖失效分析中的应用，并结合形式验证工具SAL的实践案例，为自动驾驶系统的安全设计提供了可量化、可验证的工程路径，对芯片级安全架构设计具有重要参考价值。
Part 1
失效运行架构的技术挑战
与系统性分析框架
传统L2级辅助驾驶系统采用“失效静默”（Fail-Silent）策略，即在检测到故障时直接退出并依赖人类驾驶员接管。然而，L4/L5级自动驾驶系统要求在故障发生后仍能维持安全操作，例如自主靠边停车。
● 这一失效运行能力对系统架构提出了多重挑战：
◎ 首先是冗余设计的复杂性，需要在传感器、计算单元和执行器等关键路径上实现多重冗余；
◎ 其次是故障检测与决策的实时性，要求系统在微秒级时间内完成故障诊断并切换至安全策略；
◎ 最后是系统性验证的完备性，传统FMEA（失效模式与效应分析）难以全面覆盖复杂系统的潜在失效组合。
● 为应对这些挑战，三层计算通道的参考架构：主自动驾驶通道负责正常工况下的轨迹规划，安全监控通道实时验证主通道输出的安全性（如避免碰撞），而热备冗余通道则在主通道失效时提供最小风险机动（MRM）轨迹。
◎ 以ISO 26262标准为基准，结合形式化验证技术，构建了一个覆盖“安全目标定义→架构合规性审查→量化分析→验证→改进”的闭环流程。将系统级安全目标（如避免碰撞）分解为正确性目标（ASIL D）和可用性目标（ASIL B/D），并通过马尔可夫模型量化各子系统的失效概率；
◎ 接着基于“无单点故障”原则审查架构合规性，要求主通道与冗余通道采用不同传感器模态（如摄像头+激光雷达+毫米波雷达）和异构计算平台（如不同厂商的SoC）；
◎ 随后通过量化失效分析评估硬件失效概率（基于FIT指标和组件可靠性数据）、软件复杂度（通过代码行数和圈复杂度等指标）以及依赖失效（识别共因失效并通过隔离措施提升独立性）；
◎ 最后采用SAL模型检查器进行形式化验证，将系统架构、故障模式及安全属性编码为数学模型，通过穷举状态空间验证设计的完备性，并根据验证结果迭代优化架构设计，例如增加冗余层级或引入动态重构机制。
Part 2
形式化验证
在失效运行架构中的关键作用
● 传统基于测试用例的验证方法在复杂自动驾驶系统中存在显著局限性：状态空间爆炸使得穷举测试不可行（系统状态组合数可达10^100量级），未知边界条件难以覆盖所有极端场景（如传感器遮挡或算法误判），且FMEA等人为分析方法易受主观影响而遗漏潜在失效路径。
为此，TTTech Auto引入SAL（Symbolic Analysis Laboratory）模型检查器，实现了形式化验证的工程化应用。
该工具通过状态机描述语言将系统架构、故障注入逻辑及安全属性（如“任何时刻至少有一个通道输出安全轨迹”）编码为数学公式，利用符号执行技术遍历所有可能状态转移并自动生成反例以揭示设计漏洞，同时还能验证逻辑模块到物理硬件映射是否引入共因失效。
例如，当安全监控模块与冗余通道部署在同一SoC分区时，SAL可检测因资源竞争导致的故障传播风险。
以安全监控模块的验证为例，SAL分析发现，当主通道输出正常轨迹而冗余通道因传感器故障生成错误轨迹时，监控模块可能错误地将主通道轨迹标记为“不安全”，同时将错误轨迹标记为“安全”，导致系统切换至危险状态。
为解决这一缺陷，设计通过增加监控算法的多样性（如引入独立的路径规划验证模块）消除了误判风险。这一案例充分展示了形式化验证在提升系统可靠性和安全性方面的独特优势。
● 系统性分析方法为芯片设计提供了重要启示，芯片需支持异构冗余架构，
◎ 例如多处理器核、独立内存域及安全岛（如ARM的TrustZone）以实现功能隔离；
◎ 其次，应集成硬件级错误检测机制（如奇偶校验、EDAC）以缩短故障响应时间；
◎ 此外，将SAL等形式化验证工具嵌入芯片设计流程，可实现从RTL级到系统级的全链条验证。
● 展望未来，失效运行架构的技术演进方向包括：通过软件定义架构（SDA）实现故障时的动态资源重组，利用对抗训练提升AI算法的鲁棒性，以及探索量子计算在状态空间遍历中的应用潜力。
小结
系统性分析方法通过硬件/软件冗余设计、量化失效分析及形式化验证的深度融合，为自动驾驶失效运行架构提供了切实可行的工程方案，满足ISO 26262对ASIL D级系统的严苛要求，还通过SAL工具实现了复杂系统的“数学级”安全证明。
