基于UPPAAL的微电网产能组件建模方法
2018-12-21姜科洪玫赵鹤张光兰
姜科 洪玫 赵鹤 张光兰
摘 要：微电网是指由分布式电源、储能装置、能量转换装置、相关负荷监控、保护装置汇集而成的小型发配电系统。微电网的产能组件是微电网的重要组成部分，由于电源分布具有一定的随机性且电源的稳定性和时间相关联，致使微电网的在不同运行方式和场景下的供电可靠性存在差异。因此为了提高微电网的供电可靠性，亟须要对微电网产能组件建立一个稳定可靠的模型以保证微电网供电的可靠性。从微电网为实时控制系统的角度出发，通过分析光伏、风力发电等分布式电源建立相应的数学模型，将UPPAAL对实时系统建模方法引入微电网产能组件的建模之中，建立起来了微电网光伏电源、风力电源、水力电源的模型。最后通过将建立的模型的仿真结果与基于电磁暂态仿真软件PSCAD/EMTDC的仿真结果对比，证明了该建模方法的正确性，同时建立的模型也能够更加准确的反应实时系统的真实情况。该成果可以用于微电网可靠性的自动化验证工作。
关键词：微电网；组件建模；微电网建模；产能组件；形式化验证
中图分类号：TP301.2 文献标识码：A
Abstract：Micro-grid refers to the distributed generators，energy storage devices，energy conversion devices，related load monitoring，protection devices brought together to form a small-scale distribution system，in which the production components are an important part of the micro-grid.Due to the randomness of the power distribution and the relevance between the stability of power supply and the time，there are differences in the reliability of the micro-grid in different operation modes and conditions.Therefore，in order to improve the reliability of the power supply，it is imperative to establish a stable and reliable model of the production components to ensure the reliability of the micro-grid power supply.From the perspective of micro-grid as a real-time control system，the corresponding mathematical model is established by analyzing distributed power sources such as photovoltaic power and wind power generation.UPPAAL is introduced into the modeling of micro-grid production components by modeling the real-time system to build models of photovoltaic power，wind power，hydraulic power.Finally，the simulation results of the established models are compared with the simulation results based on PSCAD/ EMTDC electromagnetic transient simulation software to prove the correctness of the modeling method，and the model can also more accurately reflect the real situation of the real-time system.The results can be used to verify the reliability of micro grid.
Keywords：micro-grid；component modeling；micro-grid modeling；production components；formal verification
1 引言（Introduction）
隨着现代化进程的加快，传统电网的弊端逐步显现，微电网逐步走入人们的视线。为缓解传统电网的供电压力，微电网的概念被提出：微电网是一个小型的发电系统，由分布式电源、储能设备、需求侧负载和控制单位等组件构成，微电网能够分担主电网的压力，在主电网故障时为用户提供可靠供电。在一些偏远地区和主电网无法到达的地区，微电网可以独立运行来满足用户的用电需求。
由于微电网具有并网和孤网两种运行方式，且由于产能组件（风力发电、光伏发电）具有一定的随机性，致使微电网在不同运行方式和场景下供电的可靠性存在差异。为了更好地发挥微电网的作用，减少微电网的重构的成本，在设计阶段保证微电网的可靠性至关重要，为此微电网建模逐渐成为人们研究的焦点，建立一个恰当的微电网模型可为后续的微电网的分析和可靠性论证提供基础从而保证微电网的可靠性。产能组件作为微电网的关键部分，本文后面部分将重点关注微电网产能组件的建模。
2 相关工作介绍（Related work introduction）
现有的微电网建模方法包括：Almada JB[1]等人采用Matlab/Simulink构建包含风—光—储的微电网的模型；Khalil[2]等人采用Simulink构建光伏阵列和风能系统产能组件模型，通过分布式控制策略在实现负载共享的情况下维持系统稳定；贺继胜[3]采用PSCAD工具构建了包含风力发电、光伏发电等产能组件的并网运行的微电网整体模型，并对微电网运行模式切换时的运行情况进行仿真。
上面的这些对微电网的建模方法都有各自的特点，在特定的方面也有自己的优势，但是不利于对系统的时间行为进行分析和论证。基于时间自动机的建模方法是研究系统的时间行为的主流方法，UPPAAL[4]则是其中代表性的建模工具，是高效的实时系统建模验证工具[5]。本文首先分析了微电网的基本机构，然后介绍了统计模型检测技术和模型检测工具UPPAAL的建模机制和特性，通过将UPPAAL引入微电网的建模之中，并结合微电网的数学模型构建起了微电网产能组件模型，最后通过与基于电磁暂态仿真软件PSCAD/EMTDC的砣矶岛微电网的仿真结果相对比，证明UPPAAL用于微电网产能组件建模的正确性，最后总结了本文的工作并对未来的工作进行了展望。
3 微电网结构与UPPAAL建模概述（Overview of microgrid structure and UPPAAL modeling）
3.1 微电网基本结构分析
一般情况下，微电网由分布式电源、储能设备、需求侧负载和控制单元等组件构成，如图1所示是微电网的基本结构图。
图1 微电网基本结构图
Fig.1 Basic structure diagram of micro-grid
由图1可以看出微电网主要由产能组件、储能组件和需求负载组成，产能组件是微电网的重要组成部分，产能组件也叫分布式电源，为微电网提供能量来源，常用的产能组件包括风力发电、光伏发电、水力发电、微型燃机和柴油发电机，产能组件是本文所要讨论的重要部分。
3.2 实时控制系统与模型检测工具UPPAAL
实时系统是一个非常宽泛的概念，通常指整个系统，其模型如图2所示。该系统有一个决策部件，通过传感器读和计算机控制决策部件来与外界交互。决策部件过计算机传感器传来的数据在一定时间内得出控制决策，并将状态信息进行存储。IEEE（美国电气电子工程师协会）定义实时系统为“那些正确性不仅取决于计算的逻辑结果，也取决于产生结果所花费的时间的系统”。一般认为，实时系统是指能够对来自所控制的外部环境（物理过程）的交互作用做出及时响应以达到预定目的的一种带时间约束的计算机系统，是一种定量式的反应系统，它被广泛地应用在许多工业领域里。
在实时系统中，某一种计算过程常常需要满足一定的时间约束。时间自动机是在有限自动机的基础上添加了时间约束产生的，从而可以处理实时系统。时间自动机通过使用真值时钟变量，提供了一个简单而全面的方法来表示有时间约束的状态转换图，时间自动机的所有时钟在系统开始时从0开始计时，并以同样的速率增加。每一次状态的转换都有可能复位一些时钟。自动机的控制放在一个状态的命题属性和时钟满足了相应的通信约束的状态里。通常，使用标有事件标记的状态转换图对系统进行建模。
UPPAAL是Uppsala大学和Aalborg大学共同开发的一个工具集，可用于实时系统的建模、仿真和验证。在UPPAAL中，系统被表示为一个包含变量、数据类型、同步信道，以及时间自动机的模型。UPPAAL通过随机自动机网络来描述系统行为，能够弥补时间自动机表达能力上的不足，构建复杂的信息物理系统的动态行为。UPPAAL适用于可以被描述为非确定的进程所组成的集合的系统，每一个进程被描述为由有限控制结构、实数值时钟和变量组成的时间自动机，过程之间通过通道和共享变量来进行通讯。典型的应用包括实时控制，通讯协议特别是那些对时间要求较高的领域。
时间自动机作为UPPAAL的基础，它是具有离散输入和输出系统的一种数学模型，它可以直观的刻画实时系统与时间有关的行为。在对微电网进行建模时，可以将微电网的控制系统考虑成为一个实时控制系统，因此采取UPPAAL对微电网的产能组件进行建模、分析、论证是一条重要的路径。
3.3 基于UPPAAL的微电网产能组件建模
产能组件的能量来源包括一些可再生能源和化石能源，可再生能源包括风能、太阳能、潮汐能等，化石能源包括柴油发电、燃料电池、天然气等。产能组件为微电网提供能量来源，本节将对几种常见的产能组件进行建模，包括风力涡轮机产能建模、光伏发电产能建模。
3.4 UPPAAL建模机制和方法
图3中包含三个随机时间自动机A、B、T，随机时间自动机A和B中均包含两個状态，分别包含同步信号a！和b！，随机时间自动机T包含三个状态和一个局部时钟C，T0状态下，C'==4表示时钟的速率为4。在这个案例中，通过变量x<=1和y<=2控制同步信号a！和b！的触发，a？和b？接收到同步信号进入下一个状态，直至到达T的最终状态T3为止。
为了更好地阐述UPPAAL的建模体系，采用Train-Gate案例进行说明。Train-Gate是多列火车过桥的控制系统，由多列火车和一个控制器组成，火车的启动和停止均需一定的时间。如图4所示一个火车的模板，Safe状态没有变量，定义了火车延迟的指数分布比率。火车延迟由指数分布决定，然后通过控制器的同步信号让appr[i]靠近。图5模型中定义了一个有理数（1+id）/N2，其中id是火车的标识符，N是火车的数量，火车的id越高到达的越快。图5表示控制器，采用一个内部队列数据结构对火车进行记录，利用函数对火车执行入队和出队操作。
3.5 风力发电建模
风力发电是“风能—机械能—电能”的一个转换过程，该过程主要涉及风力涡轮机、发电机，以及相应的传动装置。在风力的作用下，风力涡轮机叶片旋转完成“风能—机械能”的转换；在传动装置的作用下，风力涡轮机带动发电机旋转完成“机械能—电能”的转换。风力发电利用可再生能源，污染小，但具有一定的随机性，在供电稳定性方面需要进一步提升。风力发电的数学模型可以表示为[6]：
其中，P（v）表示风力发电产生的电功率，单位是W；Vci表示切入风速，Vco表示安全风速，Vr表示额定风速，单位是m/s；
Pr表示额定功率，单位是W；q（v）表示功率和风速之间的非线性关系。为了便于数据的获取，本文选择多项式功率曲线表示功率和风速之间的非线性关系，C1、C2和C3由切入风速和额定风速决定，可以通过如下公式计算得出：
风力发电的UPPAAL模型如图6所示，模型中包含三个状态：Off、Limitation、Optimization，模型从Optimization状态开始运行，根据式（1），当V>=Vco或者V 风力发电模型中的实时风速V通过函数模拟实时风速，具体参数值A、B、hour_offset和day，以及指数分布可以根据实际情况进行修改。 3.6 光伏发电建模 光伏发电的原理是通过太阳能电池将光能转化为电能，通常情况下，光伏发电系统包括太阳能电池板、逆变器、控制器三部分。光伏发电系统容易安装且无污染，可以就近为用户供电。光伏发电的数学模型可以表示为： 其中，P表示光伏发电的输出功率，G表示太阳辐照度，PSTC表示太阳能组件的额定功率，k表示功率温度系数，Tc是太阳能电池的温度，TSTC是标准测试条件下的温度，Ta为周围环境温度，TNOCT为正常工作的电池片温度。标准测试条件是AM1.5时辐射度为1000W/m2组件温度为25℃[7]。 光伏发电的UPPAAL模型如图7所示，模型包含两个状态：initial和start，根据光学发电的数学模型将initial状态下的状态变量设置为若产生的太阳辐照度小于等于0，使p_p=0并进入start状态，将状态变量设置为p_p'==0，若太阳辐照度T>0，再次进入initial状态。 光伏发电模型中的太阳辐照度T和温度Ta分别通过函数 模拟太阳辐照度和温度，具体参数值分别根据实际情况进行设定。 4 UPPAAL建模有效性分析实验（UPPAAL modeling effectiveness analysis experiment） 本文的有效性分析实验旨在证明采用统计模型检测工具UPPAAL构建的微电网产能模型是有效的，本章采用UPPAAL工具构建与参考文献[3]相同环境的砣矶岛微电网模型，对构建好的微电网模型中各组件的输出功率进行仿真，并将仿真结果与参考文献[3]中基于电磁暂态仿真软件PSCAD/EMTDC的结果进行对比，根据对比结果分析UPPAAL构建的微电网产能组件模型的有效性，进而证明基于UPPAAL构建的微电网产能组件模型是有效的。 4.1 实验环境 硬件环境： ①CPU：Intel（R）_Core（TM）_i5-3337U ②RAM：4 GB 软件环境： ①操作系统：Windows 10 ②统计模型检测工具：UPPAAL 4.1.19 4.2 实验对象 砣矶岛微电网位于烟台市长岛县境内，是我国在黄海地区建立的一个海岛微电网，是一个链式的供电系统，主要用来保障岛内军民、工业、海水淡化、海产养殖等活动的可靠供电。砣矶岛微电网基本结构如图8所示，主要包括风力发电、光伏发电、柴油发电机、各类负载和储能设备；其中，柴油发电机仅在孤网模式下运行，并网模式下不运行。 本文根据长岛地区的风速、日照和温度的历史数据，通 过函数模拟风速（A=random（30），B=random（20））、太阳辐照度（A=random（1000），B=random（200））和环境温度（A=random（40），B=random（10）），day=24*3600s，使生成风速、太阳辐照度和环境温度基本满足一般情况。砣矶岛微电网中，三台风力发电机相连，发电机组的额定功率为750kW，切入风速為3.5—4m/s，额定风速为14m/s，切出风速为25m/s；光伏发电的总容量为300kW；柴油发电机的同步发电机组的额定输出功率为1000kVA，额定转速为3000r/min；铅酸蓄电池系统的功率为2MW，容量为2MW·h，放电功率为100kW，充电功率为400kW；微电网平均总负载为2400kW，所以本文令需求侧负载的限定值L=400kW[8]。 本实验采用砣矶岛微电网作为实验对象，分别对并网运行的无储能和包含储能的砣矶岛微电网进行实验。 4.3 实验设计 为了分析采用UPPAAL构建的产能组件模型的有效性，本文设计了一个仿真对比试验，采用UPPAAL工具分别对并网砣矶岛产能组件输出功率进行仿真，并将仿真结果与参考文献[3]中基于电磁暂态仿真工具PSCAD/EMTDC的结果进行对比。为了保证对比结果的正确性，实验在同环境下进行。具体实验步骤如下： （1）采用UPPAAL构建与参考文献[3]中相同环境的砣矶岛微电网的产能组件模型，主要是并网的无储能/包含储能的砣矶岛微电网产能组件模型。 （2）采用UPPAAL对上述微电网模型中产能组件的输出功率进行仿真，得到对应情况下的仿真结果；将得到的仿真结果与基于PSCAD/EMTDC的仿真结果进行对比，分析对比结果。
4.4 仿真对比
分别构建并网的无储能和包含储能的砣矶岛微电网产能组件的UPPAAL模型，采用UPPAAL工具对产能组件的输出功率进行仿真，得到的仿真结果如图9和图10所示。其中，Pw表示风力发电的输出功率、Ppv表示光伏发电的输出功率、单位均为MW。如图11和图12为参考文献[3]中得出的无储能和包含储能的并网微电网中各组件的输出功率的仿真结果。
对图9—图12对比比可以发现，UPPAAL中虽然具有仿真功能，但并不是专业的仿真软件，且仿真时间较短，所以导致图10的仿真曲线相比专业的仿真软件的仿真曲线而言平滑度较差。但是仿真过程中主要的數据值和数据走势基本一致。
以图9和图10为例：1s时风力发电机和光伏发电开始工作并逐步上升到最大输出功率，经历0.6s的暂态过程之后，二者均趋于稳定，1.6s—3s二者的Pw、Ppv的值均相同；3s开始二者风力发电的输出功率均有所下降，在第4s时下降至1.5MW左右，并在4s开始上升，在第5s时恢复到稳定状态；4s开始二者的光伏发电的输出功率均有所下降，然后在4.5s左右开始上升并趋于稳定值0.3MW；微电网与主电网之间的交换功率Pct均在3s开始上升，然后在4.5s左右达到最高点然后下降，并在5s开始趋于稳定。通过上述的数据值和走势分析，可以说明UPPAAL构建的模型的是有效的。
综合考虑上述的仿真对比结果，虽然UPPAAL仿真结果相比专业仿真软件的平滑度较差，但是基本数据点和变化趋势基本一致，可以说明UPPAAL构建的产能组件模型是有效的。
5 结论（Conclusion）
本文通过对微电网和统计模型检测技术的研究，提出了一种基于UPPAAL的微电网产能组件建模的方法，并对建模的结果的有效性进行了论证。
（1）构建了微电网中产能组件的UPPAAL模型，包括风力发电、光伏发电、水力发电的模型；通过与基于PSCAD/EMTDC的砣矶岛微电网中各组件输出功率的仿真对比，从而论证了UPPAAL建模的有效性。
（2）根据仿真分析结果，对微电网的设计有如下建议：微电网设计和构建过程中应综合考虑各类分布式电源的优缺点，如考虑可再生能源的随机性问题、柴油发电机的环保问题等。
但是本文在基于统计模型检测的微电网可靠性验证过程中仍然存在一些问题，需要进一步的研究和解决，在构建产能组件模型时，通过函数生成部分模拟数据（如风速、太阳辐照度、环境温度），使其尽可能符合实际情况，但只考虑了一般情况下的变化。下一步需要优化数据生成方法，以覆盖特殊情况下的值的变化。
参考文献（References）
[1] Almada JB，Leao RPS，Montenegro FFD，et al.Modeling and simulation of a microgrid with multiple energy resources[C].EUROCON，2013 IEEE，2013：1150-1157.
[2] Khalil A，Alfaitori KA，Asheibi A.Modeling and Control of PV/Wind Microgrid[C].The International Renewable Energy Congress Irec，2016.
[3] 贺继胜.可再生能源微电网的建模与控制[D].广东工业大学，2014.
[4] David A，Larsen KG，Legay A，et al.Uppaal SMC tutorial[J].International Journal on Software Tools for Technology Transfer，2015，17（4）：397-415.
[5] 代声馨，洪玫，郭兵，等.多处理器实时系统可调度性分析的UPPAAL模型[J].软件学报，2015（2）：279-296.
[6] Carrillo C，Monta?o AFO，Cidrás J，et al.Review of power curve modelling for wind turbines[J].Renewable & Sustainable Energy Reviews，2013，21（5）：572-581.
[7] Hellman HP，Koivisto M，Lehtonen M.Photovoltaic power generation hourly modelling[M].2014：269-272.
[8] 邱丹骅.可再生能源海岛电网的多能源协调控制策略研究[D].华中科技大学，2013.
作者简介：
姜 科（1994-），男，硕士生.研究领域：软件形式化验证，软件分析与测试.
洪 玫（1963-），女，硕士，教授.研究领域：软件工程，软件自动化测试.
赵 鹤（1992-），女，硕士.研究领域：软件自动化测试，模型检测.
张光兰（1994-），女，硕士生.研究领域：软件自动化测试，GUI测试.
