基于UPPAAL的微電網(wǎng)產(chǎn)能組件建模方法

姜科 洪玫 趙鶴 張光蘭

摘 要：微電網(wǎng)是指由分布式電源、儲(chǔ)能裝置、能量轉(zhuǎn)換裝置、相關(guān)負(fù)荷監(jiān)控、保護(hù)裝置匯集而成的小型發(fā)配電系統(tǒng)。微電網(wǎng)的產(chǎn)能組件是微電網(wǎng)的重要組成部分，由于電源分布具有一定的隨機(jī)性且電源的穩(wěn)定性和時(shí)間相關(guān)聯(lián)，致使微電網(wǎng)的在不同運(yùn)行方式和場(chǎng)景下的供電可靠性存在差異。因此為了提高微電網(wǎng)的供電可靠性，亟須要對(duì)微電網(wǎng)產(chǎn)能組件建立一個(gè)穩(wěn)定可靠的模型以保證微電網(wǎng)供電的可靠性。從微電網(wǎng)為實(shí)時(shí)控制系統(tǒng)的角度出發(fā)，通過(guò)分析光伏、風(fēng)力發(fā)電等分布式電源建立相應(yīng)的數(shù)學(xué)模型，將UPPAAL對(duì)實(shí)時(shí)系統(tǒng)建模方法引入微電網(wǎng)產(chǎn)能組件的建模之中，建立起來(lái)了微電網(wǎng)光伏電源、風(fēng)力電源、水力電源的模型。最后通過(guò)將建立的模型的仿真結(jié)果與基于電磁暫態(tài)仿真軟件PSCAD/EMTDC的仿真結(jié)果對(duì)比，證明了該建模方法的正確性，同時(shí)建立的模型也能夠更加準(zhǔn)確的反應(yīng)實(shí)時(shí)系統(tǒng)的真實(shí)情況。該成果可以用于微電網(wǎng)可靠性的自動(dòng)化驗(yàn)證工作。

關(guān)鍵詞：微電網(wǎng)；組件建模；微電網(wǎng)建模；產(chǎn)能組件；形式化驗(yàn)證

中圖分類號(hào)：TP301.2 文獻(xiàn)標(biāo)識(shí)碼：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）

隨著現(xiàn)代化進(jìn)程的加快，傳統(tǒng)電網(wǎng)的弊端逐步顯現(xiàn)，微電網(wǎng)逐步走入人們的視線。為緩解傳統(tǒng)電網(wǎng)的供電壓力，微電網(wǎng)的概念被提出：微電網(wǎng)是一個(gè)小型的發(fā)電系統(tǒng)，由分布式電源、儲(chǔ)能設(shè)備、需求側(cè)負(fù)載和控制單位等組件構(gòu)成，微電網(wǎng)能夠分擔(dān)主電網(wǎng)的壓力，在主電網(wǎng)故障時(shí)為用戶提供可靠供電。在一些偏遠(yuǎn)地區(qū)和主電網(wǎng)無(wú)法到達(dá)的地區(qū)，微電網(wǎng)可以獨(dú)立運(yùn)行來(lái)滿足用戶的用電需求。

由于微電網(wǎng)具有并網(wǎng)和孤網(wǎng)兩種運(yùn)行方式，且由于產(chǎn)能組件（風(fēng)力發(fā)電、光伏發(fā)電）具有一定的隨機(jī)性，致使微電網(wǎng)在不同運(yùn)行方式和場(chǎng)景下供電的可靠性存在差異。為了更好地發(fā)揮微電網(wǎng)的作用，減少微電網(wǎng)的重構(gòu)的成本，在設(shè)計(jì)階段保證微電網(wǎng)的可靠性至關(guān)重要，為此微電網(wǎng)建模逐漸成為人們研究的焦點(diǎn)，建立一個(gè)恰當(dāng)?shù)奈㈦娋W(wǎng)模型可為后續(xù)的微電網(wǎng)的分析和可靠性論證提供基礎(chǔ)從而保證微電網(wǎng)的可靠性。產(chǎn)能組件作為微電網(wǎng)的關(guān)鍵部分，本文后面部分將重點(diǎn)關(guān)注微電網(wǎng)產(chǎn)能組件的建模。

2 相關(guān)工作介紹（Related work introduction）

現(xiàn)有的微電網(wǎng)建模方法包括：Almada JB[1]等人采用Matlab/Simulink構(gòu)建包含風(fēng)—光—儲(chǔ)的微電網(wǎng)的模型；Khalil[2]等人采用Simulink構(gòu)建光伏陣列和風(fēng)能系統(tǒng)產(chǎn)能組件模型，通過(guò)分布式控制策略在實(shí)現(xiàn)負(fù)載共享的情況下維持系統(tǒng)穩(wěn)定；賀繼勝[3]采用PSCAD工具構(gòu)建了包含風(fēng)力發(fā)電、光伏發(fā)電等產(chǎn)能組件的并網(wǎng)運(yùn)行的微電網(wǎng)整體模型，并對(duì)微電網(wǎng)運(yùn)行模式切換時(shí)的運(yùn)行情況進(jìn)行仿真。

上面的這些對(duì)微電網(wǎng)的建模方法都有各自的特點(diǎn)，在特定的方面也有自己的優(yōu)勢(shì)，但是不利于對(duì)系統(tǒng)的時(shí)間行為進(jìn)行分析和論證?；跁r(shí)間自動(dòng)機(jī)的建模方法是研究系統(tǒng)的時(shí)間行為的主流方法，UPPAAL[4]則是其中代表性的建模工具，是高效的實(shí)時(shí)系統(tǒng)建模驗(yàn)證工具[5]。本文首先分析了微電網(wǎng)的基本機(jī)構(gòu)，然后介紹了統(tǒng)計(jì)模型檢測(cè)技術(shù)和模型檢測(cè)工具UPPAAL的建模機(jī)制和特性，通過(guò)將UPPAAL引入微電網(wǎng)的建模之中，并結(jié)合微電網(wǎng)的數(shù)學(xué)模型構(gòu)建起了微電網(wǎng)產(chǎn)能組件模型，最后通過(guò)與基于電磁暫態(tài)仿真軟件PSCAD/EMTDC的砣磯島微電網(wǎng)的仿真結(jié)果相對(duì)比，證明UPPAAL用于微電網(wǎng)產(chǎn)能組件建模的正確性，最后總結(jié)了本文的工作并對(duì)未來(lái)的工作進(jìn)行了展望。

3 微電網(wǎng)結(jié)構(gòu)與UPPAAL建模概述（Overview of microgrid structure and UPPAAL modeling）

3.1 微電網(wǎng)基本結(jié)構(gòu)分析

一般情況下，微電網(wǎng)由分布式電源、儲(chǔ)能設(shè)備、需求側(cè)負(fù)載和控制單元等組件構(gòu)成，如圖1所示是微電網(wǎng)的基本結(jié)構(gòu)圖。

圖1 微電網(wǎng)基本結(jié)構(gòu)圖

Fig.1 Basic structure diagram of micro-grid

由圖1可以看出微電網(wǎng)主要由產(chǎn)能組件、儲(chǔ)能組件和需求負(fù)載組成，產(chǎn)能組件是微電網(wǎng)的重要組成部分，產(chǎn)能組件也叫分布式電源，為微電網(wǎng)提供能量來(lái)源，常用的產(chǎn)能組件包括風(fēng)力發(fā)電、光伏發(fā)電、水力發(fā)電、微型燃機(jī)和柴油發(fā)電機(jī)，產(chǎn)能組件是本文所要討論的重要部分。

3.2 實(shí)時(shí)控制系統(tǒng)與模型檢測(cè)工具UPPAAL

實(shí)時(shí)系統(tǒng)是一個(gè)非常寬泛的概念，通常指整個(gè)系統(tǒng)，其模型如圖2所示。該系統(tǒng)有一個(gè)決策部件，通過(guò)傳感器讀和計(jì)算機(jī)控制決策部件來(lái)與外界交互。決策部件過(guò)計(jì)算機(jī)傳感器傳來(lái)的數(shù)據(jù)在一定時(shí)間內(nèi)得出控制決策，并將狀態(tài)信息進(jìn)行存儲(chǔ)。IEEE（美國(guó)電氣電子工程師協(xié)會(huì)）定義實(shí)時(shí)系統(tǒng)為“那些正確性不僅取決于計(jì)算的邏輯結(jié)果，也取決于產(chǎn)生結(jié)果所花費(fèi)的時(shí)間的系統(tǒng)”。一般認(rèn)為，實(shí)時(shí)系統(tǒng)是指能夠?qū)?lái)自所控制的外部環(huán)境（物理過(guò)程）的交互作用做出及時(shí)響應(yīng)以達(dá)到預(yù)定目的的一種帶時(shí)間約束的計(jì)算機(jī)系統(tǒng)，是一種定量式的反應(yīng)系統(tǒng)，它被廣泛地應(yīng)用在許多工業(yè)領(lǐng)域里。

在實(shí)時(shí)系統(tǒng)中，某一種計(jì)算過(guò)程常常需要滿足一定的時(shí)間約束。時(shí)間自動(dòng)機(jī)是在有限自動(dòng)機(jī)的基礎(chǔ)上添加了時(shí)間約束產(chǎn)生的，從而可以處理實(shí)時(shí)系統(tǒng)。時(shí)間自動(dòng)機(jī)通過(guò)使用真值時(shí)鐘變量，提供了一個(gè)簡(jiǎn)單而全面的方法來(lái)表示有時(shí)間約束的狀態(tài)轉(zhuǎn)換圖，時(shí)間自動(dòng)機(jī)的所有時(shí)鐘在系統(tǒng)開始時(shí)從0開始計(jì)時(shí)，并以同樣的速率增加。每一次狀態(tài)的轉(zhuǎn)換都有可能復(fù)位一些時(shí)鐘。自動(dòng)機(jī)的控制放在一個(gè)狀態(tài)的命題屬性和時(shí)鐘滿足了相應(yīng)的通信約束的狀態(tài)里。通常，使用標(biāo)有事件標(biāo)記的狀態(tài)轉(zhuǎn)換圖對(duì)系統(tǒng)進(jìn)行建模。

UPPAAL是Uppsala大學(xué)和Aalborg大學(xué)共同開發(fā)的一個(gè)工具集，可用于實(shí)時(shí)系統(tǒng)的建模、仿真和驗(yàn)證。在UPPAAL中，系統(tǒng)被表示為一個(gè)包含變量、數(shù)據(jù)類型、同步信道，以及時(shí)間自動(dòng)機(jī)的模型。UPPAAL通過(guò)隨機(jī)自動(dòng)機(jī)網(wǎng)絡(luò)來(lái)描述系統(tǒng)行為，能夠彌補(bǔ)時(shí)間自動(dòng)機(jī)表達(dá)能力上的不足，構(gòu)建復(fù)雜的信息物理系統(tǒng)的動(dòng)態(tài)行為。UPPAAL適用于可以被描述為非確定的進(jìn)程所組成的集合的系統(tǒng)，每一個(gè)進(jìn)程被描述為由有限控制結(jié)構(gòu)、實(shí)數(shù)值時(shí)鐘和變量組成的時(shí)間自動(dòng)機(jī)，過(guò)程之間通過(guò)通道和共享變量來(lái)進(jìn)行通訊。典型的應(yīng)用包括實(shí)時(shí)控制，通訊協(xié)議特別是那些對(duì)時(shí)間要求較高的領(lǐng)域。

時(shí)間自動(dòng)機(jī)作為UPPAAL的基礎(chǔ)，它是具有離散輸入和輸出系統(tǒng)的一種數(shù)學(xué)模型，它可以直觀的刻畫實(shí)時(shí)系統(tǒng)與時(shí)間有關(guān)的行為。在對(duì)微電網(wǎng)進(jìn)行建模時(shí)，可以將微電網(wǎng)的控制系統(tǒng)考慮成為一個(gè)實(shí)時(shí)控制系統(tǒng)，因此采取UPPAAL對(duì)微電網(wǎng)的產(chǎn)能組件進(jìn)行建模、分析、論證是一條重要的路徑。

3.3 基于UPPAAL的微電網(wǎng)產(chǎn)能組件建模

產(chǎn)能組件的能量來(lái)源包括一些可再生能源和化石能源，可再生能源包括風(fēng)能、太陽(yáng)能、潮汐能等，化石能源包括柴油發(fā)電、燃料電池、天然氣等。產(chǎn)能組件為微電網(wǎng)提供能量來(lái)源，本節(jié)將對(duì)幾種常見的產(chǎn)能組件進(jìn)行建模，包括風(fēng)力渦輪機(jī)產(chǎn)能建模、光伏發(fā)電產(chǎn)能建模。

3.4 UPPAAL建模機(jī)制和方法

圖3中包含三個(gè)隨機(jī)時(shí)間自動(dòng)機(jī)A、B、T，隨機(jī)時(shí)間自動(dòng)機(jī)A和B中均包含兩個(gè)狀態(tài)，分別包含同步信號(hào)a！和b！，隨機(jī)時(shí)間自動(dòng)機(jī)T包含三個(gè)狀態(tài)和一個(gè)局部時(shí)鐘C，T0狀態(tài)下，C'==4表示時(shí)鐘的速率為4。在這個(gè)案例中，通過(guò)變量x<=1和y<=2控制同步信號(hào)a！和b！的觸發(fā)，a？和b？接收到同步信號(hào)進(jìn)入下一個(gè)狀態(tài)，直至到達(dá)T的最終狀態(tài)T3為止。

為了更好地闡述UPPAAL的建模體系，采用Train-Gate案例進(jìn)行說(shuō)明。Train-Gate是多列火車過(guò)橋的控制系統(tǒng)，由多列火車和一個(gè)控制器組成，火車的啟動(dòng)和停止均需一定的時(shí)間。如圖4所示一個(gè)火車的模板，Safe狀態(tài)沒有變量，定義了火車延遲的指數(shù)分布比率?；疖囇舆t由指數(shù)分布決定，然后通過(guò)控制器的同步信號(hào)讓appr[i]靠近。圖5模型中定義了一個(gè)有理數(shù)（1+id）/N2，其中id是火車的標(biāo)識(shí)符，N是火車的數(shù)量，火車的id越高到達(dá)的越快。圖5表示控制器，采用一個(gè)內(nèi)部隊(duì)列數(shù)據(jù)結(jié)構(gòu)對(duì)火車進(jìn)行記錄，利用函數(shù)對(duì)火車執(zhí)行入隊(duì)和出隊(duì)操作。

3.5 風(fēng)力發(fā)電建模

風(fēng)力發(fā)電是“風(fēng)能—機(jī)械能—電能”的一個(gè)轉(zhuǎn)換過(guò)程，該過(guò)程主要涉及風(fēng)力渦輪機(jī)、發(fā)電機(jī)，以及相應(yīng)的傳動(dòng)裝置。在風(fēng)力的作用下，風(fēng)力渦輪機(jī)葉片旋轉(zhuǎn)完成“風(fēng)能—機(jī)械能”的轉(zhuǎn)換；在傳動(dòng)裝置的作用下，風(fēng)力渦輪機(jī)帶動(dòng)發(fā)電機(jī)旋轉(zhuǎn)完成“機(jī)械能—電能”的轉(zhuǎn)換。風(fēng)力發(fā)電利用可再生能源，污染小，但具有一定的隨機(jī)性，在供電穩(wěn)定性方面需要進(jìn)一步提升。風(fēng)力發(fā)電的數(shù)學(xué)模型可以表示為[6]：

其中，P（v）表示風(fēng)力發(fā)電產(chǎn)生的電功率，單位是W；Vci表示切入風(fēng)速，Vco表示安全風(fēng)速，Vr表示額定風(fēng)速，單位是m/s；

Pr表示額定功率，單位是W；q（v）表示功率和風(fēng)速之間的非線性關(guān)系。為了便于數(shù)據(jù)的獲取，本文選擇多項(xiàng)式功率曲線表示功率和風(fēng)速之間的非線性關(guān)系，C1、C2和C3由切入風(fēng)速和額定風(fēng)速?zèng)Q定，可以通過(guò)如下公式計(jì)算得出：

風(fēng)力發(fā)電的UPPAAL模型如圖6所示，模型中包含三個(gè)狀態(tài)：Off、Limitation、Optimization，模型從Optimization狀態(tài)開始運(yùn)行，根據(jù)式（1），當(dāng)V>=Vco或者V=Vci且V=Vr且V

風(fēng)力發(fā)電模型中的實(shí)時(shí)風(fēng)速V通過(guò)函數(shù)模擬實(shí)時(shí)風(fēng)速，具體參數(shù)值A(chǔ)、B、hour_offset和day，以及指數(shù)分布可以根據(jù)實(shí)際情況進(jìn)行修改。

3.6 光伏發(fā)電建模

光伏發(fā)電的原理是通過(guò)太陽(yáng)能電池將光能轉(zhuǎn)化為電能，通常情況下，光伏發(fā)電系統(tǒng)包括太陽(yáng)能電池板、逆變器、控制器三部分。光伏發(fā)電系統(tǒng)容易安裝且無(wú)污染，可以就近為用戶供電。光伏發(fā)電的數(shù)學(xué)模型可以表示為：

其中，P表示光伏發(fā)電的輸出功率，G表示太陽(yáng)輻照度，PSTC表示太陽(yáng)能組件的額定功率，k表示功率溫度系數(shù)，Tc是太陽(yáng)能電池的溫度，TSTC是標(biāo)準(zhǔn)測(cè)試條件下的溫度，Ta為周圍環(huán)境溫度，TNOCT為正常工作的電池片溫度。標(biāo)準(zhǔn)測(cè)試條件是AM1.5時(shí)輻射度為1000W/m2組件溫度為25℃[7]。

光伏發(fā)電的UPPAAL模型如圖7所示，模型包含兩個(gè)狀態(tài)：initial和start，根據(jù)光學(xué)發(fā)電的數(shù)學(xué)模型將initial狀態(tài)下的狀態(tài)變量設(shè)置為若產(chǎn)生的太陽(yáng)輻照度小于等于0，使p_p=0并進(jìn)入start狀態(tài)，將狀態(tài)變量設(shè)置為p_p'==0，若太陽(yáng)輻照度T>0，再次進(jìn)入initial狀態(tài)。

光伏發(fā)電模型中的太陽(yáng)輻照度T和溫度Ta分別通過(guò)函數(shù) 模擬太陽(yáng)輻照度和溫度，具體參數(shù)值分別根據(jù)實(shí)際情況進(jìn)行設(shè)定。

4 UPPAAL建模有效性分析實(shí)驗(yàn)（UPPAAL modeling effectiveness analysis experiment）

本文的有效性分析實(shí)驗(yàn)旨在證明采用統(tǒng)計(jì)模型檢測(cè)工具UPPAAL構(gòu)建的微電網(wǎng)產(chǎn)能模型是有效的，本章采用UPPAAL工具構(gòu)建與參考文獻(xiàn)[3]相同環(huán)境的砣磯島微電網(wǎng)模型，對(duì)構(gòu)建好的微電網(wǎng)模型中各組件的輸出功率進(jìn)行仿真，并將仿真結(jié)果與參考文獻(xiàn)[3]中基于電磁暫態(tài)仿真軟件PSCAD/EMTDC的結(jié)果進(jìn)行對(duì)比，根據(jù)對(duì)比結(jié)果分析UPPAAL構(gòu)建的微電網(wǎng)產(chǎn)能組件模型的有效性，進(jìn)而證明基于UPPAAL構(gòu)建的微電網(wǎng)產(chǎn)能組件模型是有效的。

4.1 實(shí)驗(yàn)環(huán)境

硬件環(huán)境：

①CPU：Intel（R）_Core（TM）_i5-3337U

②RAM：4 GB

軟件環(huán)境：

①操作系統(tǒng)：Windows 10

②統(tǒng)計(jì)模型檢測(cè)工具：UPPAAL 4.1.19

4.2 實(shí)驗(yàn)對(duì)象

砣磯島微電網(wǎng)位于煙臺(tái)市長(zhǎng)島縣境內(nèi)，是我國(guó)在黃海地區(qū)建立的一個(gè)海島微電網(wǎng)，是一個(gè)鏈?zhǔn)降墓╇娤到y(tǒng)，主要用來(lái)保障島內(nèi)軍民、工業(yè)、海水淡化、海產(chǎn)養(yǎng)殖等活動(dòng)的可靠供電。砣磯島微電網(wǎng)基本結(jié)構(gòu)如圖8所示，主要包括風(fēng)力發(fā)電、光伏發(fā)電、柴油發(fā)電機(jī)、各類負(fù)載和儲(chǔ)能設(shè)備；其中，柴油發(fā)電機(jī)僅在孤網(wǎng)模式下運(yùn)行，并網(wǎng)模式下不運(yùn)行。

本文根據(jù)長(zhǎng)島地區(qū)的風(fēng)速、日照和溫度的歷史數(shù)據(jù)，通

過(guò)函數(shù)模擬風(fēng)速（A=random（30），B=random（20））、太陽(yáng)輻照度（A=random（1000），B=random（200））和環(huán)境溫度（A=random（40），B=random（10）），day=24*3600s，使生成風(fēng)速、太陽(yáng)輻照度和環(huán)境溫度基本滿足一般情況。砣磯島微電網(wǎng)中，三臺(tái)風(fēng)力發(fā)電機(jī)相連，發(fā)電機(jī)組的額定功率為750kW，切入風(fēng)速為3.5—4m/s，額定風(fēng)速為14m/s，切出風(fēng)速為25m/s；光伏發(fā)電的總?cè)萘繛?00kW；柴油發(fā)電機(jī)的同步發(fā)電機(jī)組的額定輸出功率為1000kVA，額定轉(zhuǎn)速為3000r/min；鉛酸蓄電池系統(tǒng)的功率為2MW，容量為2MW·h，放電功率為100kW，充電功率為400kW；微電網(wǎng)平均總負(fù)載為2400kW，所以本文令需求側(cè)負(fù)載的限定值L=400kW[8]。

本實(shí)驗(yàn)采用砣磯島微電網(wǎng)作為實(shí)驗(yàn)對(duì)象，分別對(duì)并網(wǎng)運(yùn)行的無(wú)儲(chǔ)能和包含儲(chǔ)能的砣磯島微電網(wǎng)進(jìn)行實(shí)驗(yàn)。

4.3 實(shí)驗(yàn)設(shè)計(jì)

為了分析采用UPPAAL構(gòu)建的產(chǎn)能組件模型的有效性，本文設(shè)計(jì)了一個(gè)仿真對(duì)比試驗(yàn)，采用UPPAAL工具分別對(duì)并網(wǎng)砣磯島產(chǎn)能組件輸出功率進(jìn)行仿真，并將仿真結(jié)果與參考文獻(xiàn)[3]中基于電磁暫態(tài)仿真工具PSCAD/EMTDC的結(jié)果進(jìn)行對(duì)比。為了保證對(duì)比結(jié)果的正確性，實(shí)驗(yàn)在同環(huán)境下進(jìn)行。具體實(shí)驗(yàn)步驟如下：

（1）采用UPPAAL構(gòu)建與參考文獻(xiàn)[3]中相同環(huán)境的砣磯島微電網(wǎng)的產(chǎn)能組件模型，主要是并網(wǎng)的無(wú)儲(chǔ)能/包含儲(chǔ)能的砣磯島微電網(wǎng)產(chǎn)能組件模型。

（2）采用UPPAAL對(duì)上述微電網(wǎng)模型中產(chǎn)能組件的輸出功率進(jìn)行仿真，得到對(duì)應(yīng)情況下的仿真結(jié)果；將得到的仿真結(jié)果與基于PSCAD/EMTDC的仿真結(jié)果進(jìn)行對(duì)比，分析對(duì)比結(jié)果。

4.4 仿真對(duì)比

分別構(gòu)建并網(wǎng)的無(wú)儲(chǔ)能和包含儲(chǔ)能的砣磯島微電網(wǎng)產(chǎn)能組件的UPPAAL模型，采用UPPAAL工具對(duì)產(chǎn)能組件的輸出功率進(jìn)行仿真，得到的仿真結(jié)果如圖9和圖10所示。其中，Pw表示風(fēng)力發(fā)電的輸出功率、Ppv表示光伏發(fā)電的輸出功率、單位均為MW。如圖11和圖12為參考文獻(xiàn)[3]中得出的無(wú)儲(chǔ)能和包含儲(chǔ)能的并網(wǎng)微電網(wǎng)中各組件的輸出功率的仿真結(jié)果。

對(duì)圖9—圖12對(duì)比比可以發(fā)現(xiàn)，UPPAAL中雖然具有仿真功能，但并不是專業(yè)的仿真軟件，且仿真時(shí)間較短，所以導(dǎo)致圖10的仿真曲線相比專業(yè)的仿真軟件的仿真曲線而言平滑度較差。但是仿真過(guò)程中主要的數(shù)據(jù)值和數(shù)據(jù)走勢(shì)基本一致。

以圖9和圖10為例：1s時(shí)風(fēng)力發(fā)電機(jī)和光伏發(fā)電開始工作并逐步上升到最大輸出功率，經(jīng)歷0.6s的暫態(tài)過(guò)程之后，二者均趨于穩(wěn)定，1.6s—3s二者的Pw、Ppv的值均相同；3s開始二者風(fēng)力發(fā)電的輸出功率均有所下降，在第4s時(shí)下降至1.5MW左右，并在4s開始上升，在第5s時(shí)恢復(fù)到穩(wěn)定狀態(tài)；4s開始二者的光伏發(fā)電的輸出功率均有所下降，然后在4.5s左右開始上升并趨于穩(wěn)定值0.3MW；微電網(wǎng)與主電網(wǎng)之間的交換功率Pct均在3s開始上升，然后在4.5s左右達(dá)到最高點(diǎn)然后下降，并在5s開始趨于穩(wěn)定。通過(guò)上述的數(shù)據(jù)值和走勢(shì)分析，可以說(shuō)明UPPAAL構(gòu)建的模型的是有效的。

綜合考慮上述的仿真對(duì)比結(jié)果，雖然UPPAAL仿真結(jié)果相比專業(yè)仿真軟件的平滑度較差，但是基本數(shù)據(jù)點(diǎn)和變化趨勢(shì)基本一致，可以說(shuō)明UPPAAL構(gòu)建的產(chǎn)能組件模型是有效的。

5 結(jié)論（Conclusion）

本文通過(guò)對(duì)微電網(wǎng)和統(tǒng)計(jì)模型檢測(cè)技術(shù)的研究，提出了一種基于UPPAAL的微電網(wǎng)產(chǎn)能組件建模的方法，并對(duì)建模的結(jié)果的有效性進(jìn)行了論證。

（1）構(gòu)建了微電網(wǎng)中產(chǎn)能組件的UPPAAL模型，包括風(fēng)力發(fā)電、光伏發(fā)電、水力發(fā)電的模型；通過(guò)與基于PSCAD/EMTDC的砣磯島微電網(wǎng)中各組件輸出功率的仿真對(duì)比，從而論證了UPPAAL建模的有效性。

（2）根據(jù)仿真分析結(jié)果，對(duì)微電網(wǎng)的設(shè)計(jì)有如下建議：微電網(wǎng)設(shè)計(jì)和構(gòu)建過(guò)程中應(yīng)綜合考慮各類分布式電源的優(yōu)缺點(diǎn)，如考慮可再生能源的隨機(jī)性問(wèn)題、柴油發(fā)電機(jī)的環(huán)保問(wèn)題等。

但是本文在基于統(tǒng)計(jì)模型檢測(cè)的微電網(wǎng)可靠性驗(yàn)證過(guò)程中仍然存在一些問(wèn)題，需要進(jìn)一步的研究和解決，在構(gòu)建產(chǎn)能組件模型時(shí)，通過(guò)函數(shù)生成部分模擬數(shù)據(jù)（如風(fēng)速、太陽(yáng)輻照度、環(huán)境溫度），使其盡可能符合實(shí)際情況，但只考慮了一般情況下的變化。下一步需要優(yōu)化數(shù)據(jù)生成方法，以覆蓋特殊情況下的值的變化。

參考文獻(xiàn)（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] 賀繼勝.可再生能源微電網(wǎng)的建模與控制[D].廣東工業(yè)大學(xué)，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] 代聲馨，洪玫，郭兵，等.多處理器實(shí)時(shí)系統(tǒng)可調(diào)度性分析的UPPAAL模型[J].軟件學(xué)報(bào)，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] 邱丹驊.可再生能源海島電網(wǎng)的多能源協(xié)調(diào)控制策略研究[D].華中科技大學(xué)，2013.

作者簡(jiǎn)介：

姜 科（1994-），男，碩士生.研究領(lǐng)域：軟件形式化驗(yàn)證，軟件分析與測(cè)試.

洪 玫（1963-），女，碩士，教授.研究領(lǐng)域：軟件工程，軟件自動(dòng)化測(cè)試.

趙 鶴（1992-），女，碩士.研究領(lǐng)域：軟件自動(dòng)化測(cè)試，模型檢測(cè).

張光蘭（1994-），女，碩士生.研究領(lǐng)域：軟件自動(dòng)化測(cè)試，GUI測(cè)試.