基于模型的航天器软件系统建模与验证

案例描述

面向航天器软件系统高可靠、强约束和多接口耦合的研制特点，项目以模型为主线组织需求分析、架构设计、详细设计、实现验证和结果归档，形成了贯穿开发周期的模型驱动研发路径。项目将需求获取、模型构建、性质验证、代码生成和运行确认纳入统一过程管理，使需求、设计与实现之间形成可追踪、可校核、可回溯的对应关系。

项目采用分层建模方法推进软件研制。需求阶段使用SysML建立需求模型，并配套状态机图、活动图和序列图描述系统功能、运行场景与交互关系；设计阶段采用AADL建立系统架构与行为模型，对软件构件划分、接口连接关系和运行逻辑进行形式化表达；详细设计与实现阶段使用SCADE建立可执行模型，在验证通过后生成目标代码。不同层级模型分工明确，既减少了自然语言需求表述的歧义，也避免了架构设计与详细实现之间的语义脱节。

在建模基础上，项目把形式化验证前置到需求阶段、设计阶段和详细设计阶段。需求模型与AADL模型转换为时间自动机模型后，结合CTL语义规约开展模型检查；SCADE模型则通过形式化模型和验证引擎进行性质验证。围绕空间包发送、传输层模块交互和包路由查询等关键业务，项目验证错误处理、状态迁移和异常约束，并在此基础上开展FMEA、FTA等安全分析，使功能正确性与安全性要求在同一技术路径下落实。

案例实施的具体内容

• 1. 需求分析与需求建模

项目首先对客户提供文件、用户需求和使用场景进行归并整理，形成系统需求基线和系统用例集合。需求梳理围绕航天器软件在业务执行链路中的职责边界展开，识别功能触发条件、输入输出约束、异常处理要求以及跨模块交互关系。针对遥测业务、空间包发送等关键场景，项目将需求分解到可建模、可验证、可落地的粒度，并利用SysML建立需求模型、状态机图、活动图和序列图，使需求从文本描述转化为可分析的逻辑模型。

• 2. 架构设计、详细建模与验证

在需求模型收敛后，项目进入架构设计阶段。AADL架构与行为模型用于表达软件构件划分、接口方向、数据交换关系和关键行为约束，使需求层功能能够落实到具体构件和交互机制上。围绕空间包发送等功能，模型明确构件实例、接口连接、执行条件和状态迁移关系，并通过时间自动机转换与CTL规约，对接口有效性、状态可达性和异常路径约束进行检查。随后，项目采用SCADE建立可执行详细模型，重点覆盖空间包构件初始化、包路由查询等功能，结合形式化验证工具对输入条件、边界约束和错误处理逻辑进行校核，对“路由项目数超限时返回ERR_SP_INVALID_LENGTH错误码”等具体约束进行直接验证。通过验证的SCADE模型自动生成代码，保持模型、验证结果和实现代码的一致性。

• 3. 过程数据管理与安全分析

项目建立了面向全周期的过程数据管理方式，将系统需求基线、用例、需求模型、行为模型、详细模型、验证结果及代码成果统一归档关联，以构建从原始需求到最终代码的证据链。不同建模语言之间的信息传递也由此保持连续：SysML模型提供需求边界和场景约束，AADL模型承担架构分解与接口组织，SCADE模型承接详细逻辑并形成可执行实现。

在功能建模与性质验证基础上，项目进一步将系统模型用于安全分析。围绕综合电子系统遥测功能中的核心需求，模型既描述正常业务行为，也承载故障失效条件下的系统响应关系。依托统一模型语义基础，项目开展 FMEA 和 FTA 分析，并将安全分析结论反向作用于需求约束、架构设计和详细逻辑校核，形成“功能建模—性质验证—安全分析—设计修正”的闭环。

案例亮点

项目的突出特点在于采用分层建模和分阶段验证相结合的组织方式。SysML用于需求与场景表达，AADL用于架构与行为表达，SCADE用于详细逻辑和代码生成，不同模型各自承担明确职责，保证需求、架构与实现分别在适合的表达环境中展开。与此同时，性质验证并未后置到编码完成之后，而是在需求、设计和详细设计阶段逐层展开，使逻辑冲突、接口不一致和边界条件缺失等问题能够在模型层被及时识别和修正。

另一个特点在于模型成果直接参与实现与安全分析。通过验证的SCADE模型自动生成代码，使详细设计模型成为实现活动的直接输入；FMEA和FTA又建立在同一套功能模型和行为模型之上，使风险识别能够回溯到具体功能、接口和逻辑对象。由此形成的不是彼此独立的设计、验证和安全分析活动，而是一条前后衔接、相互约束的工程链路。

实践效果及应用价值

项目形成了面向航天器软件系统的模型设计、验证与实现一体化方法，把需求建模、架构建模、详细设计建模、形式化验证、代码生成和安全分析组织到同一过程框架中，使不同阶段围绕同一组业务对象、模型成果和验证证据展开。对于需求复杂、运行约束严格、接口耦合度高的软件系统，这种方法有助于压缩阶段间的理解偏差和实现偏差。

从工程实施角度看，项目将验证活动前移到模型阶段，改变了依赖编码后测试暴露问题的工作方式。需求逻辑冲突、接口约束不一致、异常路径遗漏和边界条件处理不完整等问题，可以在模型检查和性质验证阶段被识别并修正；通过验证的详细模型再进入代码生成和后续实现，有利于保持设计意图在实现过程中的连续性。围绕空间包发送、传输层交互、包路由查询以及遥测功能安全分析形成的建模与验证链路，也为同类高可靠嵌入式软件提供了可复用的组织方法。