随着自动化技术的发展,工业控制系统在工业、能源、交通、水利等领域得到了广泛的运用。它在我国基础设施的自动化运转中发挥着重要作用,尤其是在一些安全攸关领域,例如核设施、航空航天等。因此,工业控制系统的控制软件一般都需要经过严格的、系统的测试,以确保控制软件的质量。然而随着软件规模的不断上升,测试的难度也相应地不断增加。加之测试技术本身具有一定的局限性,例如不能保证发现软件中所有的漏洞,也不能发现软件逻辑实现上的错误等。这使得测试技术并不能胜任安全攸关领域中控制软件的验证工作。而形式化验证技术能够以数学的方式证明系统在设计或实现上的正确性,因此近些年来受到了安全攸关领域的青睐,是学术界和工业界都十分关注的研究热点。IEC 61131-3是工控领域中关于控制软件编程语言的国际标准。结构化文本(ST,即Structured Text)是其提供的一种高级文本编程语言。与标准中的其他语言不同,ST允许用户使用数组、结构体等数据结构和分支、循环、函数调用等控制结构。因此它是用户实现具有复杂控制逻辑或算法的控制软件时的首选编程语言。工业化和信息化的深度融合使得控制软件越来越复杂,为ST语言的使用提供了广阔的应用场景,也带来了不断增长的验证需求。为了满足日益增长的验证需求,本文提出了基于模型检查技术的ST程序(使用ST语言编写的控制软件的简称)形式化验证方法。首先,本文面向ST程序定义了一个称为BM(Behavior Model)的形式化模型。BM可描述ST程序的运行时行为,包括工控领域中特有的周期性扫描行为。然后本文从源代码层面,提出了形式化建模方法,即从ST程序源代码得到BM模型的方法。再后,本文提出了BM上线性时态逻辑性质的形式化验证方法。为了提高形式化建模的效率,本文研究了ST语言的形式化操作语义,并基于该语义实现了形式化建模、验证过程的自动化。最后,本文设计实现了一个自动化验证工具。在实践中,本文对工业生产过程中的控制系统进行验证,发现了其实现中的错误,也从侧面证实了本文方法的可用性和实用性。