王永亮 李立生 樊迪 劉 聰 王坦坦

摘? 要： 由于傳統(tǒng)方法對電壓型配電自動(dòng)化的動(dòng)作過程的分析缺乏嚴(yán)格的數(shù)學(xué)定義與模型驗(yàn)證，導(dǎo)致結(jié)論保守或者不完備。為了解決這個(gè)問題，使用模型檢測的方法實(shí)現(xiàn)對其動(dòng)作過程的分析，提出一個(gè)用于電壓型配電自動(dòng)化的分析模板，通過時(shí)間自動(dòng)機(jī)理論建立形式化模型，并使用模型工具uppaal對其動(dòng)作過程建模與性質(zhì)驗(yàn)證。仿真結(jié)果能夠驗(yàn)證所述模型的活性、正確性和平滑性。通過對模型的科學(xué)驗(yàn)證，證明電壓型配電自動(dòng)化在配網(wǎng)自動(dòng)化建設(shè)上具有重要意義。

關(guān)鍵詞： 配電自動(dòng)化; 時(shí)間自動(dòng)機(jī); uppaal; 模型驗(yàn)證; 模型實(shí)現(xiàn)過程; 故障隔離

中圖分類號： TN99?34; TM76? ? ? ? ? ? ? ? ? ? ?文獻(xiàn)標(biāo)識碼： A? ? ? ? ? ? ? ? ? ? ? 文章編號： 1004?373X（2020）03?0138?04

Modeling and simulation of voltage?matched power

distribution automation based on uppaal

WANG Yongliang1， LI Lisheng2， FAN Di2， LIU Cong1， WANG Tantan1

（1. Shandong University of Technology， Zibo 255000， China;

2. State Grid Shandong Electric Power Company Electric Power Research Institute， Jinan 250002， China）

Abstract： Due to the lack of strict mathematical definition and model verification in the analysis of action process of voltage?matched power distribution automation by traditional methods， the conclusions obtained are conservative or incomplete. In view of this， the model detection method is used to analyze the action process. An analysis template for voltage?matched power distribution automation is proposed， which creates a formalized model by the theory of time automata， and performs modeling and property verification for the action process by the modeling tool uppaal. The simulation results can verify the activity， correctness and smoothness of the said model. The scientific verification of the model proves the importance of voltage?matched power distribution automation in the construction of distribution automation.

Keywords： power distribution automation; time automata; uppaal; model detection; model implementation process; fault isolation