标题：蒸汽锅炉安全联锁系统的形式化验证
作者：程晶晶 王莉 孔力
作者单位：华中科技大学控制科学与工程系（430074）
关键字：蒸汽锅炉，安全联锁，形式化验证，符号模型检验
摘要：蒸汽锅炉实时控制系统一股用于控制炉内水位，使其保持在特定的范围内。为了加强环保和生产安全，蒸汽锅炉实时控制系统等过程控制中的有关场所要设置监测报警及安全联锁系统，所以其安全联锁系统的验证也非常重要。本文采用形式化验证工具SMV（符号模型检验），根据比较安全联锁系统的输入输出是否符合安全联锁规范，检验蒸汽锅炉安全联锁系统设计的规范性。