Page 19 - 《软件学报》2025年第4期
P. 19

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


                 设备的调度冲突, 这是由于设备的物理特性决定的. 它指的是在任意时刻, 都不能同时向设备发送不同的信号, 使
                 其处于不同的状态. “不能同时向设备发送不同的信号”这条性质在表达时, 由于信号是来自于其他不同模型的, 比
                 如模型   a 和模型  b, 假设模型  a 在状态  m 和模型   b  在状态  n  时, 分别向该设备发送不同的信号. 我们将这句话表达
                 为 “A[] not 模型  a. 状态  m and 模型  b. 状态  n”, 其含义是在所有路径所有状态中模型       a 的状态  m  和模型  b  的状态
                 n  不能同时达到. 如果验证结果满足则表明这些状态不可能同时发生, 则需求无调度冲突. 如果验证结果不满足,
                 说明有可能在某个时刻, 两个状态会同时出现, 导致向同一设备发送不同信号, 从而产生设备调度冲突. 在生成具
                 体性质时, 需要查找可能向同一设备发送不同信号的模型, 并利用这些信号触发之前的状态进行生成, 可能会生成
                 多个性质. 由于不同验证子系统中涉及的设备和调度设备模型不同, 可运行的性质可能也会有所不同.
                    将针对每个验证子系统生成的一致性性质输入                 UPPAAL  平台, 对该子系统模型进行验证, 即可得到该部分的
                 一致性验证结果. 若每个验证子系统验证结果都是“一致”, 最终的结果才为“一致”, 否则为“不一致”. 对于不满足
                 一致性性质的可执行验证子系统模型, 我们希望定位出在该可执行验证系统模型中具体不满足的原因. 我们假设
                 领域设备库中的设备模型都是正确的, 那么出错的原因只能是在生成的软件构件                           TA  模型. 对于不满足一致性的
                 可执行验证系统模型, 根据其依赖关系, 从依赖的第               1  个需求对应的可执行验证系统模型开始进行一致性验证, 随
                 (ICUOff) 到达初始化状态的所有路径中均包含开启状态, 同时由
                 后依次添加依赖关系上的下一个需求对应的可执行验证系统模型, 据此定位出不满足一致性的具体某个需求对应
                 的软件构件    TA  模型.

                 5   案例与评估


                 5.1   案例研究
                    本节使用航空领域机载侦查控制系统进行案例研究. 该系统由显控设备                        (display control device, DCD)、综合
                 控制单元    (integrate control unit, ICU)、采集接收单元  (collecte receive unit, CRU)、信号处理单元  (signal process
                 unit, SPU) 等组成. 系统能够实现加电控制、初始化、数据加载、信号处理                   (信号分选、信号识别)、频谱监测、
                 温度报告、超温保护等功能, 共          19  个需求. 主要功能包括: 操作员通过显控设备发送指令给综合控制单元以及各
                 分设备, 包括加电、断电或者其他功能执行命令; 显示各分设备实时状态到显控设备上; 采集接收单元依据系统指
                 令实时采集信号, 信号处理单元对采集的信号进行周期处理并传给综合控制单元.
                    步骤  1: 依赖关系识别. 首先识别数据依赖关系. 分析机载侦查控制系统                   19  个子需求, 通过输入输出关系推导
                 出子需求间存在的数据依赖关系. 例如, 温度报告               (TemperatureReport) 需求从综合控制单元传感器      (ICUSensor)、
                 干扰处理单元传感器       (JPUSensor) 等设备采集温度信息      (ICUTemperature,…, JPUTemperature), 并将数据保存到温
                 度数据   (TemperatureData) 词法领域中. 超温保护需求     (OverTempProtect) 从温度数据词法领域中取出各设备的温
                 度信息, 根据具体的温度数值判断是否需要对设备进行开启或关闭操作. 因此, 温度报告需求是温度数据的生产
                 者, 超温保护需求为温度数据的消费者, 存在数据依赖<OverTempProtect, {ICUTemperature,…, JPUTemperature},
                 TemperatureReport>. 类似地, 对所有子需求进行数据依赖识别, 可获得          11  组数据依赖关系.
                    接着, 识别控制依赖关系. 例如, 信号电流控制需求              (WorkingCurrentControl) 能够驱使综合控制单元    (ICU) 进
                 入开启   (ICUOn) 或关闭  (ICUOff) 状态. 初始化需求能够驱使综合控制单元由开启状态进入初始化                   (ICUInit) 状态,
                 再由初始化状态进入到工作          (ICUWork) 状态. 根据领域设备知识库综合控制单元的设备                TA  可知, 由初始状态
                                                                   TA  初始状态到达工作状态的所有路径也都含有
                 开启状态, 符合控制依赖识别方法中的情形               3, 因此, 识别出控制依赖<Init, {ICU.ICUOn, ICU.ICUInit, ICU.
                 ICUWork}, WorkingCurrentControl>, 如图  11  所示. 类似地对所有需求进行控制依赖识别, 最终可获得          6  组控制依
                 赖关系.
                    步骤  2: 验证子系统架构生成. 对于机载侦查控制系统共有                19  个需求, 以每个需求为关注点生成         19  个验证子
                 系统架构. 这里以超温保护子系统架构为例, 说明得到其架构的过程. 根据超温保护需求与其他需求之间的数据依
                 赖关系   (图  11) 可知, 超温保护需求数据依赖于温度报告需求, 这些需求生成超温保护子系统中的软件构件, 并将
   14   15   16   17   18   19   20   21   22   23   24