摘要
混合系统形式验证技术是分析在给定的初始条件下,系统的可达集是否都在目标状态集合内。计算可达集是混合系统形式验证中的重要一步,选用何种几何体表示可达集对于整个验证精度有决定性的影响。文章对有向矩形壳和凸多面体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.
出处
《合肥工业大学学报（自然科学版）》
CAS
CSCD
北大核心
2010年第10期1506-1509,1535,共5页
Journal of Hefei University of Technology：Natural Science
关键词
形式验证
可达集
有向矩形壳
凸多面体
formal verification
reachable set
oriented rectangular hull
convex hull
