Page 294 - 《软件学报》2026年第3期

徐雄 等: 嵌入式软件 IP 通用模型 1257

形式模型和实现. 本文按照“知识模型-形式模型-实现”的顺序对软件 IP 进行介绍, 但在提取软件 IP 时, 我们从
“实现”部分开始. 针对输入的工程项目中的每个函数, 我们先提取其“实现”, 在此基础上继续提取其知识模型和形
式模型.
根据第 5 节的描述, 软件 IP 的实现由头文件 (.h) 和实现该软件 IP 功能的源代码 (.c) 组成, 其中头文件包含输
入和输出变量 (对应接口中的输入和输出端口) 以及状态和参数变量的声明. 因此, 软件 IP 实现的提取包括: (1) 声
明变量提取. 根据第 3 节中关于输入、输出、状态和参数变量的定义, 我们可以为软件工程项目中每个函数提取
这 4 种变量. 具体而言, 函数的输入变量是指函数形参和函数中使用的全局变量 (排除先写后读的变量); 函数的输
出变量是指被修改的函数形参和全局变量 (变量或其别名被修改); 函数的状态变量首先即是该函数输入变量同时
也是输出变量, 如果没有其他函数也使用了该变量, 那么该变量则是该函数的状态变量; 函数的参数变量首先是该
函数的输入变量, 如果没有别的函数以该变量为输出变量, 那么该变量则是该函数的参数变量. (2) 将每个函数转
换为软件 IP 实现: 基于第 (1) 步提取的变量以及项目的源代码生成软件 IP 实现 (头文件和源代码). 具体而言, 首
先创建头文件 (.h) 并在其中以结构体的形式声明第 (1) 步提取的 4 类变量; 其次, 将项目中的函数转换成软件 IP
实现中源代码 (.c) 的格式; 最后, 函数的头文件 (.h) 和格式化的源代码 (.c) 构成了该函数对应的软件 IP 的实现, 外
部环境可以通过引入 (#include) 软件 IP 的头文件来使用其功能.
基于提取出来的软件 IP 实现, 我们采用 LLM 的上下文学习方法, 进一步提取其知识模型. 该方法充分利用
了 LLM 在代码理解和模式识别方面的能力, 并结合少量示例, 建立了一个高效的少样本学习框架. 知识模型的提
取分为两个阶段: 提取阶段和验证阶段. 在提取阶段, 通过 API 调用 LLM, 并将温度系数设置为 0.3, 以平衡输出的
确定性和创造性. 同时, 采用约束解码方法以确保输出格式的规范性; 验证阶段包括一个 3 层验证系统: 格式验证
(使用 JSON schema 验证输出是否符合预定义的格式要求)、交叉验证 (通过抽样进行人工审查确保提取结果的准
确性) 和反向验证 (利用提取的知识模型生成软件 IP 代码片段, 并与原始代码进行比对, 验证一致性), 以确保提取
结果的准确性和可靠性. 如果验证阶段未通过, 则重新进行提取过程.
针对软件 IP 知识模型提取问题, 我们从软件 IP 的实现提取相应的契约. 然而, 目前用于契约生成的开源工
具 [97,103,104] 存在一些局限性, 例如生成效率低和自动化程度低等, 这源于它们对静态/动态分析的严重依赖以及缺乏
轻量级架构. 此外, 它们对预定义的验证目标的需求, 或仅仅专注于循环不变式生成, 导致了工具的灵活性受限. 因
此, 我们开发了一种面向软件 IP 的契约提取工具, 该工具利用 LLM 的能力, 以 ANSI C 规约语言 (ACSL) [105] 格式
为 C 程序生成形式规约 (契约), 并利用 Frama-C [106] 框架进行自动化验证.
提取出来的软件 IP 通过封装软件开发者的知识, 提供了独立于具体实现的功能模块, 这些模块可以在不同的
嵌入式系统开发项目中重复使用. 知识模型明确了软件 IP 的功能、接口、使用条件等关键信息, 使得开发者能够
快速理解并集成这些模块到新的项目中; 形式模型通过形式化方法准确描述了软件 IP 的行为和接口规约, 减少了
开发者对软件 IP 理解的偏差, 提高了复用的准确性.
8.2 案例与实验评估
本实验中从航天嵌入式领域的太搜软件 (以下简称太搜) 提取相应的软件 IP. 太搜是嵌入在卫星中的软件, 它
通过陀螺仪和太阳传感器感知太阳的位置, 并根据卫星的姿态角和位置数据, 计算控制命令, 最后通过控制推进器
来调整卫星的姿态. 太搜包含复杂的数据结构, 这对自动化提取工具构成很大的挑战, 其复杂性源于函数之间错综
复杂的相互依赖关系、对指针的广泛使用以及复杂的数据操作流程等.
本实验的测试环境配置在 Ubuntu 24.04.1 系统上, 配备了 AMD Ryzen 9 7940HX 的 CPU 和 32 GB 的 RAM.
这一配置为执行计算密集型任务提供了均衡的环境, 同时确保有足够的内存资源来处理大型数据集. 该工具主要
使用 C++和 Python 实现.
我们从太搜中提取了 49 个软件 IP. 这些软件 IP 实现部分的提取耗时近 9 s, 这表明了工具在处理具有复杂相
互依赖关系但数据结构相对可控的中等复杂嵌入式系统代码时的高效性. 关于太搜软件 IP 知识模型的提取, 我们
在 GPT-4o-0806 模型上对两种提示模板 (基本提示词 BP 和基于上下文学习的提示词 ICP) 进行评估, 结果如表 1