系统模型验证与仿真技术解析

### 系统模型验证与仿真技术解析 #### 1. 模型验证基础：PRES+ 模型到时间自动机的转换 在对系统模型进行形式化验证时，若要复用现有的高效模型检查器，首先需将 PRES+ 模型转换为模型检查器的输入语言。这里选用了 UPPAAL 模型检查环境，因其在时间模型验证方面表现高效，而 UPPAAL 的输入语言是时间自动机。所以，待验证的 PRES+ 模型需转换为时间自动机。 转换过程如下： - **变量对应**：PRES+ 模型中的每个位置对应时间自动机中的一个全局变量，该变量存储对应位置中令牌的值。若位置中无令牌，则变量被赋予默认值 ∅。 - **自动机创建**：为 PRES+ 模型中的每个转换 t 创建一个时间自动机，并为每个转换实例化一个时钟变量 ctx。一般情况下，转换 t 对应的时间自动机的位置数量比该转换的输入位置数量多 1。若转换有保护条件，则自动机还会增加一个位置。 - **位置标签**：位置标签为 s0, s1, ..., sn - 1 和 en。有保护条件的转换对应的自动机还有一个标记为 enc 的位置。令牌在 en 表示对应转换已启用，即转换的所有输入位置都有令牌且保护条件满足；令牌在 enc 表示保护条件不满足；令牌在 s0 表示转换的输入位置都无令牌，s1 表示其中一个输入位置有令牌，以此类推。 以下是一个 PRES+ 模型转换为时间自动机的示例： ```plaintext p1 t1 [2..4] x x t2 t3 t4 t5 p2 p3 p4 p5 [1..1] [5..6] [1..4] [0..3] x x x x x + 5 2x x - 2 x y (x + y) mod 3 [x < 10] [x ≥ 10] 5 ``` 转换后的时间自动机系统如下： ```plaintext s0 en t5? t1! p2:=p1, p3:=p1, p1:=∅ ct1 ≥ 2 ct1 ≤ 4 s0 en t1? t4! p5:=p3-2, p3:=∅ ct4 ≥ 1 ct4 ≤ 1 s0 enc t1? t2! p4:=p2+5, p2:=∅ ct2 ≥ 1 ct2 ≤ 4 en p2 ≥ 10 t1? p2 < 10 t3? s0 enc t1? t3! p4:=2*p2, p2:=∅ ct3 ≥ 5 ct3 ≤ 6 en p2 < 10 t1? p2 ≥ 10 t2? s0 en t2? t5! p1:=(p4+p5) mod 3, p4:=∅, p5:=∅ ct5 ≥ 0 ct5 ≤ 3 s1 ct1:=0 ct2:=0 ct3:=0 ct4:=0 ct5:=0 t2? t3? t3? ct5:=0 t4? t4? ct5:=0 t1: t4: t5: t2: t3: ``` 时间自动机中的所有转换都有同步标签，标签与转换名称相同，并附加 “!” 或 “?”。当带有 “!” 同步标签的转换被触发时，系统中所有带有相同标签 “?” 版本的转换必须同时触发。转换的添加反映了 PRES+ 模型中输入位置的令牌情况。 初始时，PRES+ 模型中只有转换 t1 启用，这在自动机中表现为只有对应 t1 的自动机在位置 en 有令牌。从 en 到 s0 的转换编码了 PRES+ 模型中转换的触发，触发时会与受 t1 触发影响的其他自动机同步，以更新它们的状态。同时，根据 PRES+ 转换函数更新输出位置对应的变量，将输入位置对应的变量赋值为默认值。 PRES+ 转换时间延迟区间的上界在自动机中表现为 en 位置的不变式，下界表现为从 en 到 s0 转换的保护条件。此外，还可采取一些措施提高生成自动机的模型检查效率，例如减少时钟数量，使多个转换对应的自动机在某些情况下共享一个时钟，从而合并自动机，减少自动机数量。 #### 2. 实验结果分析 通过将 SystemC 模型转换为 PRES+ 模型进行验证，实验在配备 Intel Xeon 2.2GHz 处理器和 2GB 主内存、运行 Linux 操作系统的机器上进行。以下是几个不同模型的验证结果： ##### 2.1 路由器模型 该模型在事务级别对路由器进行建模，将消息从一个主设备转发到两个从设备之一。验证了四个不同属性： 1. 若发出请求，则未来必须有响应。 2. 若消息发送到从设备 1，则会到达该设备。 3. 若消息发送到从设备 2，则会到达该设备。 4. 若消息发送到从设备 2，则不会到达从设备 1。 验证结果如下表所示，所有属性在几秒内均被验证为满足： | 属性 | 验证时间 (s) | | --- | --- | | 1 | 3.6 | | 2 | 1.2 | | 3 | 1.2 | | 4 | 1.5 | ##### 2.2 分组交换机模型 该模型是 SystemC 参考实现中 pkt_switch 示例的轻微修改版本，一个或多个主设备向一个或多个从设备发送消息，交换机将消息分发到正确的目的地。为处理突发消息，交换机模型为每个主设备和从设备包含一个 FIFO 队列。 验证了四个属性： 1. 无死锁。 2. 主设备发送的所有消息都将被从设备接收。 3. 从设备可能接收消息。 4. 交换机将转发其接收到的每条消息。 属性 2 验证结果为假，原因在于交换机与主设备和从设备之间信号的语义。只有当更新时新值不等于当前值时才会发生事件通知，若多个连续消息相同，只有第一条消息会通过信号到达交换机，后续相同消息无法到达目的地。 不同主设备和从设备组合的验证时间如下表所示： | 属性 | 1m 1s | 1m 2s | 2m 1s | 2m 2s | | --- | --- | --- | --- | --- | | 1 |