姜科 洪玫 趙鶴 張光蘭

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

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

中圖分類號：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）

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

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

2 相關工作介紹（Related work introduction）

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

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

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

3.1 微電網(wǎng)基本結構分析

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

圖1 微電網(wǎng)基本結構圖

Fig.1 Basic structure diagram of micro-grid

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

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

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

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

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

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

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

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

3.4 UPPAAL建模機制和方法

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

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

3.5 風力發(fā)電建模

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

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

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

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

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

3.6 光伏發(fā)電建模

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

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

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

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

4 UPPAAL建模有效性分析實驗（UPPAAL modeling effectiveness analysis experiment）

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

4.1 實驗環(huán)境

硬件環(huán)境：

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

②RAM：4 GB

軟件環(huán)境：

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

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

4.2 實驗對象

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

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

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

本實驗采用砣磯島微電網(wǎng)作為實驗對象，分別對并網(wǎng)運行的無儲能和包含儲能的砣磯島微電網(wǎng)進行實驗。

4.3 實驗設計

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

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

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

4.4 仿真對比

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

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

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

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

5 結論（Conclusion）

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

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

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

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

參考文獻（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è)大學，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] 代聲馨，洪玫，郭兵，等.多處理器實時系統(tǒng)可調(diào)度性分析的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] 邱丹驊.可再生能源海島電網(wǎng)的多能源協(xié)調(diào)控制策略研究[D].華中科技大學，2013.

作者簡介：

姜 科（1994-），男，碩士生.研究領域：軟件形式化驗證，軟件分析與測試.

洪 玫（1963-），女，碩士，教授.研究領域：軟件工程，軟件自動化測試.

趙 鶴（1992-），女，碩士.研究領域：軟件自動化測試，模型檢測.

張光蘭（1994-），女，碩士生.研究領域：軟件自動化測試，GUI測試.