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

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


                 为交互在指定的时刻发生. 对于延迟的时间约束, 我们对前一个行为交互对应的位置节点加入一个不变式                                 t<=T  表
                 示在  T  时间内不能离开该位置节点, 并在进入该位置节点的迁移上初始化时钟变量                       t, 再离开该位置节点的迁移上
                 加入守卫条件     t>=T. 对于指定时刻发生的时间约束, 我们在进入指定时刻发生的行为交互对应的位置节点的迁移
                 上加入守卫条件      t==T, 表示指定时刻才能发生对应的行为交互转换的约束条件.
                    特别地, 表   1  中给出了交互对象类型以及行为交互现象类型生成迁移上约束条件的对应关系. 对于与因果领
                 域的行为交互, 如果现象类型是值或状态, 在迁移的更新条件中添加                     int x (Phe)=1, 并声明变量  int int x (Phe) 意思是
                 将对应的行为交互       int x 的现象  Phe 声明为一个  int 变量, 并将在迁移上将其值更新为        1, 通过将其值设置为      1  来标
                 识这个值/状态代表的数据被获取, 用来代表数据获取过程. 对于与因果领域的行为交互, 如果现象类型是事件, 在
                 迁移上添加同步信号, 如果是发送信号, 则添加              int x (Phe)!, 如果是接收信号, 则添加  int x (Phe)?, 并声明信道  chan
                 int x (Phe). 对于与词法领域的行为交互, 无论哪种现象类型, 在迁移的更新条件中添加                  int x (Phe)=1, 并声明变量  int
                 int x (Phe) 意思是将对应的行为交互    int x 的现象  Phe 声明为一个  int 变量, 并将在迁移上将其值更新为         1, 通过将其
                 值设置为   1  来标识这个值/状态代表的数据被存储或者获取, 用来代表数据存储或者数据获取过程.

                                   表 1 不同交互对象类型和行为交互现象类型对应的迁移约束条件
                                                      如图

                 参与对象     现象类型                                  迁移约束条件
                           值/状态                 在迁移中添加更新条件, “int x (Phe)=1”, 声明变量“int int x (Phe)”
                 因果领域                 在迁移中添加同步信号, 如果是发送同步信号, 添加“int x (Phe)!”, 如果是接收同步信号, 添加
                            事件
                                                         “int x (Phe)?”, 声明信道“chan int x (Phe)”
                 词法领域 值/状态/事件                   在迁移中添加更新条件, “int x (Phe)=1”, 声明变量“int int x (Phe)”

                    对于构件图中的连接件, 在根据软件构件生成                TA  过程中, 将连接件代表的构件之间的行为交互转换成                 TA
                 中的通信机制. 在     TA  中, 通过共享变量实现数据的通信, 通过同步信号实现控制器与设备之间的调度. 对于软件
                 构件和设备构件之间的连接件, 根据其代表的行为交互类型使用不同的通信机制. 特别的, 对于数据存储域一类的
                 设备构件, 并没有设备       TA  供软件控制器使用同步信号进行通信, 因此软件构件                TA  与数据存储域之间只通过共
                 享变量来实现通信. 具体       TA  模型间的通信机制如表       2  所示.


                                                   表 2 TA  模型通信机制

                              参与对象I            参与对象II            现象类型             TA通信机制
                                                                  值/状态             共享变量
                               机器领域             因果领域
                                                                   事件              同步信号
                               机器领域             词法领域            值/状态/事件            共享变量

                    最后, 对获取的设备      TA  和生成的软件控制器       TA  进行模型声明, 变量和信道声明. 模型声明在           UPPAAL  工具
                 的模型声明界面进行添加, 具体为使用            system  关键字后跟每个模型名称, 每个模型名称用“,”分隔, 最后以“;”结尾.
                 对于信道变量声明使用关键字           chan, 整型变量声明使用关键字       int.
                    下面以智能家居系统中的灯光单元控制输出子系统架构为例介绍生成可执行验证子系统模型的过程. 该子系
                 统中的设备构件包括空调、灯光单元、亮度传感器、脉冲生成器以及灯光命令. 在领域设备知识库中获取设备构
                 件的  TA  模型, 其中灯光命令为词法领域转换来的设备构件, 在领域设备知识库中没有其                         TA  模型. 灯光单元   TA
                 如图  2(a) 所示, 亮度传感器以及脉冲生成器         TA     4  所示, 空调与灯光单元控制输出无关, 只是在初始化需求中
                 对空调进行初始化, 因此其        TA  不再展示. 其软件构件包括初始化、自动存储、命令存储以及灯光单元控制输出,
                 以自动存储软件构件为例, 其输入的情景图如图                10(a) 所示. 该情景图中存在顺序结构、选择结构以及时间约束.
                 将其转换成    TA  模型的过程如下.
                    首先在   TA  中建立初始位置, 命名为       AS, 然后根据情景图结构生成        TA. 对于情景图首先是行为交互          int 8 内容
                 为  int 8 :<AS, LS, BrightnessAcqIns>[event], 其交互对象  LS  属于因果领域, 现象类型为事件, 根据表  1  和表  2 的规
   12   13   14   15   16   17   18   19   20   21   22