Uppaal 4.0完整教程(二)：火车闸门(The Train Gate),费舍尔协议(Fischer’s Protocol),闲话女孩(The Gossiping Girls)示例

每个女孩都可以给另一个女孩打电话，经过一次对话后，两个女孩就会相互知道所有的秘密【译者注：此处表达的意思可能是一方可能也会知道另一方之前与别人交换来的秘密】。使用整数的解决方案听起来像是黑客行为，事实上，它是如此专业化，以至于我们以后将难以完善模型。该协议基于这样一个事实：在 id 不为 0 的严格 k 个时间单位后，所有想要进入临界区的进程也在等待进入临界区，但只有一个拥有正确的ID。尽管系统的

子不语zzh

919人浏览 · 2024-01-29 17:24:32

子不语zzh · 2024-01-29 17:24:32 发布

Uppaal 4.0完整教程(二)：火车闸门(The Train Gate),费舍尔协议(Fischer’s Protocol),闲话女孩(The Gossiping Girls)示例

A Tutorial on Uppaal 4.0

Updated November 28, 2006

4 示例1：火车闸门(The Train Gate)

4.1 描述

这个例子是 Uppaal 自带的，它是一个铁路控制系统，用于控制多列火车进入一座桥梁。这座桥是一个关键的共享资源，一次只能由一列火车使用。该系统定义了多列火车（本例中假设为4列）和一个控制器。火车不能立即停下，重新启动也需要时间。因此，在火车进入桥梁前有时间约束。当接近时，火车会发送一个appr!信号。之后，它有10个时间单位接收到停车信号。这允许火车在到达桥前安全停下。如果火车没有停下，在这10个时间单位后，它将在接下来的10个时间单位内到达桥梁。如果火车被停下，当之前的火车离开桥梁并发送leave!信号后，控制器会向它发送go!信号，火车随后恢复行进。图13和图14展示了两种情况。

图13

图13：列车闸门示例：train4即将过桥，train3已被停止，train2已接到停车指令并正在停车。Train1正在接近，并向控制器发送了一个appr!信号，控制器随后回送一个stop!信号。不同的区段有时间约束（10, 10, 以及3到5之间）

图14

图14：现在train4已经过桥并发送了一个leave!信号。控制器现在可以让train3通过go!信号过桥。Train2现在正在等待，而train1正在停车

4.2 在Uppaal中的建模

火车闸门的模型包括三个模板：

Train是火车的模型，如图9所示。
Gate是门控制器的模型，如图15所示。
IntQueue是控制器队列的模型，如图16所示。将队列从控制器中分离出来，使得模型更容易正确构建。

火车模板 在图9中的模板有五个位置：Safe, Appr, Stop, Start, 和 Cross。

图9：火车模型

初始位置是Safe，对应于火车尚未接近的状态。这个位置没有不变量，意味着火车可以在这个位置停留无限长的时间。当火车接近时，它与控制器同步。这是通过转换到Appr时的通道同步appr!完成的。控制器有一个对应的appr?。时钟x被重置，参数化变量e被设置为这列火车的身份。这个变量被队列和控制器用来知道哪列火车被允许继续行进或哪些火车必须被停下并稍后重新启动。

Appr位置有一个不变量x ≤ 20，意味着必须在20个时间单位内离开这个位置。两个外出转换由约束x ≤ 10和x ≥ 10守护，对应于桥前的两个区段：可以被停止和不能被停止。在10时，两个转换都被启用，这允许我们考虑到任何竞争条件（如果有的话）。如果火车可以被停下（x ≤ 10），则转换到Stop位置，否则火车前往Cross位置。转换到Stop也被条件e == id守护，并与stop?同步。当控制器决定停止一列火车时，它决定哪一列（设置e）并与stop!同步。

Stop位置没有不变量：火车可以被停止无限长的时间。它等待go?的同步。守卫e == id确保正确的火车被重新启动。与[60]中描述的版本相比，这里的模型被简化，即减速阶段没有明确地建模。我们可以假设，即使火车没有完全停下，它也可能接收到go?同步，这将给出一个不确定的重新启动时间。

Start位置有一个不变量x ≤ 15，它的外出转换有约束x ≥ 7。这意味着火车重新启动并在7到15个时间单位内不确定地达到Cross部分。

Cross位置类似于Start，即它在进入后3到5个时间单位内离开。

门控制器模板 门控制器在图15中与队列和火车同步。它的一些位置没有命名。通常，它们是Committed位置（用c标记）。

图15

图15：火车道闸的门自动机

控制器从Free位置开始（即，桥梁是空闲的），在那里它测试队列以查看它是否为空。如果队列为空，则控制器等待接近的火车（下一个位置）与appr?同步。当火车接近时，它通过add!同步被添加到队列。如果队列不为空，则队列上的第一列火车（通过hd!读取）被重新启动，使用go!同步。

在Occ位置，控制器主要等待正在运行的火车离开桥梁（leave?）。如果其他火车正在接近（appr?），它们被停止（stop!）并添加到队列（add!）。当一列火车离开桥梁时，控制器通过rem?同步将其从队列中移除。

队列模板 队列在图16中基本上有一个位置Start，它在等待控制器的命令。Shiftdown位置用于计算队列的移位（当前端元素被移除时需要）。这个模板使用一个整数数组，并将其作为FIFO队列处理。图16

图16. 火车道闸的队列自动机。该模板被参数化为 int[0,n] e

4.3 验证

我们检查了简单的可达性、安全性和活性属性，以及是否不存在死锁。简单的可达性属性检查给定位置是否可达：

$E<>\ Gate.Occ$ ：门可以接收并存储来自排队接近的列车的消息。
$E<>\ Train1.Cross$ ：列车1可以过桥。我们为其他列车检查类似的属性。
$E<>\ Train1.Cross\ and\ Train2.Stop$ ：列车1可以正在过桥，而列车2在等待过桥。我们为其他列车检查类似的属性。
$E<>\ Train1.Cross\ \&\&\ Train2.Stop\ \&\&\ Train3.Stop\ \&\&\ Train4.Stop$ 与前一个属性类似，所有其他列车都在等待过桥。我们为其他列车有类似的属性。

以下安全属性必须在所有可达状态下成立：

$A[]\ Train1.Cross+Train2.Cross+Train3.Cross+Train4.Cross<=1$ 。
任何时候都不会有超过一列列车在桥上。这个表达式使用了 $T r ain 1. C ross$ 评估为真或假，即1或0的事实。
$A[]\ Queue.list[N-1]\ ==\ 0$
队列中永远不会有N个元素，即数组永远不会溢出。实际上，模型将N定义为列车数量+1以检查此属性。可以使用与列车数量相匹配的队列长度并检查此属性： $(Gate.add1\ or\ Gate.add2)\ imply\ Queue.len\ <\ N-1$ ，其中位置add1和add2是模型中唯一可能进行add!的位置。

活性属性的形式为 $Train1.Appr\ -->\ Train1.Cross$ ：每当列车1接近桥时，它最终将过桥，其他列车也类似。最后，为了检查系统是否无死锁，我们验证属性 $A[]\ not\ deadlock$ 。

假设我们在队列中犯了一个错误，即我们在与hd?同步的过渡中在模板IntQueue中写了e:=list[1]而不是e:=list[0]来读取队首。在考虑索引时，我们可能会感到困惑。有趣的是要注意，除了活性属性之外，其他属性仍然成立。验证给出了一个反例，显示了可能发生的情况：一列列车可能会过桥，但下一列列车将不得不停止。当队列移动时，再次启动的列车永远不是第一列，因此队首的列车被卡住，永远无法过桥。

5 示例2：费舍尔协议

5.1 描述

费舍尔协议是一个著名的互斥协议，为n个进程设计。它是一个定时协议，其中并发进程使用共享变量id来检查延迟以及它们进入临界区的顺序。
【译者注：
费舍尔互斥协议是一个用于在分布式计算环境中实现互斥的算法，它确保多个进程在共享资源时不会同时进入临界区。这个协议由Michael J. Fischer提出。

关键点	说明
目的	确保在分布式系统中，多个进程不会同时进入临界区
环境	通常在一个没有共享内存的分布式系统中使用，进程间通过消息传递进行通信
延迟	在高负载下，由于消息传递的延迟，可能会导致性能问题
容错性	费舍尔协议在节点或通信失败时可能不鲁棒
适用场景	适合于进程数较少，网络可靠的环境

基本步骤	步骤说明
请求阶段	进程向所有其他进程发送请求消息，表示它希望进入临界区
等待阶段	进程等待来自所有其他进程的许可
临界区	一旦获得所有必要的许可，进程进入临界区
退出阶段	进程完成临界区工作后，通知所有其他进程它已退出临界区

】

5.2 在Uppaal中的建模

该协议的自动机如图17所示。

图17

图 17. 费舍尔协议的模板。模板的参数是 const pid。模板具有局部声明 clock x; const k 2

从初始位置（用双圈标记）开始，如果id==0，进程将进入请求位置req，这检查是否轮到没有进程进入临界区【译者注：“是否轮到没有进程进入临界区” 可以理解为某个进程（或线程）通过检查条件，确定是否它具有进入临界区的权限】。

进程在req中非确定性地停留 0 到 k 个时间单位，然后进入等待位置并将 id 设置为它们的进程ID（pid）。在那里，它们必须至少等待k个时间单位，x>k，k是一个常数（这里为2），如果轮到它们了，id==pid，才能进入临界区CS。该协议基于这样一个事实：在 id 不为 0 的严格 k 个时间单位后，所有想要进入临界区的进程也在等待进入临界区，但只有一个拥有正确的ID。退出临界区后，进程重置 id 以允许其他进程进入CS。当进程在等待时，它们通过返回到req，可能在另一个进程退出CS时重试。

5.3 验证

该协议的安全属性是检查临界区CS的互斥性：

$A[]\ P1.cs\ +\ P2.cs\ +\ P3.cs\ +\ P4.cs\ <=\ 1$ 。

这个属性使用了这样的技巧：这些测试评估为真或假，即0或1。我们检查系统是否无死锁，使用属性:

$A[]\ not\ deadlock$

活性属性的形式为:

$P1.req\ -->\ P1.wait$ ，

其他进程也类似。它们检查每当一个进程尝试( request )进入临界区时，它总是最终会进入等待位置。直观地，读者也可能期望属性P1.req --> P1.cs，类似地表示临界区最终是可达的。然而，这个属性被违反了。解释是，进程被允许永远留在等待中，因此有一种方式可以避免临界区。

现在，如果我们尝试修复模型，并在 wait 位置添加不变量x <= 2*k，属性P1.req --> P1.cs仍然不成立，因为可能达到一个P1.wait处于活动状态的死锁状态，因此有一条路径不通往临界区。

死锁如下：P1.wait满足0 ≤ x ≤ 2和P4.wait满足2 ≤ x ≤ 4。在这个状态下，由于P4.wait上的不变量和P4.wait因为id == 1不能离开，所以禁止延迟。

6 示例 3：闲话女孩

6.1 描述

设有 n 个女孩，每个女孩都有一个私密秘密想与其他人分享。每个女孩都可以给另一个女孩打电话，经过一次对话后，两个女孩就会相互知道所有的秘密【译者注：此处表达的意思可能是一方可能也会知道另一方之前与别人交换来的秘密】。问题是要找出需要多少通电话，以便所有女孩都知道所有的秘密。问题的一个变种是增加对话时间，并询问交换所有秘密所需的时间，允许同时进行电话。

这个问题的基本表述并不是时钟自动机，通常是一个组合问题，有一个由 n 位组成的字符串，每个女孩可能最多取 $2^n$ 个值。这意味着我们总共有一个由 $n^2$ 位组成的字符串，取 $2^{n^2}$ 个值（与系统的其他状态相乘）。

6.2 在 Uppaal 中建模

我们面临着关于如何表示秘密以及在哪里存储秘密的选择。一种方法是使用一个整数，并使用算术运算手动设置或重置其位。尽管系统的大小受整数大小的限制，但快速复杂性评估表明，状态空间无论如何都会迅速爆炸，所以这实际上并不是一个限制。另一种方法是使用布尔值数组。使用整数的解决方案听起来像是黑客行为，事实上，它是如此专业化，以至于我们以后将难以完善模型。布尔值模型肯定更易于阅读，这对于正式验证是可取的。第二个选择是在哪里存储消息：在一个大型共享表中还是与每个女孩过程的本地存储。参考模型可在 http://www.cs.aau.dk/~adavid/UPPAAL-tutorial/ 获取【译者注：貌似链接已经失效】。

通用声明(Generic Declarations) 全局声明包含：

const int GIRLS = 4;
typedef int[0,GIRLS-1] girl_t;
chan phone[girl_t], reply[girl_t];

这使我们能够轻松扩展模型。请注意，可以声明通道数组由给定类型索引，这隐式地为它们提供正确的大小(Notice that it is possible to declare that arrays of channels are indexed by a given type, which implicitely gives them the right size.)。这对于稍后通过标量(scalar)集进行对称性减少(symmetry reduction)是必要的。

女孩过程(模板) 被命名为 Girl，并且具有 girl_t id 作为参数。每个女孩都有不同的 ID。系统声明很简单：system Girl;。这利用了 Uppaal 的自动实例化功能。生成范围在其参数上的 Girl 模板的所有实例。实例的数量由常量 GIRLS 控制。

灵活建模(Flexible Modelling ) 我们为模板 Girl 声明了三个本地函数。请注意，它们可以访问参数 id。这些函数用一个独特的秘密来初始化模板（start()），并向其他模板发送和接收秘密（talk() 和 listen()）。我们可以更改这些函数，但仍保持相同的模型，这使得模型灵活。

整数(Integers) 使用整数进行编码，在全局声明中添加了 meta int tmp;，并在模板 Girl 的本地声明中添加了以下内容：

girl_t g;
int secrets;
void start() { secrets = 1 << id; }
void talk() { tmp = secrets; }
void listen() { secrets |= tmp;}

初始化是通过将比特位 id 设置为一来完成的。初始的Committed位置确保在开始交换秘密之前初始化了所有女孩。然后我们有一个使用共享变量的标准消息传递，接收者将发送的秘密与自己的秘密合并（逻辑或）。共享变量被声明为 meta，这意味着它是一个特殊的临时变量，不是状态的一部分，即不会在两个状态之间引用这样的变量。我们假设这些函数是与频道同步使用的。

布尔值(Booleans) 使用布尔值进行编码，在全局声明中添加了 meta bool tmp[girl_t];，并在模板 Girl 的本地声明中添加了以下内容：

girl_t g;
bool secrets[girl_t];
void start() { secrets[id] = true; }
void talk() { tmp = secrets; }
void listen() { for(i:girl_t) secrets[i] |= tmp[i]; }

在这个版本中，我们使用数组之间的赋值进行 talk()。函数 listen() 使用了一个迭代器。gossip0.xml（使用整数）和 gossip1.xml（使用布尔值）模型的自动机在图 18 中给出。

图18

图18：对闲话女孩的第一次建模尝试

这第一次尝试描绘了我们希望模型在发送和接收方面对称，并且 talk() 和 listen() 的对称使用也让这件事情看起来相当自然。局部变量 g 记录了给定模板正在与哪个其他女孩通信。发送者选择其接收者，接收者选择其发送者

【译者注：

----------------------------------------------------------

j:girl_t 是选择(selections)，详见第一期，代表j是girl_t类型的变量，能在关联的边上访问，并且它们将在其各自类型的范围内取一个非确定性值
在这里插入图片描述
】。

----------------------------------------------------------

让我们首先在三个方面改进模型：

中间状态 Listen 应该被设为Committed，否则所有半开始和完成的呼叫的交错 $^{[1]}$ (interleaving)将发生。
一个选择(select)就足够了，因为我们在这里建模的是其他东西，即 girl id 选择一个频道 j，任何选择相同频道的其他女孩都可以与 id 通信。
当局部变量 g 的值不相关时，即不需要保留之前的通信时，它会对状态空间产生不良影响。我们可以在开始时对称地设置它，并在通信后将其重置为 id。

【译者注：

----------------------------------------------------------

在这里插入图片描述

---------------------------------------------------------- 】

这些是模型的典型“优化”：通过使用Committed位置避免无用的交错，确保您准确地模拟所需内容而不是更多，以及“活动变量减少”。更新后的模型（gossip2.xml/integers(整数)，gossip3.xml/booleans（布尔值））在图 19 中显示。

图19

图19：改进后的闲话女孩模型

模板保持了一个不变量，即变量 g 始终等于 id，除非它没有发送。此外，当选择一个频道j时，它对应于确切的女孩 j。一个提交位置就足够了，但标记它们两个是一个好习惯。当我们阅读模型时，它更明确。由于模型表现更好，我们现在可以在大致相同的时间内检查 5 个女孩而不是 4 个，考虑到模型的指数复杂性，这是一个非常好的改进。

进一步优化 我们可以通过声明只有一个频道 chan call 来抽象哪条通信线被使用。由于语义规定，任何一对启用( enabled )的边（call!,call?）都可以被采取，我们不需要进行额外的选择。此外，进程无法与自身同步，因此我们也不需要这种检查 $^{[2]}$ 。缺点是我们从发送者的角度失去了对接收者的信息。在我们的案例中，我们不需要这个。我们也可以摆脱局部变量 g。我们可以使用旧函数的序列 talk()-listen()-talk()-listen()，但我们可以通过将中间的 listen()-talk() 合并为一个并简化 listen() 为一个简单的赋值来简化这些，因为我们知道消息已经包含了发送的秘密。全局声明更新为仅包含 chan call;用于频道。更新的自动机在图 20 中描绘。

在这里插入图片描述

图20：闲话女孩的优化模型

模型的整数版本（gossip4.xml）有以下局部函数：

int secrets;
void start() { secrets = 1 << id; }
void talk() { tmp = secrets; }
void exchange() { secrets = (tmp |= secrets); }
void listen() { secrets = tmp; }

模型的布尔值版本（gossip5.xml）更改为：

bool secrets[girl_t];
void start() { secrets[id] = true; }
void talk() { tmp = secrets; }
void exchange() { for(i:girl_t) tmp[i] |= secrets[i];
secrets = tmp; }
void listen() { secrets = tmp; }

exchange函数本可以写为：

void exchange() {
for(i:girl_t) secrets[i] = (tmp[i] |= secrets[i]);
}

这几乎是一样的。不同之处在于第一种情况下解释指令的数量较少。更进一步的优化将是在模型中将这些函数内联到边上，但那样我们会为了不到5%的速度提升而失去可读性。通过拥有一个参数化的共享表并完全避免消息传递，可以进一步优化模型。我们把这留给读者作为练习，但我们注意到这种改变破坏了每个过程本地秘密( local secrets)的漂亮设计。

6.3 验证

我们检查所有女孩都知道所有秘密的属性。对于模型的整数版本，属性是：

$E<>\ forall(i:girl\_t)\ forall(j:girl\_t)\ (Girl(i).secrets\ \&\ (1 << j))$

我们可以写一个更短但不太明显的等价公式，利用 $2^{GIRLS} - 1$ 生成一个位掩码，将前 GIRLS 位设置为一：

$E<> forall(i:girl\_t)\ Girl(i).secrets\ ==\ ((1\ <<\ GIRLS)-1)$

布尔版本的公式是：

$E<>\ forall(i:girl\_t)\ forall(j:girl\_t)\ Girl(i).secrets[j]$

这些公式使用了 “ $f or - a ll$ 结构，它提供了紧凑的公式，可以随着模型中女孩数量的增加而自动扩展。整数版本通过位掩码检查位是否设置。

表 1 显示了不同女孩数量的不同模型的资源消耗。

表1：不同女孩数量的不同模型的资源消耗，结果以秒/兆字节表示

实验在配备 Uppaal rev. 2842 的 AMD Opteron 2.2GHz 上运行。结果显示谨慎处理模型并尽可能优化模型以减少状态空间是多么重要。我们注意到，在这个模型中我们甚至没有时间。由于其简单性，整数模型的速度更快，但内存消耗略低。

6.4 改进模型的验证

Uppaal 特性了两种主要的技术以改进验证。这些技术直接关系到验证，并且与模型优化正交。第一个是对称性减少。由于我们从一开始就设计了对称的模型，利用这个特性是通过使用一个标量集作为类型 girl_t 来完成的。第二个特性是泛化的扫描线方法。我们需要定义一个进度度量来帮助搜索。此外，只有布尔模型适用于对称性减少，因为我们不能以对称的方式（使用标量）访问整数中的单个位。

对称性减少( Symmetry Reduction ) 唯一需要改变的是类型 girl_t 的定义。我们为新模型（gossip6.xml）使用了一个标量集：

$typedef\ scalar[GIRLS]\ girl\_t;$