安全性：本文提出的GPS时钟自动机不含任何等待不可能发生事件的状态，即自动机无死锁；收到预期条件转移会跳出等待循环，即自动机无活锁；
　　完整性：自动机不含未定义的条件转移参数，包括正常和异常处理，即自动机具有完整性；
　　活动性：经过有限步可回到初态，且无不可达态，即自动机具有活动性。

三、GPS时钟算法分析
　　根据本算法所取得的GPS软件时钟与标准时之间的时钟误差精度主要是由于1.25ms中断与2S中断的不稳定性决定。
1.时钟精度分析
　　由20ms中断和1.25ms中断时序（图2）可以看出，在20ms中断中出现的1.25ms中断的个数一定是16个（由硬件实现），但由于1.25ms中断可能丢失或增加等情况，这就造成了两个相邻20ms中断间隔并非完全是20ms，这将改变GPS时钟自动机的条件转移参数值为1；若丢失或增加一个2S中断，也会改变GPS时钟自动机的条件转移参数值为1。以上两种情况就增加了所维护的GPS时钟的不稳定性因素。我们定义标准时间为T,算法所取到的时间为T′，2S中断处理时间为Δ。下面将讨论它们的具体关系（对条件转移参数值为1时的3种情况进行讨论）：
　　情况一：这种情况发生的概率相对来说较大。若丢失一个1.25ms中断，由于20ms中断之间必须保证有16个1.25ms中断，也就是说即将到来的20ms中断比标准时将推迟1.25ms+Δ，见图5。

absMiddle" border="0" onload="return imgresize(this);" onclick="javascript:window.open(this.src);" style="cursor:pointer;"/>

情况二：这种情况发生的概率相对来说较小。丢失一个2S中断，将会使条件转移参数值为1，使自动机当前状态迁移到初始状态，自动机将重新获取时钟并校正时钟，但不会影响时钟精度。
　　情况三：这种情况发生的概率微乎其微。但若1.25ms中断多了一个，也就是说即将到来的20ms中断比标准时将提前1.25ms-Δ（见图6）；若多了一个2S中断，自动机将重新获取并校正时钟，但不会影响时钟的精度。
absMiddle" border="0" onload="return imgresize(this);" onclick="javascript:window.open(this.src);" style="cursor:pointer;"/>

我们对连续的1.25ms中断进行分析，假设每次1.25ms中断正确到来的概率为p，丢失或增加了一个1.25ms中断的概率为q（稳定情况下每天平均±1×10-11,失锁保持稳定情况下每天平均(1×10-10），其中p+q=1。对以上3种情况，我们进行k次取样，假设前k-1次1.25ms中断均正确到达，但第k次1.25 ms中断丢失或增加了一个1.25ms中断的概率为p{X=k}，此随机变量X符合几何分布［5］，即
absMiddle" border="0" onload="return imgresize(this);" onclick="javascript:window.open(this.src);" style="cursor:pointer;"/>

也就是说，平均有1/(1-p)个1.25ms中断中将有一个1.25ms中断丢失或增加。
　　令从GPS时钟自动机的初态开始运行到现在的总时间为Tw，每两个相邻的1.25ms中断时间为T0=1.25ms，假设GPS时钟的误差精度为ΔT,本算法计算的GPS时钟时间为T′，标准时间为T,所以时钟误差［3，4，5］为