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

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

们之间的交互关系, 将混合模型转换到一个统一的中间语言进行分析与代码生成. 以上基于模型的嵌入式系统开发
环境对系统行为进行建模和仿真分析, 然而它们存在的共同问题是缺乏严格的形式语义, 难以支持形式验证.
[3]
支持形式验证的模型设计方法已有一些研究. SCADE 是一个高安全性的嵌入式软件开发环境, 集成了嵌入
式系统建模、仿真、形式验证, 代码生成等功能. 它的核心语言是同步数据流语言 LUSTRE [25] , 具有严格的语义.
然而, 它对系统构件和封装的支持较弱. Event-B [26] 是一个基于事件的系统建模和分析方法, 它支持系统各抽象层
次的建模并通过逐步精化和严格的数学证明来保证不同层次行为的一致性. Event-B 被扩展到混成系统 [27,28] , 能够
处理连续物理环境和离散控制系统的建模和分析. 欧洲 COMPASS 项目致力于建立成体系系统 (systems of
systems) 的集成建模框架, 提出的建模语言 CML [29] 集成了 Z 方法 [30] 、CSP [31] 和 VDM [32] , 定义了基于程序统一理
论 UTP [33] 的语义, 并且支持与 SysML [34] 的无缝集成来描述软硬件体系结构. 欧洲 CESAR 项目提出的 Polychrony [35]
是一个异构的嵌入式与实时系统开发框架, 它的核心语言是 Signal [36] , 能够描述硬件特性, 支持多时钟以及同步/异
步通信, 通过精化技术逐步对系统加以实现. CML 和 Polychrony 主要处理离散系统. Zélus [37−39] 以同步数据流语言
LUSTRE 为基础进行扩展, 支持连续行为的刻画, 实现了一个较强的类型系统, 能够静态地检查出部分错误行为.
上面所提到的基于模型的形式框架基本停留在软件模型的形式化层次上, 对于可复用软件构件的支持 (包括界面
封装、组合等) 没有进行深入的研究.
1.2 基于构件的开发
基于构件的设计方法 (CBD) 的基本特点是抽象掉软件模块实现细节, 提供其接口及规约, 封装成可复用的构
件, 并提供构件组合操作, 从而有效构造复杂系统并提高系统开发效率. CBD 方法支持构件的替换, 保证系统正确
[9]
性. 工业界主流的 CBD 技术包括 J2EE/EJB 、CORBA/CCM 和 [8] COM/DCOM 等. J2EE/EJB 采用基于软件构件
[7]
模型的分布对象计算体系, 可以显著简化复杂的企业级开发. 所有开发者必须遵循构件的开放规范, 从而实现构件
的兼容性和可移植性等. CORBA 是一种跨越网络、操作系统和机器实现分布对象之间互操作的工业标准, CORBA/
CCM 是用于开发和部署 CORBA 应用程序的服务器端构件规范. COM 是微软提出的基于构件的开发技术, 在此
基础上继续推出了 DCOM, 使基于构件的网络应用的开发成为可能. 此外, 针对航天飞行器软件, NASA 的 JPL 喷
气推进实验室提出了 F Prime 开源框架 [40] , 该框架将构件分为 3 类: 主动构件、被动构件和队列构件, 这些构件的
对外接口分为指令、时间、事件、参数、遥测等 [41] . F prime 提供了一种面向航天飞行软件体系结构方法, 该方法
可以生成代码框架 [42] , 加快飞行控制程序的开发过程. 但是以上这些技术对构件没有进行形式化描述.
学术界已有一些基于构件的形式设计框架. Reo 是一种抽象行为类型的构件形式模型 [43] , 其中构件行为被定
义为在构件端口上输入数据流和输出数据流之间的关系. BIP 是实时系统的构件模型 [44] , 通过行为层、交互层和
优先级层来描述构件的行为和它们之间的交互关系. 最近, BIP 的扩展能够描述动态构件和带参构件的行为 [45−48] .
rCOS 是一个构件和对象系统的统一语义模型 [49−53] , 其将构件定义为 4 个部分: 接口、契约、实现和发行, 并定义
了一组构件组合操作以及构件间的黏合代码, 从而可以将若干已知构件黏合成一个复杂构件. 然而, 以上的构件框
架主要关注功能性, 缺少对于实时、资源、连续行为等方面的支持. 这方面的工作目前比较少并且不够深入. 文
献 [54,55] 将 Simulink 转换到微分动态逻辑然后进行分析验证, 然而该方法没有考虑转换的正确性. CyPhyML 是
一种基于构件的信息物理融合系统的组合和交互语言, 使用 FORMULA 约束逻辑来描述包括连续行为在内的构
件行为以及不同构件间的约束关系和一致性 [56] . 文献 [57] 实现了一个信息物理融合系统的模型和工具集成平台
OpenMETA, 结合了模型驱动的设计和基于构件的设计, 允许将不同的构件组装在一起, 基于 FORMULA 定义不
同部件之间的语义一致性, 并且在工具集成阶段, 支持包括混成系统在内的多种模型和对应的验证算法.
1.3 基于契约的设计
基于契约的设计 (design by contract) 方法能够独立地描述各个系统构件的责任以及对构件所在环境的假设,
检查构件之间组装时是否相容、一致, 从而保证组装后系统的正确性, 并支持构件替换. 基于契约的设计思想最早
由 Meyer 在软件工程领域提出 [58,59] , 这个思想起源于 Floyd-Hoare 逻辑 [60] . 给定程序 M, 它的 Hoare 三元组表示为
{p}M{q}, 其中 p 表示输入满足的性质, q 表示 M 执行后输出满足的性质. 从而, 将 (p, q) 定义为 M 的契约. 契约的