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

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

其转换为形式化语言模型, 最后对其采用形式化手段进行验证. 这些方法关注如何将非形式化或半形式化需求模
型转化为形式化模型. 一些研究聚焦于 UML 或 SysML 相关的模型与其扩展. 例如, 黄友能等人使用扩展后的
UML 顺序图对需求进行半形式化建模, 最后转换成线性混成自动机模型, 并使用 BACH 工具进行相关性质的验
证 [4] . Fotso 等人 [5] 使用 SysML/KAOS 对系统需求进行半形式化建模, 然后将其转化为 B 系统规范 [22] , 最后用
Rodin 工具验证需求一致性. 杨璐等人 [6] 采用半形式化方法消息顺序图 (MSC) [23] 对需求进行建模, 然后再将 MSC
模型转换为时间自动机, 最后用 UPPAAL 工具 [14] 进行一致性验证. 我们前期的工作将 UML 顺序图映射至时钟约
束规约语言 (clock constraint specification lanuage, CCSL), 并提出了基于 SMT 和基于时钟图的验证方法 [7] .
也有工作基于其他的描述. 如李腾飞等人 [8] 提出了一种转换方法, 将 SCADE [17] 模型描述的功能需求内容转换
为 Lustre [24] 形式, 再使用 Jkind 工具进行验证. Vuotto 等人 [9] 提出的需求一致性检查的工具 ReqV, 使用一组结构化
自然语言表达的需求作为输入, 将其翻译成 LTL 语言后使用 SPECPRO 进行验证. Wang 等人 [10] 将自然语言需求
转换为命题投影时间逻辑 (PPTL), 再使用 PPTLSAT 工具对其进行冲突检测. Vidal 等人 [12] 提出了一种领域特定语
言 GIRL, 用于描述软件需求结构不变量、实体以及它们之间的关系, 然后再将 GIRL 模型转换为 Alloy 规约, 使
用 Alloy SAT 求解器自动验证需求一致性. 我们还提出了一种模式语言 SafeNL 来表达安全需求, 将 SafeNL 语句
在详细阐述本文方法之前, 首先介绍一个简单的智能家居系统的案例, 以展示需求一致性验证的全过程, 其问
转换为 CCSL 后使用 MyCCSL 工具进行形式化验证 [3] . 但是, 上述研究工作都聚焦于验证结果的正确性, 并未关
注如何约减验证系统的状态空间.
形式化方法也在探索约减验证系统状态空间的方式. 例如, 统计模型检测方法不遍历整个状态空间, 而是通过
蒙特卡罗模拟的方法估计性质满足或不满足的概率 [25] . Ramesh 等人 [26] 提出一种新的采样方法为蒙特卡罗模拟提
供包含知识更多的样本, 从而减少需要枚举的样本数量, 进而起到验证状态空间约减效果. Zhu 等人 [27] 针对线性时
序逻辑 (LTL) 模型检查状态空间爆炸问题, 将机器学习分类算法引入进来, 提取 LTL 公式特征并输入机器学习二
元分类器得到一个可接受的预测验证结果. Clarke 等人 [11] 主张使用组合模型验证思维约减验证状态空间. 组合模
型检查不直接验证复杂的程序, 而是单独验证其并行过程, 然后通过检查单个过程的属性来推导组合的属性, 进而
实现加速验证的目标 [28,29] . Namjoshi 等人 [30] 将其扩展到参数化通信模型检查中, 以验证分布式网络协议和共享内
存并发程序. Zhou 等人 [31] 提出基于验证性质来约减 SOPC 变量、分支数量的方法, 删减与待验证性质无关的变量、
分支, 得到验证所需的最小变量、分支集合. Shen 等人 [32] 提出了一种通过值约减和转换关系约减的方法, 通过去
除变量的冗余值, 去除与被验证变量无关的转换来实现. 但这些方法大部分并没有应用于需求的形式化验证中, 特
别地, 其中的组合验证以分解为前提, 并不关心怎么分解.
在需求形式化验证中, 也已经存在一些组合验证方法来约减状态空间. 例如, Yuan 等人 [17] 分别基于问题框架
和约束提出了两种投影方法. 基于问题框架的方法通过功能分解将系统分解为子属性, 而基于约束投影的方法则
消除了冗余变量, 两种方法均可减小验证空间. 刘筱珊等人 [18] 提出对轨道交通区域控制器系统进行问题框架需求
建模, 基于投影对需求进行分解, 并将子需求自动生成安全需求验证模型, 进行组合验证. 尽管这些工作都隶属组
合验证的范畴且都有效减少了验证空间, 但它们都是需求的可满足性验证, 并没有针对需求的一致性验证.

2 预备知识

2.1 运行案例介绍

题陈述如下.
智能家居系统问题: 需要一个计算机系统来控制灯光和空调, 该系统涉及到灯光单元 (light unit, LU)、空调
(air condition, AC)、亮度传感器 (light sensor, LS)、温度传感器 (temperature sensor, TS)、脉冲生成器 (pulse
generator, PG) 设备以及灯光命令 (light command, LC)、空调命令 (AC command, ACC) 数据存储. 该系统共有 6
个需求, 分别为初始化 (initialization)、自动存储 (automatic save)、命令存储 (commanded save)、灯光单元控制输
出 (LU control output)、温度控制 (temperature control)、空调控制输出 (AC control output). 其中, 初始化需求用来