UPPAAL模型检测工具

从UPPAAL开始

1. 原理：
   时间自动机是一个有时钟变量扩展的有限状态机，它使用时间变量评估为实数的密集时间模型，所有时钟同步进行。在uppaal中，一个系统被模拟成一个并行的几个这样的时间自动机网络。系统的状态由所有自动机的位置，时钟值和离散变量的值来定义。每个自动机可能会分别触发一个边或与另一个自动机同步，从而导致一个新的状态。

2.UPPAAL工具

uppaal有三部分组成：编辑器、模拟器、验证器。这三部分的功能分别是：

编辑器对模型进行编辑，并进行系统声明和模型声明。编辑器分为两部分：访问不同模板和声明的树窗格以及绘图画布/文本编辑器。模拟器对建立好的模型进行仿真，若所建立的模型符合语法要求，则模型会成功上传并仿真出结果; 验证器对模型应该满足的性质进行验证。

invariant： 粉色 一组在循环体内、每次迭代均保持为真的性质
guard： 绿色 满足条件就跳转下个location
update： 蓝色，跳转下个location后执行该命令，通常为赋值语句
sync：浅蓝色 个人理解是对该路径的描述