工业控制系统(ICS)是应用于工业基础设施的系统,多使用于监督控制、数据采集和工业自动化等。工业控制系统中包含了多种不同的硬件、软件,整体具有复杂的、基于组件的体系结构。传统的工业控制系统是仅基于机械和电子设备的封闭系统。随着网络技术的发展,现如今越来越多的信息技术和通信设备集成到了现代工控系统中,增加了系统之间的复杂性和互连程度。同时,有关于工业控制系统的网络安全问题也逐渐显现增加。越来越多的防御方法被应用于工业控制系统网络,极大提高了系统的安全性。同时,有关于工控网络系统安全防御的形式化描述也成为一个热点。形式化方法通过精准的数学描述,抽象系统行为,以验证安全防御方法应用于工控系统中逻辑的可行性和正确性。本文将主动防御方法应用于工业控制系统的安全防御中,使用PAT为安全防御系统建立时间自动机模型,并使用形式化验证方法对模型进行分析验证,以验证评估该防御方法在工业控制系统应用中的正确性和安全性。本文首先对工业控制系统以及当前安全防御方法相关知识进行研究和分析,将主动防御方法应用于工业控制系统防御。本文使用PAT为系统行为、攻击者进攻、安全判决策略、系统受到攻击后恢复机制等建立时间自动机模型,描述安全防御系统防御行。最后选择使用模型检测作为形式化验证方法,对系统行为以及安全防御方法的死锁、正确性、可达性以及线性时序逻辑等安全属性进行形式化验证分析。本文的主要成果如下:(1)使用时间自动机为主动防御工业控制系统安全模型建立模型,模拟安全防御模型的动态防御机制,描述安全模型的工作过程。比较选择主动防御中执行体的个数,验证选择三个执行体可以更好的平衡正确率与系统安全防御的效率。(2)使用时间自动机为主动防御的单选判决策略、多选判决策略建立模型。结合多选判决和单选判决策略的特点提出复合选择判决策略,并建立时间自动机模型。该策略具有减少系统资源开支,增加判决选择正确率的优势。(3)为系统编写相关断言语句,对系统模型进行有关死锁算法,可达性算法,线性时许逻辑算法等的验证和分析。并使用语言包含验证方法验证分析系统的属性模式,以评估主动防御应用于工业控制系统的有效性。