UPPAAL 是一个形式化验证器，可以用来验证自己写的算法写对了没，是否会出现死锁、数据竞争等等不良状况。
它的输入是 UML 状态机图，需要程序员清晰地标注出状态转换的约束条件，然后它会在程序员给出的性质上推理，如果性质有反例，就给出反例的 UML 时序图。
除了推理以外，也可以一步步运行状态机，看看执行的过程玩。
心脏模型必须满足「两次心房事件（PLRL.two）之间的间隔（PLRL.t）必须小于最大心率间隔(≤TLRI , Time Lowest Rate Interval）」
静态检查发现当前的代码不满足这个性质，于是我使用 Get Trace 来获取一个可能的运行路径
界面下方的是执行路径，我（在点击了很多其他步看来看去之后）点击了其中的一步，在这一步里，我的代码运行到了「AVI_CountDown」这一步，可以看到左侧的变量列表里，PDDD.uriT 的取值范围可能会达到 2850 ，这太大了，于是我思考了一下，觉得我应该是在这一步漏掉了一个判断条件。
我点击这个节点，添加了一个新的条件，「 uriT ≤ LRI 」，这样就可以在这一步限制住 uriT 可能的大小了。
果然，这么一来，静态检查就通过了。
在之前代码的基础上， 检查「心房跳动的时间间隔（停留在 PURL.interval 这一行代码上时的 PURL.t ） 不能太长 ( ≥ TURI , Time Upper Rate Interval ）」
随便看看（看了好久）就能看出来，当我的起搏器模型 （ PDDD ）内部的时钟已经走到 200 ms 的时候， PURL （用于验证心脏跳动时间间隔的辅助模型） 里的时钟却被上一次 Vin 时间归零了，所以我总是比它大 200 ms
