催化裂化分馏系统的信息安全需求分析与形式化验证研究.pdf

华中科技大学硕士学位论文

摘要

催化裂化分馏系统作为国家石油炼化上下游产业链的重要环节，保障其安全稳

定运行对国民经济稳步增长至关重要。随着工业互联网和信息化技术在炼化企业的

大范围推广，催化裂化分馏系统的生产效率和自动化水平大幅度提高，但同时也将传

统信息系统的信息安全威胁引入了之前相对封闭的工业控制系统环境中。为了避免

或缓解网络攻击对系统在实际运行过程中产生的危害影响，亟需在系统运行前开展

信息安全验证。本文针对分馏系统的信息安全需求验证不完备，以及形式化模型缺乏

结合对象业务行为的问题，提出了一种融合系统理论过程分析和有色Petri网的信息

安全验证方法。本文从如下三个方面展开深入研究：

（1）为了解决传统安全需求分析方法难以获取全面的催化裂化分馏系统信息安

全需求的问题，从系统层级综合考虑功能性故障和控制-数据不安全交互，通过系统

理论过程分析方法生成完备的表征催化裂化分馏系统行为的信息安全需求，为形式

化验证提供规约基础。

（2）针对现有形式化建模方法无法精准地描述催化裂化分馏系统的行为机理和

功能逻辑的问题，提出了基于有色Petri网的形式化建模方法，该方法通过分析分层

控制结构模型与CPN模型的转换规则，利用CPNTools建模工具构建催化裂化分馏

系统控制行为的分层CPN模型。在此基础上注入典型的攻击行为，构建催化裂化分

馏系统威胁场景的分层CPN模型，为形式化验证提供模型基础。

（3）结合催化裂化分馏系统的信息安全需求和形式化模型，构建安全验证CPN

模型，设计有无攻击下的催化裂化分馏系统的控制行为的对比实验场景，结合模型的

状态空间验证结果、安全验证结果和动态模拟仿真结果，对系统的控制行为进行安全

性分析。验证结果反映了所提安全验证方案的可行性和有效性，且该方案有助于后续

工业控制系统的事前安全分析，并为安全防护设计提供了理论支撑。

关键词：催化裂化分馏系统；信息安全；需求分析；有色Petri网；形式化验证

I

华中科技大学硕士学位论文

Abstract

Asacrucialelementinthenationalpetroleumrefiningindustrychain,thefluid

catalyticcracking(FCC)fractionationsystemplaysavitalroleinensuringitssafeandstable

operation,whichisessentialforthesteadygrowthofthenationaleconomy.Withthe

widespreadpromotionofIndustrialInternetandinformationtechnologyintherefining

industry,theproductionefficiencyandautomationleveloftheFCCfractionationsystem

havebeensignificantlyimproved.However,thecyber-securitythreatsoftraditional

informationsystemshavebeenintroducedintothepreviouslyrelativelyclosedindustrial

controlsystemenvironment.Inordertoavoidoralleviatetheharmfuleffectsofcyber-

attacksonthesystemduringactualoperation,itisurgentlynecessarytoconductsecurity

verificationbeforethesystemruns.Thisthes