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

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

式系统需求一致性的组合验证方法框架, 如图 3 所示. 首先根据问题图和设备知识库识别系统需求之间的依赖关
系, 其次根据依赖关系生成验证子系统架构, 明确每个验证子系统模型所需的构件, 第 3 步根据情景图生成每个构
件的时间自动机表示, 与领域设备知识库一起生成可执行验证子系统模型集合. 最后对可以执行验证子系统进行
一致性验证, 对验证结果进行综合并进行不一致的定位.

① ② ③ ④ 满足一致
依赖关系识别 验证子系统 可执行验证系统 一致性验证与 性结果集
依赖关系 架构生成 验证子系统 模型生成 可执行验证子 不一致定位 验证
架构集合 系统模型集合 结果
不一致定
位结果集
设备知识库
图 3 方法框架图

第 1 步: 需求依赖关系识别. 识别子需求之间由于数据和设备共享造成的依赖关系, 包括数据依赖和控制依
赖. 其中数据依赖是由于数据共享造成的, 主要刻画了有的需求“消费”数据而必须依赖有些需求“生产”数据的情
需要建模涉及相关的人类指令.
况. 控制依赖由设备共享造成的, 刻画了不同需求中设备状态变化导致的“后面”状态的需求依赖“前面”状态需求
的情况. 识别这些依赖关系需要知道不同需求对词法领域的操作以及设备的状态.
第 2 步: 验证子系统架构生成. 目的是要明确验证子系统的组成构件. 基本原则是每个子需求都应该对应一个
验证子系统, 但必须加入被依赖项的需求对应的验证模型. 在每个需求的问题图和情景图中都包含了对软件与设
备的交互, 我们将其转换为构件和连接件, 以形成验证子系统的架构. 其中构件包括由于依赖关系相互依赖的软件
构件, 以及软件构件所需的设备构件, 连接件包括各种构件之间的交互信息.
第 3 步: 可执行验证系统模型生成. 在得到的验证子系统架构的基础上, 生成多组可执行的验证子系统模型.
每一组可执行的验证系统模型都要包括每个构件的 TA 模型, 它们之间的连接, 以及对信道、变量以及模型的声
明. 可以根据情景图自动生成软件构件的 TA. 可以接从领域设备知识库中选择所需的设备 TA. 对于验证子系统
架构中的连接件, 则根据 TA 模型的通信机制生成相应的同步信号和共享变量.
第 4 步: 一致性验证与不一致定位. 我们将生成的多组可执行验证子系统模型通过 UPPAAL 平台进行一致性
验证. 本文中将一致性定义为同一设备不能出现调度冲突. 具体的性质可以依据生成的可执行验证系统模型中的
设备及设备库中的可能状态进行自动生成. 最后综合所有的可执行验证子系统模型验证结果, 只有所有验证结果
都是“一致”的情况下, 最终的结果才为“一致”, 否则为“不一致”. 对所有不满足一致性的需求进行错误定位, 方便
用户进行更改.

3.2 设备知识库
设备一般包括传感器和执行器. 传感器用于定期监测外部环境变量或检测人类行为. 为了构建监视属性的传
感器 TA, 考虑工作模式和可能的模式转换. 我们将每个工作模式映射到 TA 中的一个位置节点. 通常, 传感器有两
种工作模式, 关闭和打开. 工作模式的转换可以是时间驱动的, 也可以是事件驱动的. 同时传感器具有更新它们所
监视的环境变量的自迁移. 例如, 在图 4(a) 中, 亮度传感器通过触发同步信号“BrightnessAcqIns”获取环境亮度. 对
于用于检测人类行为的传感器 TA, 建立模型中的位置节点以及相应的迁移与前述过程非常相似. 唯一的不同在于

执行器通常由控制信号触发, 并以特定的工作模式运行. 这些模式是明确定义的, 例如开或关. 在 TA 建模中,
执行器的工作模式可以直接映射到位置节点, 由映射的迁移触发状态转换. 例如, 图 4(b) 中脉冲生成器有两种工
作模式, 发送打开脉冲 (SendOn) 和发送关闭脉冲 (SendOff), 这对应到 TA 模型中的两个不同位置节点 SendOn 和
SendOff. 执行器通常具有响应时间, 我们可以在执行器接收到同步信号后、达到预期状态前添加待定位置节点,
如图 4(b) 中, 位置节点 PGWork 和 Delay 具有不变式“PGt<=20”, 用来表达接收开关脉冲信号响应时间 20 s 后才
进入对应的发送开关脉冲状态位置节点.