UPPAAL使用方法

由于刚开始学习时间自动机及其使用方法，对UPPAAL使用不太熟悉，网上能找到的教程很少，摸索了很久终于成功实现一个小例子，所以记录一下详细教程。

这里用到的例子参考【UPPAAL学习笔记】1：基本使用示例，详细信息可自行有链接查看，本文重点手把手教学UPPAAL方法，本人也是刚开始学习，有不足或理解有误的情况欢迎指出。

下面使用几个小例子展示使用 UPPAAL建模，验证的方法。

简单迁移

建模

首先，打开UPPAAL 后，【文件】→【新建模型】
在这里插入图片描述
新建模型如下所示：

需要建的模型如下图，为一个简单的TS模型

在【编辑器】的模板（【Template】）中，右侧通过添加位置、顶点（钉子）和边进行建模。

位置用名称和不变量标记。通过下面红框修改位置类型
在这里插入图片描述
通过【编辑location】，在【名字】处为位置命名，在【Invariant】处编辑不变量

通过下图添加位置

以相同的方法，将其命名为end，通过下图添加边，边用守卫条件（Guard）（例如，e == id）、同步（Sync）（例如，go?）和赋值（Update）（例如，x:=0）标记。

在这里插入图片描述
创建模型如下，可以在红框处修改模板名字，添加参数

在【模型声明】处将模型实例化，得到Process，此处实例化Template()，名称与模板名称相同，由于此处模板没有参数，故()内为空

// Place template instantiations here.
Process = Template();
// List one or more processes to be composed into a system.
system Process;

在这里插入图片描述
建模完成后，对模板进行语法检查，点击【工具】→【检查语法】，若右下角没有消息，则语法无误，可继续进行模拟或验证。

模拟

在【模拟器】中可以看到这个模型
在这里插入图片描述
选中例化对象Process，点击【下一步】，就可以往下走

当TS走到end状态后就无路可走了，故【使能迁移】里也没有选项了

验证

在【验证器】中，点击【添加】，在【待验证性质】中输入待验证性质

性质描述意义如下：

E<> p：存在一条路径，其中最终成立p，可达属性（）。
A[] p：对于所有路径，始终成立p，安全属性（安全属性的形式是：某些坏事永远不会发生）。
E[] p：存在一条路径，其中始终成立p，安全属性。
A<> p：对于所有路径，最终将成立p，活性属性（活性属性的形式是：某些事最终会发生）。
p --> q：每当成立p时，最终将成立q，活性属性。

此处验证两条性质：
E<> Process.end
A<> Process.end

在这里插入图片描述
依次对性质进行验证，选中需验证的性质，点击【开始验证】即可。验证结果在下方【验证进度与结果】中。

此处，E<> Process.end表示存在一条路径，未来能让实例Process到达end状态，显然，验证结果通过；
A<> Process.end表示对所有路径，都能在未来让实例Process达到end状态，验证结果不通过。因为一个TS的Guard条件通过，只表示“这条迁移可以发生”，但不代表一定会发生，可能存在一直停留在start状态的情况，而不发生这条唯一的迁移，因此不满足这条性质。
若想让迁移在一定条件下一定发生，可以为状态设置不变性，一旦不变性不满足，就无法停留在这个状态，迫使其进行迁移。

互斥进入临界区

新增内容为：

边的标记方法
模板参数设置及实例化

建模

模型如下图
在这里插入图片描述
参数声明，模板名字为mutex,参数表设置：

const int[1,2] me, int[0,1] &req_self, int[0,1] &req_other

可以简单的把参数表理解成进程模板例化时候的构造器，这里有三个参数：

me表示自己的ID，这是个[1,2]范围内不变的值，所以给个const修饰
req_self表示自己有没有请求进入临界区，这是个[1,0]范围内双方都要知道的变化的量，所以用传引用的方式，传个全局变量的引用进来
req_other也是同理，表示对方有没有请求进入临界区

在这里插入图片描述
全局变量声明：

// Place global declarations here.
int[0,1] req1, req2;
int[1,2] turn;

在这里插入图片描述

模型声明，此处对模板的实例化，需对应模板参数设置输入参数，其中req1, req2为全局变量，在全局的声明中设置, 为这个进程模板mutex例化为P1和P2，全局变量req1和req2保存两方有没有请求进入临界区（用传引用的方式传进去），整个系统就是这两个例化的进程：

// Place template instantiations here.
P1 = mutex(1, req1, req2);
P2 = mutex(2, req2, req1);

// List one or more processes to be composed into a system.
system P1, P2;

在这里插入图片描述

同步通道和时钟控制

新增内容：

模板参数设置及实例化
一个项目中使用两个进程模板
为状态添加不变性条件

建模

模型如下图所示
在这里插入图片描述

需建立两个模板，新建模板方法为：【编辑】【添加模板】

在这里插入图片描述
建模方法同上，对边的标记方法为：右键需标记的边，选择【编辑edge】

依次填写，Guard（守卫条件，如，x>=2，e == id），同步通信（Sync，如，go?，reset?），赋值（Update，如，x:=0，e:=id）

建立模型如下图。
模板P1是一个自循环，Guard条件x>=2时进行Sync（同步通信），往通道reset上发送重置信号（!表示发送，?表示接收)
在这里插入图片描述
模板Obs（意为Observer，观察者），行为就是接收到通道reset上的信号之后，就将全局变量x设置为0（其实是表示时钟重置，要从后面声明的地方看出这一点）：

这里要注意taken上有个C，因为它勾选了Commited，被标记Commited的状态会冻结时间流逝，而且下一次转移一定从某个Commited状态开始（要把所有冻结时间的状态走出去，才能考虑普通的状态），如果多个状态被标Commited，它们就按Interleaving算。
模型声明部分，这里可以不去显式做例化（为啥？），直接两个模板拿来用：

// Place template instantiations here.
// Process = Template();
// List one or more processes to be composed into a system.
system P1, Obs;

在这里插入图片描述

设置全局变量（全局的【声明】），其中，x是时钟（clock），reset是通道（chan）：

// Place global declarations here.
clock x;
chan reset;

在这里插入图片描述

模拟

语法检查通过就可以去模拟，就是P1发信号然后Obs重置然后再回来,因为taken状态被标Commited，所以到必须使Obs走出这个状态才能桀纣往下走，即图中红框部分：总是先让Obs回到idle状态。在这里插入图片描述

验证

此处验证两条性质：
A[] Obs.taken imply x>=2,即对所有路径的所有状态都有，如果Obs到达了taken状态，一定有时钟x满足x>=2，验证是通过的，因为x>=2才能发信号到reset通道上，让Obs同步接收之后进到taken状态。
E<> Obs.idle and x>3，即存在某个路径上某个状态，Obs在idle状态闲置时就有x>3了，验证也是通过的。这条性质直观上可能让人感觉不能通过（因为x>=2是P1迁移的条件），但是回想最开始学的，这些Guard条件满足时只表示“迁移可以发生”，而不是一定会发生，所以P1完全可以x超过3了还不发生迁移，也就不会往reset发信号，所以Obs也就处在最开始的idle状态了。
在这里插入图片描述

为状态添加不变性条件

对上述E<> Obs.idle and x>3性质的验证通过，是因为可以一直停留在某个状态，要解决这个问题，可以为状态添加一个有关时钟的不变性条件，当时间流逝使得这个条件不满足时，就不得不离开这个状态，发生迁移。
在模板P1中编辑位置loop(双击或右键编辑)，在【Invariant】里添加x<=3，为P1的loop状态添加了x<=3的限制，也就是说它最多可以在这里停留到时钟流到3，就必须执行迁移到别的状态去了.
在这里插入图片描述

验证性质A[] Obs.taken imply (x>=2 and x<=3)，即只要Obs到了taken状态，时钟x一定在2和3之间，验证通过。