逻辑控制器的形式验证及其应用

　　1　简　介

　　近年来,对设备自动化和系统集成的程度的要求越来越高,使得控制工程师不得不面对规模和复杂程度不断增加的复杂系统。微型计算机和微处理器的迅速发展并在实际中的大量应用,推动了新型数字控制器不断涌现。在现代过程工业中,大量采用PLC和DCS。当数字控制装置与模拟量的对象打交道时所出现的现象需要很好地分析和理解,同时需要保障控制程序的正确性和操作安全。由于目前现有的软件工具只能检查控制程序中的逻辑错误,而对物理对象的控制是否符合要求则无能为力,所以大多数情况下对这类逻辑控制系统的正确性和安全性问题,需要依靠编程者的实际经验和大量的仿真运行来分析,缺乏比较合适可信的验证工具。

　　随着混合系统的形式验证技术的发展,为现代工业过程逻辑控制程序的验证问题提供了新的手段。混合系统是连续变量过程和离散事件过程并存且相互交换信息的动态系统。在化工过程控制等应用中,运行于控制系统上的软件的主体是执行逻辑控制函数;即使软件的主体是连续控制,程序往往还包括故障紧急处理和运行模式的切换等;并且受控物理对象中包含了大量的离散元件,如阀门、开关、继电器,以及用于安全监督的传感器等。可以说,这类系统的控制,是混合系统控制的典型实例。

　　混合系统的形式验证技术不象仿真方法,每次只能产生特定初始条件和输入信号的一条轨迹,即使进行大量耗时耗力的多次仿真,其完备性也难以从理论上得到保障,因而可信度较低。混合系统的形式验证技术是通过穷举算法对系统进行可达分析:在一次运行中,给定初始状态和输入信号的集合后,模型检查系统的每一种可能行为,来证明所有的可达状态是否满足预定的规范,从而为控制程序的可靠性提供了科学分析。

　　2　混合系统的形式验证技术

　　混合系统形式验证技术的原理是用计时混合矩形自动机对控制系统建模,利用仿真对(Bisimu-lation)原理,将原系统的可达性分析转化为其商迁移系统的可达性分析,从而大大降低了计算量,使全空间搜索成为可能。

　　2.1　迁移系统(Transition Systems)

　　定义(迁移系统):一般迁移系统是一个集合:

　　T = (S, ,→S0,SF)

　　其中:

　　S———状态集合;———事件的字母表;→ S× ×S———迁移关系;S0 S———初始状态的集合;SF S———终止状态集合。定义(等价关系):称某个关系~ S×S是等价的,如果满足:

　　①自反性:对于所有的s,有(s,s)∈~;

　　②对称性:若有(s,s′)∈~,则有(s′,s)∈~;

　　③传递性:若(s,s′)∈~和(s′,s″)∈~,则(s,s″)∈~。