3. 软件架构验证
软件架构验证的核心问题不是“模型画得对不对”，而是“模型所声明的结构约束，在真实实现中是否成立”。AADL 与 SysML 分别从不同视角支撑这一判断：AADL 面向运行时架构，天然描述任务、线程、处理器、总线、分区与端到端时延；SysML 面向系统建模，擅长需求、块定义、内部块图与参数约束。综合航电的架构验证，通常以 SysML 承接需求与系统分解，以 AADL 承接可调度、可隔离、可分析的运行时视图，再通过接口一致性检查把两张视图“钉”在一起。
一、两种语言的验证视角差异
AADL 的验证视角是“资源—时间—流”。它把系统拆成软件组件（进程、线程、子程序）、执行平台组件（处理器、虚拟处理器、存储器、总线）和复合组件，并通过属性（Period、Deadline、Compute_Execution_Time、Priority、Dispatch_Protocol）把调度语义写进模型。因此 AADL 模型可以直接导出到调度分析、端到端流分析和资源预算检查工具中。SysML 的验证视角是“需求—结构—参数”。它通过需求图建立追溯，通过块定义图与内部块图描述逻辑接口，通过参数图表达约束方程，但本身不携带调度语义，时间行为需要借助 MARTE 或映射到 AADL 才能分析。
实践中的分工是：SysML 回答“系统应该由哪些功能块组成、接口承载什么数据、满足哪条需求”；AADL 回答“这些功能块映射到哪些分区和处理器、周期与优先级如何、最坏执行时间是否满足截止期”。两者不是替代关系，而是同一架构的两个可验证切面。
二、接口一致性检查：把两张视图钉在一起
接口一致性检查不是简单比对端口名，而是检查四类语义是否对齐。第一类是名称与方向：SysML 的 out 端口必须对应 AADL 的 out 数据端口，方向反转会导致数据流分析得出错误结论。第二类是数据类型与量纲：SysML 中高度用 Altitude_m（米），AADL 端口若声明为 Altitude_ft（英尺），即使名字相近也会在集成时产生 3.28 倍误差。第三类是时间语义：SysML 连接器若隐含“事件触发”，而 AADL 端口配置为 Sampling 周期采样，则高频事件会被漏采。第四类是流路径完整性：SysML IBD 中从传感器到作动器的每条流，必须在 AADL 中存在对应的端口连接链，否则该功能在运行时不可达。
可执行的检查方式是建立一张接口映射表，逐行核对。例如某综合航电的“大气数据—飞行指引”链路：
| SysML 端口 | 方向 | 类型/单位 | AADL 端口 | 时间语义 | 结论 |
|---|---|---|---|---|---|
| ADC.out.altitude | out | Altitude_m | ADC_Alt : out data | Sampling 50ms | 一致 |
| ADC.out.airspeed | out | Speed_kt | ADC_Spd : out data | Sampling 50ms | 一致 |
| FG.in.altitude | in | Altitude_ft | FG_Alt : in data | Sampling 50ms | 单位不一致 |
| FG.in.valid | in | Boolean | — | 事件触发 | AADL 缺失 |
表中第三行暴露了单位不一致，第四行暴露了 AADL 模型缺少有效性标志端口。这两处若不在架构阶段修正，将在集成测试中表现为高度跳变或无效数据被当作有效值使用。
三、分区与时间隔离验证
综合航电普遍采用 ARINC 653 分区机制，验证目标是证明“分区预算之和不超过主帧周期，且每个分区内线程的最坏执行时间不超过其分区窗口”。设主帧周期为 100 ms，四个分区预算分别为 25 ms、30 ms、20 ms、15 ms，合计 90 ms，剩余 10 ms 作为系统余量，满足 Σ预算 ≤ 主帧周期。若某分区内三个线程的 WCET 分别为 6 ms、8 ms、5 ms，合计 19 ms，小于该分区 20 ms 窗口，则时间隔离成立；若合计达到 22 ms，则线程会溢出窗口，导致后续分区被挤压，必须调整线程周期或降低 WCET。
空间隔离验证则检查：分区之间不存在共享内存写操作，所有跨分区通信必须经过采样端口或队列端口；每个分区的代码段、数据段、堆栈在存储器映射中互不重叠。AADL 中通过 Actual_Memory_Binding 和分区属性表达这些约束，验证工具可自动检查绑定冲突。
四、综合航电架构验证实战
以一个简化的综合航电场景为例：系统包含大气数据计算机（ADC）、飞行指引（FG）、显示管理（DM）和健康监控（HM）四个功能块，运行于两个处理器、四个分区。验证流程如下。
第一步，建立 SysML 逻辑视图。在 IBD 中定义 ADC 向 FG 输出高度、空速和有效性标志，FG 向 DM 输出指引指令，HM 采集各分区健康状态。为每个端口标注数据类型、单位和更新周期。
第二步，建立 AADL 运行时视图。将四个功能块映射为四个进程，每个进程绑定到一个虚拟处理器分区；ADC 与 FG 的线程周期设为 50 ms，DM 设为 100 ms，HM 设为 200 ms；通过端口连接表达 ADC→FG→DM 的数据流。
第三步，执行接口一致性检查。按前述四类语义逐项核对，修正 FG 的高度单位与 ADC 一致，补齐有效性标志端口，确认所有采样周期匹配。
第四步，执行分区与时间隔离分析。计算分区预算总和、各分区线程 WCET 总和、端到端时延。示例结果：ADC→FG→DM 的端到端时延为 50 ms（ADC 采样）+ 8 ms（FG 计算）+ 50 ms（DM 采样）= 108 ms，若需求要求不超过 150 ms，则满足；若要求不超过 100 ms，则需缩短 DM 采样周期或改为事件触发。
第五步，形成验证结论。将接口检查表、预算计算表、时延计算结果与需求追溯关系一并归档。任何一项不满足，都回到 SysML 或 AADL 模型修改，而不是在代码阶段打补丁。