工业控制系统作为交通、能源、先进制造等关键基础设施的核心,被视为国家安全战略重要组成部分。随着国家工业制造智能化深入发展,一方面,不断复杂化的功能需求及交互环境导致系统安全保障变得更加困难。系统故障可能对物理世界的生命、环境、财产等造成严重损害。另一方面,信息物理融合系统作为工业4.0核心架构,展现出灵活、高效、经济等众多优点。因而吸引越来越多传统系统加入到“工业互联网”,以便打通“信息孤岛”,提高产能,增强行业竞争力。直观地,对行为正确性要求近乎苛刻的工业控制系统而言,软件功能日益复杂化,并从“物理隔离”的本地环境转向“开放式”的网络环境,对系统安全带来极大挑战。面对日益复杂化、开放化的系统发展趋势,传统方法主要利用测试与仿真提高系统正确性,即不利于排查高隐蔽性缺陷,又可能伴随巨大经济开销。因而,形式化方法,作为开发高可信软件的一类关键技术,受到学术界和工业界的高度关注。现有研究中,大部分对存量代码进行静态验证。若系统功能复杂化,一般的静态方法复杂度也会随之变高,且在缺乏复杂系统分解机制的情况下,产生较大经济开销。同时,对于已编码程序,若在开发后期发现重大问题,则可能面临高昂的修复成本,甚至被迫放弃系统。从部署的角度考虑,若生产环境中出现与模型中正确性假设相冲突的情况,如遭受恶意攻击,则难以为其提供有效保护。而有关运行时验证的现有研究中,主要采用外部监控方式,实时性与自修复能力不可避免地受到通信环境、同步机制、电气特性等诸多因素制约。因此,本文面向遵循IEC 61131国际规范的工业控制系统,研究覆盖设计开发、测试验证、现场运行阶段的系统安全保障方法,主要包括模型设计与验证、代码生成、性质挖掘以及运行时验证。首先,基于支持精化关系的形式化语言,提出工业控制领域相关的建模及验证方法,有效保障设计模型与需求规范一致性。然后,利用精化模型生成对应的工业控制程序代码,从而避免人工编码过程中可能引入的错误,并提高开发效率。紧接着,基于作用于源码的静态验证技术,提出一种程序性质挖掘方法,可进一步地指导我们对系统软件分析、修复、迭代、加固等。最后,为保障生产环境中系统安全,提出一种非侵入式的运行时动态验证方法,且利用代码不敏感、本地化、增量式验证机制,提高其普适性、实时性和高效性。旨在增强系统在监控诊断、实时防护、自我修复等方面的关键能力。本文的主要贡献如下:·对应软件生命周期的设计开发阶段,基于Event-B形式语言与精化特性,提出一种面向工业控制系统的建模及验证方法,提供支持离散时间属性且包含固件层、配置层、业务层的通用模型框架。一方面,利用精化机制对复杂系统进行分解,使其较好地适用于复杂功能的建模;另一方面,通过对设计模型与需求规范的一致性验证,有效保障系统设计过程中的正确性,从而起到尽早发现系统缺陷、减少后期重大问题修复风险的作用。·在构建具体的业务层模型之后,提出从模型到代码的自动生成方法,并且生成的工业控制程序符合IEC 61131-3国际规范。利用代码生成的方式可以较好地保障模型与程序的一致性,从而避免手动编码过程中可能引入的错误,且提高开发效率。·对应测试验证阶段,提出一种作用于工业控制程序源码的性质挖掘方法。该方法利用循环不变式、可满足性模理论、经典机器学习算法以及精化关系,静态地验证用户性质并尝试进一步挖掘更强的性质描述,可用于指导对系统进一步分析、修复、迭代、加固等。·对应生产环境中的运行阶段,提出一种非侵入式的工业控制系统运行时验证方法。一方面,提供用于描述工业控制领域性质规范的特定语言;另一方面,实现代码不敏感、本地化、增量式的验证机制,提高普适性、实时性和高效性,从而增强系统在实时安全防护和动态修复等方面的重要能力。