uppaal是由瑞典Uppsala大学的信息技术学院和丹麦Aalborg大学计算科学学院联合开发的一个集成工具环境，被用来对转换时间自动机网络模型的实时系统进行建模、仿真和验证。与其他模型检测工具相比，uppaal有很好的高效性和实用性。时间自动机是一个有时钟变量扩展的有限状态机，它使用时间变量评估为实数的密集时间模型，所有时钟同步进行。在uppaal中，一个系统被模拟成一个并行的几个这样的时间自动机网络。系统的状态由所有自动机的位置，时钟值和离散变量的值来定义。每个自动机可能会分别触发一个边或与另一个自动机同步，从而导致一个新的状态。
该博文的模型在uppaal4.0.14上实现，uppaal有三部分组成：编辑器、模拟器、验证器。这三部分的功能分别是：
- 编辑器对模型进行编辑，并进行系统声明和模型声明。编辑器分为两部分：访问不同模板和声明的树窗格以及绘图画布/文本编辑器。
- 模拟器对建立好的模型进行仿真，若所建立的模型符合语法要求，则模型会成功上传并仿真出结果；
- 验证器对模型应该满足的性质进行验证。
该模型有四列火车和一个门组成，在一个时间点只能有一辆火车通过门，下面是建模、仿真、模型性质验证的过程：
建立模型
- 首先建立火车（train）的模型，并分别进行模板声明和变量声明，如下图所示：
图1 train模型和模型中的变量声明
图2 train模型的局部变量声明
- 建立门（gate）的模型，并进行变量声明，如下图所示：
图3 gate模型和模型中的变量声明
- 建立控制器队列的模型（IntQueue），并分别进行模板声明和变量声明，如下图所示：
图4 IntQueue模型和模型中的变量声明
图5 IntQueue模型的局部变量声明
- 模型声明和系统声明，如图6所示。模型声明里列出模板实例，系统声明里列出组成系统的一个或多个进程。
图6 模型声明和系统声明
- 声明系统的全局变量，如图7所示：
图7 系统的全局变量声明
模型仿真
如图8所示，为仿真出来的四列火车uppaal模型：
图8 四列火车的uppaal模型
图9为四辆火车在行驶过程中的调度过程：
图9 模型的调度过程
模型的性质验证
图10中分别对模型应该满足标准和性质进行验证：
图10 对模型的性质进行验证
- 性质A[] Queue.list[N-1]== 0 表示队列中不可能有N个元素，即数组永远不会溢出。实际上，模型定义了N作为火车的数量+ 1来检查这个属性。可以使用与列车数量匹配的队列长度来检查此属性，易知，模型应该满足这个性质。
- 性质A[] Train1.Cross+Train2.Cross+Train3.Cross+Train4.Cross<=1表示在任何时候只有一列火车通过桥。 该表达式使用Train1.Cross来评估结果的真或假，即1或0。易知，模型应该满足这个性质。
- 性质E<>Train1.Cross and Train2.Stop and Train3.Stop and Train4.Stop表示火车1可以过桥，火车2、3、4正在等待过桥，其他火车具有相似的性质。
- 性质E<>Train1.Cross and Train2.Stop表示列车1可以过桥，而火车2正在等待过桥，其他火车具有相似的性质。
- 性质E<>Train1.Cross表示火车1可以过桥，可以用同样的方法检测其他火车。