混合系统的形式验证技术及其在化工过程控制中的应用
42 浏览量
2021-01-15
14:50:16
上传
评论
收藏 176KB PDF 举报
第 16 卷 第 2 期
V ol. 16 N o . 2
控 制 与 决 策
CON TR OL A N D DE CIS I ON
2001 年 3 月
M a r. 2001
文章编号: 1001-0920( 2001) 02-0203-04
混合系统的形式验证技术及其
在化工过程控制中的应用
张学军, 谢剑英, 张苗苗
( 上海交通大学 自动化系, 上海 200030)
摘 要: 针 对
PL C
等逻辑控制 器控制连续 对象的可 靠性问题, 给出了 混合系统的 形式验证 的方法, 即
用混合矩形自动机建模, 通过其商迁移的可 达性分析, 证明了控制程序的正确性。应用实例表明该 方法
是可行和有效的。
关键词: 混合系统; 矩形自动机; 形式验证; 可达性
中图分类号: T P 301 文献标识码:
A
Formal Verif ication of Hybrid Systems and
Its Application on Chemical Process Control
ZH A N G X ue-j un, X I E J ian-y ing, ZH A NG M iao-miao
( Depar tment of A utom atio n, Shang hai Jiao tong U niv ersity , Shang hai 200030, China)
Abstract: A iming at r eliability of pr ogra mmable log ic co nt ro ller for continuo us plants, an appr oach is
pr esented to make the hy brid systems
′
fo rma l ver ificat ion
.
T he mo del is g iven out by using hy brid rect-
ang ular auto mata a nd t he analy sis o f its quo tient tr ansitio n system′s r eachability is present ed. T he prin-
ciples o f ver ificat ion ar e given. T he method is illustr ated by an exam ple of chemical pro cess contr ol.
Key words
:
hy brid systems
;
r ectangular auto mata
;
formal verification
;
r eachability
1 引 言
现代工业已大量采用可编程逻辑控制器和计算
机分布式控制系统。当数字控制装置与模拟量的对
象打交道时, 应很好地分析和理解所出现的现象, 同
时也应保障控制程序的正确性和操作安全性。由于
现有的软件工具只能检查控制程序中的逻辑错误,
而对物理对象的控制是否符合要求则无能为力, 因
此对于这类逻辑控制系统的正确性和安全性问题,
大多依靠编程者的实际经验和大量的仿真运行进行
分析, 缺乏比较合适可信的验证工具。
近年来, 混合系统的形式验证技术获得了丰硕
的研究成果, 为现代工业过程逻辑控制程序的验证
提供了新的手段。混合系统是连续变量过程和离散
事件过程并存且相互交换信息的动态系统。在化工
过程控制等应用中, 运行于控制系统的软件的主体
是执行逻辑控制函数。即使软件的主体是连续控制,
其程序也往往包括故障紧急处理和运行模式的切换
等, 且受控对象中包含大量的离散元件( 如阀门、开
关、继电器、传感器等) 。可以说, 这类系统是混合系
收稿日期: 1999-08-20; 修回日期: 2000-02-14
作者简介: 张学军( 1972—) , 男, 河北滦南 人, 博 士生, 从事混合 系统的分析与 控制等研究; 谢剑英( 1940—) , 男, 福建龙岩
人, 教授, 博士生导师, 从事复杂工业过程控制、智能控制等研究。
资源评论
