汽轮机控制保护系统形式化建模及安全性分析

摘要：随着科学技术的发展，发电装备智能化的程度正处于持续提升的阶段，进而促使汽轮机控制保护系统与网络技术的结合愈加紧密。与此同时，在汽轮机系统安全性研究中，一系列的网络攻击引起了社会各界的广泛讨论与关注，也掀起了汽轮机网络安全的研究热潮。本文分别探讨了汽轮机控制保护系统形式化建模以及相应的安全性，为该方向的研究提供了具体的路径。

关键词：汽轮机；控制保护系统；形式化建模；安全性

引言：汽轮机控制保护系统的形式化建模与安全性的分析，可以使用刻画逻辑准确、过程描述完整的形式化方法创建全新的汽轮机控制保护系统模型，有关单位能够利用标签转移系统模型揭示形式化方法中活性特性与系统控制保护逻辑间的内在联系。与此同时，还要对汽轮机控制保护系统安全性的不足进行深入的掌握和改革，进而保证对汽轮机实际运行过程中逻辑的合理性以及结果的准确性。

1 汽轮机控制保护系统形式化建模

汽轮机控制保护系统包括电液调速系统（DEH）、监测系统（TSI）和保护系统（ETS）。对该系统的形式化建模需要采用UML统一建模语言，应用Petri网方法和时间自动机方法。

1.1 UML统一建模语言

UML是一种用来对密集型系统进行可视化建模、为面向对象开发系统的产品进行说明、可视化和编制文档的通用语言。针对目标系统的不同特性，UML中定义了类图、用例图、状态图、对象图、协作图、活动图、时序图、构件图以及部署图等9种不同视图来描述这些特性。

统一建模语言融入了软件工程领域的新思想、新方法和新技术，使软件设计人员沟通更简明，进一步缩短了设计时间，降低开发成本。它的应用范围很宽，可以应用于软件开发、数据库、嵌入式开发等领域。其特点是具有通俗性、统一性、图示性，动态模型与静态模型相结合，缺点是语义不明确且视图间存在冗余，可能会导致信息不一致。因此，UML最适于数据建模，业务建模，对象建模，组件建模。

1.2 Petri网描述方法

Petri网是一种针对离散并行系统的数学描述方法。Petri网的描述功能强大，由库所、变迁、令牌和弧等四部分组成，用图形化符号来描述变迁间的因果关系。此外，它还引入了并发的概念，是一种更适合于描述现代物理理论或异步、并发计算机系统的模型描述方法。

作为一种图形化和数学化的建模工具，Petri网广泛应用于自动化和计算机等领域，用于描述系统各状态变化和状态之间的迁移关系，能够对系统的顺序、结构、同步、异步等行为进行精准的描述。其优点是直观易懂，操作简单，能描述并发系统，但是其缺点是所建立的模型容易变得很大，不适用于复杂大型系统建模，而且所建的模型没有时间的概念，这就没有办法满足实时系统建模。

1.3 时间自动机

自动机是一种数学理论，它把结构、功能和关系置于一个离散的数学系统之上作为研究对象，通过一系列基本符号描述系统的进程。自动机可以分为有限自动机、线性有界自动机、图灵机等，而且可以对这些基本自动机结构进行拓补交换，依据不同系统的特点形成不同的自动机。

时间自动机在传统的有限状态自动机基础上增加了时钟约束。系统可以包含多个时钟，这些时间在执行时都是同时开始的，并且速度一致。添加了时钟约束时，只有在所给条件满足且在时钟约束范围内，才会发生从当前状态到下一状态的“跳转”。时间自动机的优点是能够对大型复杂的逻辑系统进行建模，又具有表达时间的能力，缺点是它解决问题的范围有限。

2 汽轮机控制保护系统的安全性和活性

每个系统都有其自身独特的功能，汽轮机控制保护系统也不例外，通过对汽轮机控制保护系统的研究可知，控制保护逻辑正是实现功能的载体。因此，对汽轮机控制保护逻辑的刻画对于系统的安全性研究而言，显得尤为重要。

通过进一步地的研究，可以发现安全性和活性作为形式化方法中两项最基本的属性，对于汽轮机控制保护逻辑问题的研究，具有重要意义。它们的一般性定义为：安全性，某些行为在系统中不会发生。活性，规定一些行为在系统中必须发生。

2.1 安全性的定义

在形式化方法中，安全性的定义是“坏的事情”不会发生；活性的形式化定义是“好的事情”一定会发生。而在汽轮机控制保护逻辑中，控制逻辑是为了保证汽轮机能够按照额定转速进行转动；保护逻辑则是为了阻止汽轮机在故障情况下继续转动。结合活性和安全性的定义，控制逻辑要实现的预期目标，实际上就是活性中的“好的事情”，而故障或者保护系统失常的情况则指的是安全性中“坏的事情”。因此，控制保护逻辑完整性的问题就转化为形式化模型中活性的完整性问题。因为时间自动机更重视对转移过程的描述，而安全性和活性作为一种特性，用该方法进行描述是不合适的。而标签转移系统与时间自动机系统语句形式相似，但更需要注重对系统特性的阐明和描述。

2.2 活性的定义

对于活性完整性的检测问题，已经提出了一种基于仿真的分布式系统活性推导方法，该方法主要分为两类，一类基于扩展模拟关系，由已知系统的活性进行扩展推导；而另一类则是基于演绎方法，使用图解法进行推导验证。同时，又提供了一种基于公平性的时序逻辑方法，该方法将时间与一阶逻辑相结合，可以有效地对系统的安全性和活性进行建模与验证。存在性、可推导性及持久性三个证明规则，并且通过对具体事例中活性完整性的证明来说明规则的有效性。为了描述混合动力系统中活性的自动否定问题，给出一个新属性的定义：“如果一个系统死了，那么它就永远不会再活了”，并根据“死性”提出了一种针对非线性混合动力系统活性完整性的验证算法。

定义的死性可否定系统中活性的完整性，即死性存在，则活性必不存在，而关于系统死性是否存在是通过对某些安全性的证明来实现的。因为活性和死性本质上属于互斥特性，那么我们对活性完整性的证明，也可以尝试对安全性的证明来实现。

3 结束语

综上所述，汽轮机控制保护系统对于汽轮机行业的进步与发展至关重要，通过围绕汽轮机控制保护系统的形式化建模与安全性分析展开研究，借助时间自动机的方法对由主汽阀和调节阀组成的控制系统，在很大程度上实现安全性能的提升和保护，使其在运行过程中愈加的安全、稳定，进而保证汽轮机行业的发展能够推动我国相关行业的不断进步。

参考文献：

[1]陶冶.汽轮机系统能耗分析与结构优化研究[D].武汉:华中科技大学, 2015.

[2]刘振亚.智能电网技术[M].第1版.北京:中国电力出版社,2016.

[3]聂雨.大型燃煤发电机组汽轮机系统仿真建模与变工况特性研究[D].武汉:华中科技大学, 2014.

[4]雷傲宇,刘蔚,周剑等.极端情况下电网遭受外部攻击的风险评估模型探索[J].广东电力,2022,35(08):50-59.

[5]高景斌.核电汽轮机控制保护系统设计及样机研制[J].自动化仪表,2021,42(S1):74-77.