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

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

则, 在 TA 模型中添加一个位置节点, 建立从初始位置到该位置的迁移, 并在迁移上添加同步信号 Brightness-
AcqIns!. 接着情景图中是一个选择结构, 根据情景图选择结构对应的 TA 模型结构, 先标记当前位置节点为选择结
构开始位置命名为 start, 建立满足约束条件的一个分支, 添加一个位置节点命名为 AutoSendOn, 建立从 start 到
AutoSendOn 的迁移, 并将选择结构中的约束条件 Brightness<100 作为迁移的守卫条件. 同时建立另外一个为不满
足约束条件的分支, 添加一个位置节点命名为 L1, 建立从 start 到 L1 的迁移, 将选择结构中约束条件取反即
Brightness>=100 作为迁移上的守卫条件.

AS
int 8 int 5
BrightnessAcqIns!
Brightness<100? Brightness<100? Brightness>=100
start
L1
int Brightness<=200
Brightness>200? int 9 6 Brightness>200? Brightness<100
AUt=0
Brightness>200
int 10 int 7
AutoSendOn
AutoSendOff
OpenInstructionStorageIns=1,
CloseInstructionStorageIns=1, AUt=0
after(5 ms) after(5 ms) AUt=0
end
AUt>=5
AUt<=5
(a) 自动存储的情景图 (b) 自动存储的TA模型
图 10 自动存储的情景图及生成的 TA 模型

对于满足约束条件的分支, 情景图中下一个行为交互 int 9 内容为 int 9 :<AS, LC, OpenInstructionStorageIns>
[event], 交互对象 LC 是词法领域, 现象类型为事件, 根据表 1 和表 2 规则, 添加一个位置节点, 由于该行为交互下
一个便是分支结构结束, 因此将该位置节点命名为 end, 并建立从 AutoSendOn 到 end 的迁移, 在迁移上添加更新
条件 最后, 对从领域设备知识库中获取的设备构件的
OpenInstructionStorageIns=1. 对于不满足约束条件的分支, 情景图中下一个又是一个选择结构, 因此再分别建
立满足该约束条件和不满足该约束条件的分支, 对于满足约束条件的分支, 添加一个位置节点, 命名为 AutoSendOff,
建立从 L1 到 AutoSendOff 的迁移, 迁移上的添加守卫条件 Brightness>200, 对于不满足约束条件的分支, 由于后续
没有其他行为交互, 因此直接建立从 L1 到 end 的迁移, 并添加守卫条件 Brightness<=200. 接着对于情景图中最后
一个行为交互 int 1 内容为 int 10 :<AS, LC, CloseInstructionStorageIns>[event], 交互对象为词法领域, 现象类型为事
0
件, 因此建立从 AutoSendOff 到 end 的迁移, 并添加更新条件 CloseInstructionStorageIns=1. 最后情景图中还有一个
时间约束, 表示延时 5ms, 因此在 end 位置上添加不变式 Aut<=5, 并在进入 end 位置的所有迁移上添加更新条件
Aut=0, 以及在离开 end 位置的迁移上添加守卫条件 Aut>=5. 由于 end 位置为选择结构的所有分支的汇合位置节
点, 为了使该控制器 TA 可以重复调度执行, 因此建立从 end 位置到初始位置 AS 的迁移. 生成的自动存储 TA 模
型如图 10(b) 所示.
TA 与根据软件构件和其对应情景图生成的软件构件 TA
进行模型声明, 以及变量和信道声明. 在 UPPAAL 工具的模型声明界面添加模型声明 system Initialization,
AutomaticSave, CommandedSave, LUControlOutput, LightUnit, LightSensor, PulseGenerator, AirCondition. 变量声明
便是对生成 TA 过程中添加的时钟、整型变量、信道进行声明.

4.4 一致性验证与不一致定位
根据文献 [34], 需求一致性被定义为在转换系统中存在满足所有时间约束的任意长的时间路径. 时间路径是
一个状态序列, 以及系统从一个状态到下一个状态的时间. 在我们的方法中, 我们使用时间自动机来表示状态、状
态迁移和时间, 用时间计算树逻辑 (TCTL) 来表达要验证的性质. 我们认为需求的一致性在嵌入式系统中表现为