地下建筑工程中的设备系统经常处于静止状态，为保证其在需要时能安全可靠的运行，需对设备定期进行自动巡检在自动巡检过程中，设备自动巡检控制逻辑起到了举足轻重的作用为了解决复杂的设备自动巡检控制逻辑造成的一系列问题，之前提出了一种层级有限自动机(HFA)的形式化模型，并利用HFA对设备自动巡检控制逻辑实现了行为建模，但并未添加时间属性及验证其正确性与可靠性现提出一种层级时间自动机形式化模型，并利用它对设备自动巡检控制逻辑进行建模，再用UPPAAL对其进行分析与形式化验证，分别验证其安全性、可达性、活性及时间约束，以此来确保其时效正确性与可靠性这种建模与形式化验证方法，弥补了之前无时间约束的漏洞，有效的确保了设备自动巡检控制逻辑的正确性与可靠性最终，该模型通过了模拟和验证，充分证明了设备自动巡检控制逻辑是正确可靠的。