基于UPPAAL的微電網產能組件建模方法

姜科 洪玫 趙鶴 張光蘭

摘 要：微電網是指由分布式電源、儲能裝置、能量轉換裝置、相關負荷監控、保護裝置匯集而成的小型發配電系統。微電網的產能組件是微電網的重要組成部分，由于電源分布具有一定的隨機性且電源的穩定性和時間相關聯，致使微電網的在不同運行方式和場景下的供電可靠性存在差異。因此為了提高微電網的供電可靠性，亟須要對微電網產能組件建立一個穩定可靠的模型以保證微電網供電的可靠性。從微電網為實時控制系統的角度出發，通過分析光伏、風力發電等分布式電源建立相應的數學模型，將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狀態沒有變量，定義了火車延遲的指數分布比率?；疖囇舆t由指數分布決定，然后通過控制器的同步信號讓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=Vci且V=Vr且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測試.