PLC(可编程逻辑控制器)是一种嵌入式设备,广泛应用于工业控制领域。这些领域对程序的正确性要求很高,但传统的模拟、测试等方法无法覆盖所有情况,因此有必要采用严格的形式化方法对其进行验证。现有的PLC形式验证工作没有给出系统的方法去证明时序逻辑描述的时序、实时规约。本文提出了一组验证规则,帮助用户通过逻辑推导的方式证明PLC程序的时序、实时性质。本文的主要研究工作如下:(1)给出了一种PLC编程语言——ST(structured text)语言子集的一个操作语义。该语义覆盖了大部分重要特性如扫描周期、TON定时器等。其中定时器模型采用西门子S7-200系列PLC中10-ms分辨率定时器实现,和现有的模型相比更加精确、符合实际。在此基础上扩展了Hoare逻辑,以证明单周期性质,即程序执行一个扫描周期的效果。(2)提出了一组针对时序性质的验证规则。从单周期性质出发,运用这些规则可推导出线性时序逻辑描述的多周期性质。这些规则主要针对PLC程序中两类常见的规约:安全性和自保持性质。其中安全性性质的验证已经有比较成熟的工作,本文将现有方法迁移到PLC这样的循环执行系统。自保持结构是PLC程序特有的基本编程环节,本文提出了针对这类结构的形式规约和验证方法。(3)提出了一组针对实时性质的验证规则。由于PLC程序的实时功能主要通过定时器实现,首先使用实时逻辑MTL(metric temporal logic)描述了定时器在各种情况下的行为;然后提出了定时器规则,以证明典型情况下的带定时器程序满足这些规约;再结合其他时序性质,推导出整个程序所满足的实时性质。(4)使用交互式定理证明器Coq实现所有验证环节:包括程序形式语义、规约语言和验证规则。开发了针对单周期性质和定时器性质的自动证明策略,以简化验证过程。使用上述方法,对多种常见的编程环节进行了验证。结果表明,该方法能够有效地处理典型的PLC程序,并能纠察出一些错误。