形式验证中近似流管道的算法研究  

Algorithm research on flow pipe approximation of formal verification

作　　者：罗来豹[1] 方敏[1] 刘震[1] 

机构地区：[1]合肥工业大学电气与自动化工程学院,安徽合肥230009

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

摘　　要：混合系统形式验证技术是分析在给定的初始条件下,系统的可达集是否都在目标状态集合内。计算可达集是混合系统形式验证中的重要一步,选用何种几何体表示可达集对于整个验证精度有决定性的影响。文章对有向矩形壳和凸多面体2种状态可达集近似表示方法进行了分析比较,结合2种方法的优点提出了流管道过近似混合算法以降低保守性和提高运算速度;最后在Matlab环境下实现了混合算法并且验证了1个分段非线性系统实例,验证结果显示了所提混合算法的有效性。Formal verification of hybrid system analyzes whether the reachable sets of system are in target state sets in the case of given initial conditions.Computing reachable sets is an important step in formal verification of hybrid system.The geometry chosen to represent reachable sets has a decisive effect on the efficiency of the whole procedure.Two approaches for approximating reachable sets of oriented rectangular hull and convex hull are analyzed and compared in this paper.A hybrid algorithm is presented to compute the over approximating flow pipe,which has the merits of two geometrical approaches in order to reduce conservatism and improve computing speed.Finally the hybrid algorithm is implemented in Matlab environment.A section non-linear system is taken as an example to be verified.The results show that the presented hybrid algorithm is effective.

关 键 词：形式验证 可达集 有向矩形壳 凸多面体 

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