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

针对PLC等逻辑控制器控制连续对象的可靠性问题 ,给出了混合系统的形式验证的方法 ,即用混合矩形自动机建模 ,通过可达性分析 ,从而证明控制程序的正确性 ,最后结合化工过程控制中的应用实例做了说明。

混合系统的形式验证技术及其在化工过程控制中的应用

针对 PL C等逻辑控制器控制连续对象的可靠性问题 ,给出了混合系统的形式验证的方法 ,即用混合矩形自动机建模 ,通过其商迁移的可达性分析 ,证明了控制程序的正确性。应用实例表明该方法是可行和有效的。

基于矩形混杂自动机的交叉口建模及可达性分析

针对交通网络中交叉口车流具有连续时间特性,动态信号灯的切换具有离散事件特性的情况,以四相位单交叉口为对象,考虑车辆到达的随机性,以微分包含的形式描述车辆到达率,建立了一个四相位交叉口的矩形混杂自动机模型.该模型中以车辆排队长度为连续状态变量描述连续车流动态,以信号灯状态为离散状态变量描述离散信号灯动态.在该模型基础上,分析了交叉口各个方向的输入、输出车流动态,采用矩形混杂自动机可达性分析方法详细分析了车辆排队长度的可达集,使用CheckMate 3.6工具箱进行仿真.仿真结果表明了矩形混杂自动机模型和可达性分析方法的有效性,不仅能够刻画交叉口车流的动态混杂特性,而且能够验证信号灯配时方案对车流疏导是否有效,为信号灯配时设计提供一种检验方法.