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

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

控制依赖可以分为 3 种情况.
情况 1. 一个需求使得另外一个需求的前置条件发生: 若需求 R 1 发生的前置条件为设备 dev 处于状态 s, 而综
合设备知识库中该设备 TA 可知, 能够令该设备进入状态 s 的交互只有需求 R 2 的交互, 那么需求 R 1 因为设备 dev
的状态 s 而控制依赖于 R 2 , 记为<R 1 , dev.s, R 2 >.
情况 2. 需求前置条件之间存在关系: 若需求 R 1 的前置条件为设备 dev 处于状态 s m , 需求 R 2 发生的前置条件
为设备 dev 处于状态 s n , 并且根据设备知识库中该设备 TA 可知, 从初始状态出发到 s m 的所有路径中都包含位置
s n , 即若要到达 s m 必须先经过 s n , 那么需求 R 1 因为设备 dev 的状态 s m 、s n 而控制依赖于 R 2 , 记为<R 1 , {dev.s m ,
dev.s n }, R 2 >.
情况 3. 需求引发的设备状态变迁之间存在关系: 若需求 R 1 的期望交互 int i 驱使设备 dev 进入状态 s m , 需求
R 2 的期望交互 int j 驱使设备 dev 进入状态 s n , 并且根据设备知识库中该设备 TA 可知, 从初始状态出发到 s m 的所
有路径中都包含 s n , 即若要到达 s m 必须先经过 s n , 那么需求 R 1 因为设备 dev 的状态 s m 、s n 而控制依赖于 R 2 , 记为
<R 1, {dev.s m , dev.s n }, R 2 > .
例如, 图 6 展示了初始化与灯光单元控制输出两个需求间的控制依赖关系. 初始化需求驱使灯光单元从灯光
常包含软件组件、设备组件以及组件之间的连接器. 为了表达验证子系统架构, 我们使用
单元初始化 (LUInit) 状态进入灯光关闭 (LUOff) 模式. 控制输出需求可以驱使灯光单元设备进入灯光关闭或灯光
打开 (LUOn) 状态, 并且在设备知识库灯光单元自动机模型中, 从初始节点到灯光打开状态的所有路径中都包含
灯光关闭状态, 符合情形 3, 因此存在控制依赖<LU control output, {LU.LUOff, LU.LUOn}, Initialization>.

LUInit
Light sensor Initialization
(LS) LUInitPulse?
C
LUInit -> LUOff LUOff LUOffPulse?
Initialization Pulse generator t=0
(Init) (PG) t>=2 LUOnPulse?
C RoomBrightness=Brightness
delayOn delayOff
Light unit t<=2 t=0 t<=2

LU control (LU) C LUOn or LUOff RoomBrightness=Brightness+200
output LUOffPulse? t>=2
(LUCO)

Light LU control LUOn
Command (LC) output
LUOnPulse?
图 6 控制依赖例子

4.2 验证子系统架构生成
验证子系统架构生成的目的就是基于识别出的依赖关系将待验证需求分解为多个相关需求组, 并据此定义验
证子系统, 明确每个验证子系统所包含的构件. 通常, 验证子系统的数量与子需求的个数相同. 为了确保每个子需
求都满足待验证的属性, 我们应为每个子需求分配一个验证子系统. 然而, 由于子需求之间存在各种依赖关系, 每
个验证子系统应包含其对应子需求所依赖的子需求, 以确保其能真正实现. 这也可能导致部分子系统是重复的, 因
此, 实际子系统的数量需要剔除重复的子系统. 在验证子系统的构成方面, 根据嵌入式系统的架构, 验证子系统通
UML 组件图, 将输入问
题图的各个领域转换为组件图中的不同组件, 并将行为交互转换为组件图中的连接器.
具体验证子系统架构生成过程为: 首先每个子需求对应一个验证子系统. 除此之外, 该验证子系统还包括该子
需求所依赖的其他子需求. 当然这个过程中可能存在子需求不依赖于其他任何子需求. 最后验证子系统还需要加
入与该子系统中所有需求相关的设备, 即与需求对应的问题图中的机器领域存在行为交互关系的因果领域或词法
领域. 接下来, 我们可以根据所有上述相关要素来比较两个子系统是否重复. 如果发现有重复的子系统, 我们将只
保留其中一个.