可编程逻辑控制器（PLC）是一种被广泛应用于工业控制领域的嵌入式设备。它常被用于实现安全攸关系统的控制逻辑,例如核电、交通、医疗设备等。这些系统对软件的正确性、可靠性有着极高的要求。而目前PLC程序开发主要依赖于个人经验,需求描述错误、程序设计错误难以避免。SPS4PLC来源于规格说明模式语言SPS,是一个专用于描述PLC控制系统的规格说明模式语言,它能够以接近自然语言的方式精确描述PLC控制系统的需求。SPS2PLC是一个由SPS4PLC规格说明自动生成PLC程序的工具,然而其生成过程的正确性尚未经过机器确认。为验证SPS2PLC工具所生成的程序的正确性,本文针对SPS4PLC语言所描述的规格说明,对PLC程序进行自动化的模型检验。本文的主要工作如下:（1）本文给出了一个PLC指令表语言程序的形式语义模型,其中重点讨论了扫描周期长度的设置方法和定时器的语义规则,在此基础上给出了PLC程序到时间自动机模型的翻译方法。（2）本文提出了一种不固定扫描周期长度的建模方法,通过理论分析和实验分析,发现这种不固定扫描周期的建模方法既能够有效检测性质,又能提高验证的效率。不过,这种建模方法在某些情况下可能导致本应通过验证的程序验证不通过,因此本文采用了二次验证的方式,即优先使用不固定扫描周期的模型用于验证,当验证失败后再使用固定扫描周期长度的模型重新验证。（3）为了说明转化得到的时间自动机模型和PLC程序的形式语义模型的关系,本文从操作语义的层面对这二者的行为进行了一致性证明。（4）针对状态空间爆炸问题,本文介绍了影响锥约简在本文工作中的具体实现方案。（5）本文通过观察者方法将SPS4PLC转化为了可验证的TCTL逻辑公式。（6）最后,本文设计与实现了面向SPS4PLC的PLC自动验证工具PLCVerifier。应用PLCVerifier能够快速地对SPS2PLC所自动生成的程序的正确性予以验证。本文应用PLCVerifier检验了SPS4PLC所有范围模式的实现模式,发现了3处实现模式与语义不一致的情况,并给出了修正。针对若干规模不同的PLC系统,验证了SPS2PLC生成的代码,发现在不涉及循环依赖的情况下,SPS2PLC均能生成正确的代码。此外,本工具也可以验证使用其他方式开发的PLC程序。