Page 8 - 《软件学报》2025年第4期

1414 软件学报 2025 年第 36 卷第 4 期

case evaluations. This method thus provides a practical solution for verifying the requirements of complex embedded systems.
Key words: complex embedded system; requirements consistency; compositional verification
众所周知, 软件系统成功开发的先决条件是高质量的需求文档 [1] . 一致性验证就是一种确保需求文档高质量
的技术. 它也是解决 Zowghi 等人 [2] 提出的需求的完整性和正确性的关键. 因此, 需求的一致性验证是软件开发中
非常重要的一步 [3] . 目前, 很多形式化方法被广泛用于需求的一致性验证 [3−12] , 各种各样的形式化验证语言和工具,
[5]
比如, Z3 [13] 、UPPAAL [14] 、Rodin , 已经被应用于需求形式化验证中. 形式化方法在需求验证领域已经展示出它
们强大的能力 [15] . 特别是在安全攸关系统中, 这些方法的应用已经取得了显著的验证效果.
近些年来, 嵌入式系统规模和复杂度呈现出持续增长的趋势 [16] . 这一现象给需求一致性验证带来了新的挑战,
即验证状态空间巨大, 出现状态空间爆炸的问题, 使得一致性验证迎来的挑战. 特别地, 在嵌入式系统中, 其软件就
是要控制各种各样的物理设备, 以满足用户的需求, 其软件需求描述中涉及大量与物理设备的接口, 由于这些设备
存在严格的物理约束, 如控制信号之间的先后顺序关系, 这就要求在需求的一致性验证中必须考虑这些物理约束.
这将使得验证的状态空间进一步扩大, 加剧了验证的复杂度.
鉴于复杂的需求常常被分解为多个子需求, 一种可能实用的降低验证系统状态空间的方法就是使用 Clarke
的组合验证中验证子系统的有效构建提供了依据.
等人提出的组合验证 [11] . 通过将大型系统的验证分解为其子系统的验证, 组合验证可以在需求阶段处理更大规模
的形式验证, 检测潜在的错误, 从而防止在后期阶段进行昂贵的修改. 我们前期提出了对需求先分解再进行组合验
证的方法 [17,18] . 它针对轨道交通的区域控制器的安全需求采用了问题框架 [19,20] 建模, 并基于投影进行了安全需求
分解, 最后再根据子安全需求生成了待验证性质及验证子系统. 这些工作通过需求分解降低了验证模型的复杂度,
减少了验证空间, 缓解了需求验证中状态空间爆炸的问题. 然而, 它们主要是对需求可满足性的验证.
在前期工作的基础上, 本文提出对复杂嵌入式系统进行需求一致性的组合验证, 面临的主要问题是如何有效
地构建验证子系统. 理论上来说, 每个验证子系统都应该可以独立运行, 都应该对应一组相关子需求, 以确保需求
整体的一致性. 但是由于子需求之间可能存在设备与数据的共享, 每个子需求可能都会隐式地依赖于其他子需求.
因此, 在进行验证子系统构建时, 相关需求组必须考虑到每个子需求及其依赖的需求. 另外, 针对嵌入式系统的特
征, 每个验证子系统都必须包含软件构件与设备构件, 以保证设备的物理约束得到满足.
为了解决上述问题, 我们提出了一种复杂嵌入式系统需求一致性的组合验证方法. 它基于需求分解, 识别需求
间的依赖关系, 通过这些依赖关系组装验证子系统, 利用现有的一致性验证方法实现对复杂嵌入式系统需求的组
合验证, 并能初步定位到不一致的需求. 特别地, 为了保证每个验证子系统中物理设备的特性的不变性, 我们预定
义了其行为模型, 将其做成构件, 并通过不同的构件组装所有的验证子系统. 具体而言, 我们采用问题框架方法中
的问题图以及前期提出的情景图 [21] 对需求进行建模和分解, 并预设领域设备知识库对设备的物理特性进行建模.
其中, 由于物理设备的因果性及时间敏感性, 我们采用时间自动机 [14] 对其进行行为建模与验证. 在验证子系统的
组装过程中, 根据需求生成预期软件的行为模型, 并结合物理设备的模型进行构件级的动态组装. 这种组合方法有
效地约减了每个验证子系统的验证状态空间, 并能定位到不一致性.
本文的主要贡献包括: 提出了复杂嵌入式系统需求一致性的组合验证方法框架. 首先进行子需求依赖关系的
识别, 并根据依赖关系和预设的知识库动态组装验证子系统, 能够有效约减需求一致性验证系统中的状态空间, 从
而使原本无法进行验证的复杂需求也能够进行有效验证. 根据嵌入式系统子需求间的设备和数据共享情况, 我们
提出了一种基于模型的嵌入式系统需求依赖关系识别方法. 这种方法可以有效地识别相关需求组, 为需求一致性

本文第 1 节对相关工作进行比较. 第 2 节介绍预备知识. 第 3 节给出方法框架与设备知识库. 第 4 节描述方法
细节. 第 5 节以航天领域机载侦查系统为例进行案例研究, 对本文方法进行评估和讨论. 最后, 第 6 节总结全文并
展望未来工作.

1 相关工作

目前有很多关于嵌入式系统需求一致性验证的工作, 它们使用各种形式的需求描述语言进行需求建模, 再将