形式化方法在电网信息物理系统中的应用

doi:10.11930/j.issn.1004-9649.202007008

中国电力 ›› 2021, Vol. 54 ›› Issue (3): 31-37.DOI: 10.11930/j.issn.1004-9649.202007008

• 国家“十三五”智能电网重大专项专栏：（六）先进计算与人工智能技术专栏 • 上一篇下一篇

形式化方法在电网信息物理系统中的应用

黄莉^1,2, 梁云^1,2, 黄辉^1,2, 赵若涵³

1. 全球能源互联网研究院有限公司，北京 102209;
2. 国家电网公司电力智能传感技术及应用联合实验室，北京 102209;
3. 国网电力科学研究院实验验证中心，江苏南京 210032

收稿日期:2020-07-10 修回日期:2020-10-30 出版日期:2021-03-05 发布日期:2021-03-17
作者简介:黄莉(1986-)，女，通信作者，硕士，高级工程师，从事电力信息通信及传感技术研究，E-mail：huangli@geiri.sgcc.com.cn
基金资助:
国家重点研发计划资助项目(电网信息物理系统分析与控制的基础理论与方法，2017YFB0903000)

Application of Formal Methods in Power Grid Cyber Physical Systems

HUANG Li^1,2, LIANG Yun^1,2, HUANG Hui^1,2, ZHAO Ruohan³

1. Global Energy Interconnection Research Institute Co., Ltd., Beijing 102209, China;
2. Laboratory of Electric Power Intelligent Sensing Technology and Application, Beijing 102209, China;
3. State Grid Electric Power Research Institute, Nanjing 210032, China

Received:2020-07-10 Revised:2020-10-30 Online:2021-03-05 Published:2021-03-17
Supported by:
This work is supported by the National Key Research and Development Program of China(Basic Theories and Methods of Analysis and Control of the Cyber Physical Systems for Power Grid, No.2017YFB0903000)

摘要/Abstract

摘要： 电网信息物理系统中的嵌入式终端不仅要具备常规的信息交互能力，还要在资源约束条件下，满足测控的实时性要求。面向规模庞大的复杂系统，需要引入形式化方法验证其可靠性。通过分析形式化方法在电网信息物理系统中的应用，设计实现一种适用于电网信息物理系统中嵌入式系统信息交互过程分析的形式化方法及模型检验软件工具，并结合实际案例详细分析模型检验工具的应用过程。实际案例表明，形式化方法可以缩小从高层设计到代码实现的距离，提高产品的可靠性，模型检验软件工具能够对当前嵌入式装置规模和复杂度快速增长带来的可靠性保障问题提供可参考的解决方案。

关键词: 电网信息物理系统, 形式化方法, 资源约束, 信息交互, 模型检验

Abstract: The embedded terminals in the power grid cyber physical systems need to not only have the ability of information interaction, but also meet the real-time requirements of measurement and control under resource constraints. It is necessary to introduce formal methods to verify the reliability of complex systems with large scale. This paper analyzes the application of formal methods in power grid cyber physical systems, designs and realizes a formal method and model checking software tool for analyzing the information interaction process of embedded system in the power grid cyber physical systems. The application process of the model checking tool is analyzed in detail through a practical case, and the application results show that the formal method can shorten the distance from high level design to code implementation and improve the reliability of the products. The model checking software tool can provide a reference solution to the reliability assurance problem caused by the rapid increase of embedded devices in terms of scale and complexity.

Key words: power grid cyber physical systems, formal method, resource constraints, information interaction, model checking

黄莉, 梁云, 黄辉, 赵若涵. 形式化方法在电网信息物理系统中的应用[J]. 中国电力, 2021, 54(3): 31-37.

HUANG Li, LIANG Yun, HUANG Hui, ZHAO Ruohan. Application of Formal Methods in Power Grid Cyber Physical Systems[J]. Electric Power, 2021, 54(3): 31-37.

导出引用管理器 EndNote|Ris|BibTeX

链接本文: https://www.electricpower.com.cn/CN/10.11930/j.issn.1004-9649.202007008

https://www.electricpower.com.cn/CN/Y2021/V54/I3/31

参考文献

[1] 张广泉. 形式化方法导论[M]. 北京: 清华大学出版社, 2015.
[2] 刘东, 盛万兴, 王云, 等. 电网信息物理系统的关键技术及其进展[J]. 中国电机工程学报, 2015, 35(14): 3522-3531
LIU Dong, SHENG Wanxing, WANG Yun, et al. Key technologies and trends of cyber physical system for power grid[J]. Proceedings of the CSEE, 2015, 35(14): 3522-3531
[3] 刘林, 张运洲, 王雪, 等. 能源互联网目标下电力信息物理系统深度融合发展研究[J]. 中国电力, 2019, 52(1): 2-9
LIU Lin, ZHANG Yunzhou, WANG Xue, et al. Research on deep integration of power cyber physical system under energy Internet goals[J]. Electric Power, 2019, 52(1): 2-9
[4] 梁云, 黄莉, 侯兴哲, 等. 配电网CPS的通信需求和网络资源分配方案探讨[J]. 中国电力, 2019, 52(1): 32-39
LIANG Yun, HUANG Li, HOU Xingzhe, et al. Discussion on communication requirement and network resource allocation scheme of cyber physical system for distribution network[J]. Electric Power, 2019, 52(1): 32-39
[5] 中国科学技术协会. 2017-2018中国计算机科学技术发展报告[R]. 北京: 中国科学技术协会, 2019.
[6] 李婉璐. 软件工程中的形式化方法研究综述[J]. 数字技术与应用, 2015(10): 108-109
[7] 张连怡. 构件系统模型检测方法研究[D]. 北京: 清华大学, 2015.
ZHANG Lianyi. Model checking of component-based systems[D]. Beijing: Tsinghua University, 2015.
[8] 彭飞, 张涛, 王金双, 等. 计算机系统形式化验证中的模型检测方法综述[J]. 军事通信技术, 2016, 37(2): 38-42, 76
PENG Fei, ZHANG Tao, WANG Jinshuang, et al. Overview of model checking methods in computer system formal verification[J]. Journal of Military Communications Technology, 2016, 37(2): 38-42, 76
[9] 魏欧, 石玉峰, 徐丙凤, 等. 软件模型检测中的抽象模型研究综述[J]. 计算机研究与发展, 2015, 52(7): 1580-1603
WEI Ou, SHI Yufeng, XU Bingfeng, et al. Abstract modeling formalisms in software model checking[J]. Journal of Computer Research and Development, 2015, 52(7): 1580-1603
[10] 侯刚, 周宽久, 勇嘉伟, 等. 模型检测中状态爆炸问题研究综述[J]. 计算机科学, 2013, 40(增刊1): 77-86, 111
HOU Gang, ZHOU Kuanjiu, YONG Jiawei, et al. Survey of state explosion problem in model checking[J]. Computer Science, 2013, 40(S1): 77-86, 111
[11] 陈志, 高阳阳, 朱彦沛, 等. 基于局部偏序规约的控制器局域网模型验证方法: CN103888462A[P]. 2014-06-25.
[12] 谢健, 阚双龙, 黄志球, 等. 嵌入偏序约简的状态事件线性时序逻辑验证[J]. 计算机学报, 2019, 42(10): 2145-2159
XIE Jian, KAN Shuanglong, HUANG Zhiqiu, et al. State/event linear temporal logic verification with the integration of partial order reduction[J]. Chinese Journal of Computers, 2019, 42(10): 2145-2159
[13] 单来祥, 覃征, 卢欣晔, 等. 线性时序逻辑转换Büchi自动机的按需即时算法[J]. 清华大学学报(自然科学版), 2014, 54(2): 281-288
SHAN Laixiang, QIN Zheng, LU Xinye, et al. On-the-fly translation algorithm from linear temporal logic to Büchi automata[J]. Journal of Tsinghua University (Science and Technology), 2014, 54(2): 281-288
[14] 朱晨曦. 基于AADL的信息物理融合系统的分析与设计方法[D]. 广州: 广东工业大学, 2014.
ZHU Chenxi. The analysis and design method of cyber-physical system based on AADL[D]. Guangzhou: Guangdong University of Technology, 2014.
[15] 钱磊. 信息物理融合系统的形式化建模与讨论[D]. 上海: 华东师范大学, 2013.
QIAN Lei. Research on modeling of cyber-physical systems[D]. Shanghai: East China Normal University, 2013.
[16] 孙守卿. 基于模型检测工具SPIN的安全协议分析和验证[D]. 兰州: 兰州大学, 2006.
SUN Shouqing. Security protocol analysis and verification based on model checker SPIN[D]. Lanzhou: Lanzhou University, 2006.
[17] 代声馨, 洪玫, 郭兵, 等. 多处理器实时系统可调度性分析的UPPAAL模型[J]. 软件学报, 2015, 26(2): 279-296
DAI Shengxin, HONG Mei, GUO Bing, et al. Schedulability analysis model for multiprocessor real-time systems using UPPAAL[J]. Journal of Software, 2015, 26(2): 279-296
[18] 凌万水, 刘东, 洪俊, 等. 形式化校验技术在智能配电网自愈中的应用[J]. 电力系统自动化, 2012, 36(18): 62-66
LING Wanshui, LIU Dong, HONG Jun, et al. Formal verification technology application in self-healing of smart distribution grid[J]. Automation of Electric Power Systems, 2012, 36(18): 62-66
[19] 何建伟, 姚淑珍. 基于Petri网的状态机变迁的形式化方法研究[C]// 第十一届全国Petri网理论与应用学术年会. 2007.
[20] 陈伟伟, 吕盼, 纪凤坤, 等. 基于多维度检测与Petri网的变电站接地故障风险评估[J]. 电力系统保护与控制, 2019, 47(23): 152-159
CHEN Weiwei, LÜ Pan, JI Fengkun, et al. Risk assessment of substation grounding fault based on multidimensional detection and Petri net[J]. Power System Protection and Control, 2019, 47(23): 152-159
[21] 白海洋, 李静, 赵娜. 基于时间自动机的嵌入式软件模型可调度性验证[J]. 计算机工程与科学, 2013, 35(3): 121-127
BAI Haiyang, LI Jing, ZHAO Na. Schedulability validation of embedded software model based on time automaton[J]. Computer Engineering & Science, 2013, 35(3): 121-127
[22] 熊海军, 王晓辉, 朱永利, 等. IEC61850智能电子设备交互实时性建模与验证[J]. 电力系统自动化, 2014, 38(19): 90-95, 121
XIONG Haijun, WANG Xiaohui, ZHU Yongli, et al. Modeling and verification of real-time interaction for IEC 61850 intelligent electronic device[J]. Automation of Electric Power Systems, 2014, 38(19): 90-95, 121

形式化方法在电网信息物理系统中的应用

Application of Formal Methods in Power Grid Cyber Physical Systems

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 4

编辑推荐

Metrics

[1]	冯宝成, 金震, 侯炜, 徐光福. 花瓣型配电网区域备自投系统控制策略优化研究及应用[J]. 中国电力, 2024, 57(1): 244-254.
[2]	麻吕斌, 郝一浩, 薛利, 李彬, 祁兵, 陈宋宋. 一种基于改进型THP编码的需求响应信息传输优化方法[J]. 中国电力, 2022, 55(10): 201-208.
[3]	吴英俊, 范婷婷, 徐昊, 倪明. 考虑天气影响的配电信息物理系统可靠性评估[J]. 中国电力, 2020, 53(4): 59-68.
[4]	王宇飞, 邱健, 李俊娥. 考虑攻击损益的电网CPS场站级跨空间连锁故障早期预警方法[J]. 中国电力, 2020, 53(1): 92-99.

模态框（Modal）标题

形式化方法在电网信息物理系统中的应用

Application of Formal Methods in Power Grid Cyber Physical Systems

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 4

编辑推荐

Metrics