【精彩论文】形式化方法在电网信息物理系统中的应用

观点凝练

摘要：电网信息物理系统中的嵌入式终端不仅要具备常规的信息交互能力，还要在资源约束条件下，满足测控的实时性要求。面向规模庞大的复杂系统，需要引入形式化方法验证其可靠性。通过分析形式化方法在电网信息物理系统中的应用，设计实现一种适用于电网信息物理系统中嵌入式系统信息交互过程分析的形式化方法及模型检验软件工具，并结合实际案例详细分析模型检验工具的应用过程。实际案例表明，形式化方法可以缩小从高层设计到代码实现的距离，提高产品的可靠性，模型检验软件工具能够对当前嵌入式装置规模和复杂度快速增长带来的可靠性保障问题提供可参考的解决方案。
结论：本文基于电网信息物理系统典型应用场景，从理论层面研究其嵌入式终端及系统的形式化建模需求，设计实现了一种适用于电网信息物理系统中嵌入式系统信息交互过程分析的形式化方法及模型检验软件工具，并针对智能变电站场景中的双网互校逻辑过程开展应用验证。形式化的模型检验方法特别适用于电网信息物理系统的应用场景，能够有效验证信息交互过程能否满足性能需求。本文采用的线性时序逻辑（LTL）描述嵌入式装置或交互过程需验证的性质，并对LTL进行扩展，可以描述相关的设备、环境特性，采用结合LTL和Petri网的方法，对系统模型的特性进行检测。本文设计的软件工具实现了交互协议的建模和模型检验，并提供可视化界面，将逻辑验证的结果用基于Petri网的可达图形式展示，能够直观判断反例的执行轨迹。实际案例表明，形式化方法可以缩小从高层设计到代码实现的距离，为嵌入式装置规模和复杂度快速增长带来的可靠性保障问题提供可参考的解决方案。针对模型检验场景固定，难以表示具体性能指标的问题，后续将进一步研究在系统运行阶段用实测参数对模型进行调整，完成综合验证。

引文信息

黄莉, 梁云, 黄辉, 等. 形式化方法在电网信息物理系统中的应用[J]. 中国电力, 2021, 54(3): 31-37.HUANG Li, LIANG Yun, HUANG Hui, et al. Application of formal methods in power grid cyber physical systems[J]. Electric Power, 2021, 54(3): 31-37.

 往期回顾 

编辑：杨彪

审核：方彤

声明

根据国家版权局最新规定，纸媒、网站、微博、微信公众号转载、摘编《中国电力》编辑部的作品，转载时要包含本微信号名称、二维码等关键信息，在文首注明《中国电力》原创。个人请按本微信原文转发、分享。欢迎大家转载分享。