工业控制系统是控制自动化作业的软硬件系统,目前广泛应用于工业自动化生产领域以及一些关键基础设施中。其中,可编程控制器PLC是应用最为广泛的工业控制器。IEC 61131-3标准是第一个关于PLC控制软件编程语言的国际标准。它将软件工程中先进的编程思想引入到工业控制领域,为PLC控制软件开发提供了统一的编程语言标准,克服了传统工业控制系统开放性差、兼容性差、难于维护等问题。为了便于不同PLC编程人群的使用,以及适应不同的PLC应用场景,IEC 61131-3标准提供了五类各具特色的编程语言,其中包括两种文本化编程语言——指令表编程语言与结构化文本编程语言,以及两种图形化编程语言——梯形图编程语言与功能块图编程语言。此外,该标准还提供了一种称为顺序功能表图的编程语言,用于描述PLC控制软件的整体结构和功能。针对不同的语言设计相应的测试与验证方案,将会增加控制软件测试与验证的复杂度,因此IEC 61131-3标准中多种语言的共存问题,对PLC程序的测试和验证带来了严峻考验。在深入研究IEC 61131-3标准的基础上,本文结合五种编程语言的特点,对形式化建模语言CSP进行了扩展,提出了一种面向IEC 61131-3标准、较为简洁的中间语言ICIL。该语言相对于CSP语言来说,扩展了语句的概念,增强了其计算能力。同时,还增加了周期式扫描通道的概念,该通道能够准确描述PLC程序被周期式扫描执行的行为。为了准确描述ICIL语言,本文在描述其语法的基础上,通过操作语义表示了该语言的含义。操作语义是形式语义学中的一种语义,可用于构建ICIL程序的迁移系统。基于ICIL语言的迁移系统,本文还对PLC程序的形式化验证方法进行了探索。此外,本文根据ICIL语言的语法及标准中各类语言的特性,设计了从IEC 61131-3语言到ICIL语言的转换方法,并且实现了中间语言转换工具ICILConvertor。在该工具中,本文通过多个应用实例的转换实验说明了以上转换方案的可行性。本文对IEC 61131-3标准的中间语言设计,中间语言转换方法的研究,以及PLC程序形式化验证方法的探索,有利于促进PLC控制软件开发及验证的一体化进程,有助于推进工控安全环境的建设。