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

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

4.3 可执行验证系统模型生成
这一步就是要根据生成的验证子系统架构生成可以在 UPPAAL 平台执行验证的 NTA. 每个 NTA 都包括生
成验证子系统架构中的软件构件、设备构件以及连接件转换生成对应的 TA. 其具体过程如下.
首先, 我们将验证子系统架构中的设备构件转换为 TA 模型. 这些设备构件主要来源于问题图的因果领域和
词法领域. 对于由因果领域转换而来的设备构件, 它们属于受控设备, 可以直接从领域设备知识库中获取其 TA 模
型. 然而, 来自词法领域的设备构件则代表数据存储域. 在 TA 模型中, 数据存储类的物理设备主要通过更新变量
来实现数据的存储. 在验证模型的过程中, 我们并不过分关注数据本身, 而是更关注整个系统的运行. 因此, 对于数
据存储域类的构件, 我们仅在与其通过连接件连接的软件构件上做出相应处理, 而不单独建立 TA 模型.
接下来为软件构件生成对应的 TA 模型. 这一过程将情景图中的软件行为生成对应的 TA 模型. 需要分别考
虑情景图中包含的顺序结构、选择结构、分支结构、并行结构、循环结构和时间约束. 每种情景图结构对应转换
成 TA 模型结构如图 9 所示. 对于顺序结构, 表示的是两个行为交互之间的顺序关系, 因此对于每个行为交互节点,
在 TA 中建立一个位置, 并建立从前一个位置到该位置的迁移, 迁移上的约束条件根据交互对象类型以及行为交
互的类型建立对应的约束条件. 对于选择结构, 首先标记选择结构开始位置, 如 start, 然后建立两个位置节点, 并建
立从 start 到这里两个位置的迁移, 迁移上的约束条件根据选择结构中的约束条件, 一个为满足该条件的约束, 另
一个即为不满足该条件的约束, 然后根据其后续结构建立对应模型, 最后汇合两条分支到一个位置节点, 如 end.
对于分支结构, 首先也是标记其分支开始位置, 如 start, 其可能具有多条分支, 对于每条分支都建立一个位置节点,
建立从 strat 到每个分支位置节点的迁移, 迁移上的约束条件根据交互对象类型以及行为交互的类型进行建立, 最
后所有分支到一个位置节点.

情景图结构 TA模型结构
int 1 constraint int 2 constraint
顺序结构 int 1 int 2
int 1 constraint
int 1 …
选择结构 Constraint?
int 2 constraint
int 2 …
…
int 1 constraint
…
int 1 图 9 不同情景图结构对应的
分支结构 … … … …
int n … int n constraint …
n
int 1 …
int 1 constraint int n constraint
并行结构 … … … n
…
int n
int 1 constraint
…
循环结构 Constraint? int 1
…
时间约束 int 1 int 2
after(T)
时间约束 int 1 int 2
at(T)
TA 模型结构

对于并行结构, 表达的是所有分支上并发执行. 我们使用紧急位置节点 (位置节点图标中带有 U 的位置节点,
表示在该位置上没有时间流逝) 表示进入紧急位置节点的迁移以及离开紧急位置节点的迁移是同时发生的. 因此
对于并行结构, 我们在 TA 中, 建立每个行为交互的紧急位置节点, 并建立从前一位置节点到该位置的迁移, 迁移
约束条件根据交互对象类型以及行为交互类型建立. 对于循环结构, 建立 TA 模型, 首先标记循环开始位置节点,
如 start, 然后根据循环内的行为交互建立对应的位置节点及到该位置的迁移约束条件, 最后建立从循环内最后一
个位置节点到开始位置节点的迁移, 迁移上的约束条件根据循环结构内的约束条件生成. 对于时间约束, 情景图中
有两类时间约束, 一类表达延迟, 即一个行为交互发生后间隔多久时间再发生下一个行为交互, 另一类表达某个行