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

1244 软件学报 2026 年第 37 卷第 3 期

一个重要概念是精化: 对于任意的程序, 如果它是契约 A 的实现蕴含着它也是契约 B 的实现, 那么契约 A 是契约
B 的精化. Meyer 又将基于契约的设计推广到面向对象领域. 如 Eiffel 语言 [59] 定义了类的契约.
基于契约的设计后来被推广到反应式系统和信息物理融合系统. 反应式系统 (reactive system) 是指需要连续
地与环境交互的系统, 而信息物理融合系统是集连续演化、离散控制、通信、并行等一体的混合系统. Abadi 等
人 [61,62] 首次提出了反应式系统的假设/保证 (assume/guarantee) 规约, 基于博弈论来定义组件和环境的行为, 并定义
规约之间的精化、规约的并行组合和相容性. 假设 (assumption) 表示对环境行为的假设, 保证 (guarantee) 表示在
这个环境假设下, 系统本身能够保证的行为, 它们都定义为性质. 最典型的性质表示形式是执行迹的集合, 每个迹
表示状态序列或事件序列. de Alfaro 等人 [63] 提出接口自动机 (interface automata), 并利用接口自动机描述系统构件
接口与环境之间的契约关系. 接口模型被扩展以处理更加复杂的行为, 例如实时、资源等问题 [64,65] . 接口输入输出
自动机 [66] 与接口自动机不同, 它将环境的假设和系统的保证分别定义为两个不同的自动机.
除了安全性, 系统还有对于实时、资源约束等方面的需求. 文献 [67] 提出了多视点模型的数学基础. 针对实
时性质, 文献 [68,69] 提出了实时接口, 定义了实时接口的相容性、精化, 以及并行组合、合取、商等组合方式, 在
此基础上实现了工具 ECDAR [70] . 模态规约的实时扩展在文献 [71] 中给出. 文献 [72] 扩展了实时接口契约, 能够描
述周期性、任务完成时间以及与任务调度有关的假设/保证性质, 一些相关的工作参见文献 [73]. 文献 [74] 介绍了
[75]
实时调度规约, 接口可以定义时间、资源、调度策略等多方面的需求, 实现了分析工具 CARTS , 并应用在 ARINC
分区调度中 [76] . 另外, 还有一些专门针对资源约束的接口契约方面的工作 [77] . 假设/保证契约设计还被推广到概率
和随机系统中, 能够处理定量概率性质的描述和验证 [78−80] . 基于契约的设计方法需要从已有软件资产中提取契约,
并在契约上进行复杂的操作和推理, 在理论上仍是一个挑战, 因而无法在实践中应用到大规模嵌入式软件.
另一方面, 在电子电路设计领域, 硬件 IP 对芯片中常用的功能模块进行封装, 具有高度的可复用性、可组合
性和可验证性, 提升了芯片设计的效率. 为方便设计者使用, 硬件 IP 的生产者需要提供详细的使用文档. 为了促
进 IP 产业的发展, SPIRIT Consortium 出台了 IP-XACT 标准 [11] . IP-XACT 使用 XML 格式的语言来定义和描述 IP
的规约以及 IP 之间相互连接的细节, 给出了通用的设计表示, 可以在 IP 设计的不同流程内部进行交换. 硬件 IP
的设计理念与成功经验为嵌入式软件描述与建模提供了参考. 此外, 知识工程领域提出了知件的概念. 知件是独立
的、计算机可操作的、商品化的、有完备文档的、可被某一类软件调用的知识模块 [81] . 知件工程的愿景是形成
与软件和硬件并列的第 3 大产业 [82] . 与知件不同, 本文提出的软件 IP 是一个软件知识实体, 其本质是一种软件模
块, 支持嵌入式软件的智能合成.
2 嵌入式软件 IP 通用模型设计思路

本文的主要贡献是提出面向嵌入式系统的软件 IP 通用模型, 在介绍具体的模型之前, 本节就该模型的设计思
路予以介绍.
2.1 软件功能模块通用模型
一个软件功能模块都可以抽象成一个输入输出模型, 如图 1 所示. 功能模块的一次执行包含顺序的 3 个步骤:
输入、计算、输出. 从输入端获取计算需要的资源, 然后执行计算, 最后将计算结果从输出端输出. 对模型的输入
和输出进行不同的解释, 会得到不同的软件模型.
如果将图 1 中的输入端解释为请求接口, 输出端解释为提供接口, 那么会得到软件构件模型, 如图 2 所示. 软
件构件是软件系统中具有相对独立功能、可以明确辨识、接口由契约指定、和语境有明显依赖关系、可独立部
署的可组装软件实体 [83] . 构件的请求接口描述了为实现构件的功能所需要的外部服务, 提供接口以 API 的形式向
外部环境提供构件的至少一个功能 (服务).
如果将图 1 中的输入和输出解释为数据和事件端口, 那么会得到数据流/事件流模型, 如图 3 所示. 模型驱动
开发 (MDD) 通常采用这种数据流/事件流模型. MDD 方法一般分为 3 个阶段: 首先是建模, 根据系统设计需求从
模型库中选择合适的数据流/事件流模块完成组装; 其次是分析, 通过仿真、测试、形式验证等方法确认组装的模
型是否满足需求; 最后是代码生成, 利用模型转换技术, 将抽象的模型逐步精化为可执行代码.