站场电动放空阀控制逻辑的形式化建模与验证  

Formal modeling and verification of control logic for electric vent valve in station

作　　者：董秀娟 赵浩羽 徐宝昌[2] 周裕东 董长锁 赵正开 DONG Xiujuan;ZHAO Haoyu;XU Baochang;ZHOU Yudong;DONG Changsuo;ZHAO Zhengkai(PipeChina Beijing Pipeline Co.,Ltd.,Beijing 100101,China;College of Information Science and Engineering,China University of Petroleum in Beijing,Beijing 102249,China)

机构地区：[1]国家管网集团北京管道有限公司,北京100101 [2]中国石油大学(北京)信息科学与工程学院,北京102249

出　　处：《现代电子技术》2023年第17期155-162,共8页Modern Electronics Technique

基　　金：国家石油天然气管网集团有限公司科学研究与技术开发项目(Y180022KY01KF0330004)。

摘　　要：在油气管道控制系统典型逻辑标准编制的早期,对拟标准化控制逻辑的建模与验证能够提前发现设计缺陷,有助于提高控制系统的功能完整性与安全性,进而避免因控制逻辑设计失误导致的危险事故发生。根据形式化验证方法中模型检验的原理,利用时间自动机及其验证工具UPPAAL,对天然气站场电动放空阀通用控制逻辑开展形式化建模与验证,将逻辑图中的各类功能组件以及阀门动作流程独立建模,用于刻画完整的控制逻辑操作过程,综合验证结果发现,阀门的“开”“关”切换逻辑存在设计缺陷。最后,通过反例分析给出合理的优化方案,优化后的验证结果表明,优化方案能够满足控制系统功能完整性与安全性需求,形式化方法为管道站控系统控制逻辑可靠性验证提供了一个全新的技术路径。In the early stage of the compilation of typical logic standards for oil and gas pipeline control systems,the design defects of the modeling and verification of quasi⁃standardized control logic can be found in advance,which is helpful to improve the functional integrity and safety of the control systems,and then avoid dangerous accidents caused by control logic design errors.According to the principle of model checking in the formal verification method,the timed automata and its verification tool UPPAAL are used to carry out formal modeling and verification of the general control logic of the electric vent valve in the natural gas station.The various functional blocks and the valve action process in the logic diagram are independently modeled to describe the complete control logic operation process.The results of comprehensive verification show that there are design defects in the″open″and″close″switching logic of the valve.Finally,a reasonable optimization scheme by counter⁃example analysis is given.The verification results show that the optimized scheme can meet the functional integrity and safety requirements of the control systems,and the formal method can provide a new technical path for the reliability verification of the control logic of the pipeline station control systems.

关 键 词：油气管道 控制逻辑 形式化方法 时间自动机 UPPAAL 形式化验证方法 

分 类 号：TN876.3-34[电子电信—信息与通信工程]