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

杨晓 等: 复杂嵌入式系统需求一致性的组合验证方法 1419

NEt>=60 && bcount==3
Brightness=150,NEt=0,bcount=0 SendOn
Brightness=300, PGt>=20 OpenPulse!
PGWork PGt=0
BrightnessAcqIns? NEt=0,bcount=1
NEt>=60 && bcount==0 PGt<=20 PGt<=20
LSWork
Delay
NEt<=60 NEt>=60 && bcount==1 ClosePulse!
PGt>=20
Brightness=120, PGt=0
SendOff
NEt=0,bcount=2
Brightness=50,NEt=0,bcount=3
NEt>=60 && bcount==2
(a) 传感器: 亮度传感器 (b) 执行器: 脉冲生成器
图 4 智能家居系统设备 TA 举例

4 方法细节

Light unit
4.1 依赖关系识别
需求依赖关系分为两类: 数据依赖和控制依赖.
(1) 数据依赖识别
数据依赖指两个或多个需求共享同一个词法领域, 一个需求“生产”数据, 另一个需求“消费”数据. 数据依赖发
生在那些存在对同一数据读写操作的需求之间. 对于使用问题框架描述的需求模型, 若需求 R 1 的交互 int i 表达了
从词法领域 ds 取出数据 data 的行为, 而需求 R 2 的交互 int j 表达了将数据 data 保存到词法领域 ds 的行为. 那么需
求 R 1 由于数据 data 而数据依赖于 R 2 , 记为“R 1 ->R 2 , because of {data}”. 例如, 图 5 展示了命令保存与灯光单元控
制输出需求间的数据依赖关系. 命令保存需求需要软件接收脉冲生成器发出的开关灯信号, 再将信号转换为灯光
开关指令 (OpenInstruction, CloseInstruction) 保存到灯光命令词法领域中. 灯光单元控制输出需求要求软件从灯光
命令领域中取出保存的灯光开关指令, 将其转换为灯光单元能够识别的信号格式后再发给灯光单元, 从而实现开
灯或关灯效果. 图 5 案例存在数据依赖“LU control output -> Commanded save, because of {OpenInstruction,
CloseInstruction}”, 表示灯光单元控制输出因为打开指令 (OpenInstruction)、关闭指令 (CloseInstruction) 而数据依
赖于命令保存.

Pulse generator
(PG)
Commanded C Commanded
save (CS) save
Light
command (LC)
{OpenInstruction, CloseInstruction}

Light
LU control command (LC) LU control
output output
(LUCO)
(LU)
C
图 5 数据依赖例子

(2) 控制依赖识别
控制依赖是指两个或多个需求共享同一个设备, 由于设备状态之间的关系导致的需求之间的先后关系. 这种
先后关系可以通过触发设备发生状态变迁的交互和该需求的前置条件进行识别. 其中需求的前置条件是指需求中
涉及的设备在进入该需求之前的状态. 该条件需要在问题图中进行补充. 根据需求间交互和前置条件之间的关系,