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

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


                 中  int 2 与 0  int 2 之间的关系. 行为使能关系表示行为交互节点使能期望交互节点, 用行为交互节点指向期望交互节
                           2
                 点的实线箭头表示, 如图       1(b) 中  int 2 与 6  int 2 之间的关系. 需求期望关系表示期望交互节点要求行为交互节点发
                                                   2
                 生, 用期望交互节点指向行为交互节点的实线箭头表示, 如图                  1(b) 中  int 2 与 0  int 2 之间的关系. 同步关系表示行为
                                                                               4
                 交互节点与期望交互节点同时发生, 用无箭头实线表示.

                 2.3   时间自动机
                    我们使用时间自动机        (TA) 作为形式化验证模型, 其验证系统模型采用一组并发的时间自动网络                      (NTA) 来表
                 示. 时间自动机的定义如下        [14] .
                    定义  1. 时间自动机是一个元组        (L, l 0 , X,   Σ  , E, I), 其中  L  是一个有限的位置  (状态) 集; l 0 ∈L  是初始位置; X 是
                                                                   X
                 有限时钟集;    Σ  是动作的有限集合, 例如同步; E ⊆ L×       Σ  ×G(X)×2 ×L  是一个有限的边集, 边上有动作、守卫以及
                 待重置的时钟集, 其中      G(X) 是  X  上的守卫集; I:L→G(X) 为每个位置分配一个不变式.
                    我们以图    2(a) 中的灯光单元为例来解释        TA. 在  LightUnit 中有  5  个位置, 即  LUOff、LUOn  和  LUInit 以及另
                 外两个位置    delayOff 和  delayOn  用以表示响应时间. 在这两个位置中, 有时钟变量         t, 以及不变式   t<=2, 用于限制时
                 来说, 一个嵌入式系统通常包含软件和多个设备, 如传感器和执行器等. 软件从传感器获得信息, 通过执行器控制
                 钟  t 的值, 时钟变量可以随时间增加. 从       LUOff 到  delayOff 的迁移是通过接收同步信号       LUOnPulse 触发.

                                                                       AutoSendOn
                                 delayOff                                        OpenInstructionStorageIns=1,
                   LUOffPulse?                                     Brightness<100
                           LUOnPulse?  RoomBrightness=Brightness+200  AS         AUt=0              AUt<=5
                   LUInit      t=0     t>=2                BrightnessAcqIns!      Brightness<=200  AUt=0
                           LUOff  t<=2
                                  t<=2     LUOn                     Brightness>=100
                   LUInitPulse?  t>=2  t=0                               Brightness>200  CloseInstructionStorageIns=1,
                    RoomBrightness=Brightness  LUOffPulse?                    AutoSendOff  AUt=0
                                  delayOn      LUOnPulse?         AUt>=5
                                (a) 灯光单元                                     (b) 自动存储
                                 OpenInstructionStorageIns==1  OpenInstructionLoadIns=1,  LUOnPulse!  end
                                 LUCO                   OpenInstructionStorageIns=0
                                                        CloseInstructionLoadIns=1,
                                 CloseInstructionStorageIns==1  CloseInstructionStorageIns=0  LUOffPulse!
                                          OpenInstructionLoadIns=0,CloseInstructionLoadIns=0
                                                     (c) 灯光单元控制输出
                                              图 2 智能家居系统时间自动机模型

                    在  NTA  中  TA  之间通过共享变量和广播信道进行通信. 共享变量在系统声明时称, 可用于                       NTA  中的任何
                 TA. 信道提供了一种确保不同         TA  中转换同步的方法. 一旦同步信号发送           (!) 完成, 同步信号接收    (?) 也立即响应.
                 例如, 图  2  给出了灯光控制器例子中的        3  个  TA, 灯光单元与自动存储共享环境变量亮度            (brightness), 灯光单元与
                 控制输出通过同步信号        LUOnPulse 和  LUOffPulse 进行通信. 控制输出发送     (!)LUOnPulse 同步信号, 而灯光单元
                 接收  (?)LUOnPulse 同步信号.

                 3   方法框架与设备知识库


                 3.1   方法框架
                    为了降低验证状态空间, 我们考虑首先对复杂嵌入式系统需求进行分解, 然后分别对它们进行组合验证. 一般


                 外部操作对象, 其需求具有较强的设备依赖性. 这种依赖性使得嵌入式系统的需求相互交织. 这使得我们选择基于
                 情景的问题投影      [21,33] 作为嵌入式系统需求的分解方式, 它可以将设备和需求一起投影在同一个情景维度下, 使得
                 子需求也保持与设备的关系. 我们将投影后的问题图和情景图组合作为输入. 其次, 在组合验证中, 由于需求之间
                 可能存在设备的共享, 为了保障该设备行为的约束, 我们提出对该设备进行预建模, 在验证的时候对其验证系统进
                 行动态组装. 最后, 在验证系统组装中, 由于设备和数据的共享, 造成了需求之间的数据和控制依赖, 这些依赖使得
                 被依赖需求必须与依赖需求一起运行, 才能组装成可以独立运行的验证子系统. 因此, 我们设计了                             4  步的复杂嵌入
   6   7   8   9   10   11   12   13   14   15   16