常压炉加热系统形式建模的验证  

Modeling and formal verification of atmospheric pressure oven heating system

作　　者：刘震[1,2] 方敏[1] 罗来豹[1] 李加良[1] 

机构地区：[1]合肥工业大学电气与自动化工程学院,安徽合肥230009 [2]中国科学院固体物理研究所,安徽合肥230031

出　　处：《合肥工业大学学报（自然科学版）》2010年第10期1501-1505,共5页Journal of Hefei University of Technology：Natural Science

摘　　要：文章运用基于流管道的混合动态系统形式验证方法,解决了常压炉加热系统工艺参数的验证问题;通过对常压炉加热系统的运行机理进行分析并建立混合自动机模型,应用状态可达集的过近似方法计算近似流管道;通过对近似流管道的分析,验证常压炉加热系统设定的燃料流量是否满足生产工艺要求;经多次验证,最终得到了燃料流量的取值范围。In this paper,formal verification of hybrid systems based on flow pipe is applied to verify the process parameters of the atmospheric pressure oven heating system.Firstly,the production process of the atmospheric pressure oven heating system is analyzed.Then the hybrid automaton of the atmospheric pressure oven heating system is constructed and the verification tool PHAVer is used to compute the reachable sets of the automaton by the flow pipe approximation method.And formal verification is carried out based on flow pipe approximation to testify whether the proposed fuel flow satisfies production process requirements.Following a mass of verification,parameter ranges of fuel flow are finally obtained.

关 键 词：形式验证 常压炉 混合系统 混合自动机 

分 类 号：TP301[自动化与计算机技术—计算机系统结构] TP15[自动化与计算机技术—计算机科学与技术]