【作者】 刘震；

【导师】 方敏；

【作者基本信息】 合肥工业大学 ， 控制理论与控制工程， 2010， 硕士

【摘要】 混杂系统的形式验证技术是利用数学分析方法对混杂系统的安全性进行验证。近十年来,模型验证技术是形式验证研究的主要方法。模型验证技术是指,利用计算机强大的计算功能自动地对混杂系统的数学模型进行整个状态空间中进行遍历搜索,对系统所有可能的运行轨迹进行收敛计算或过近似计算,以检验系统的实现方案是否满足系统的设计要求。论文首先介绍了模型验证的概念和特点,常用的混杂系统建模方法如混杂自动机、混杂Petri网、层次结构和时段演算。分析了可达集的两种计算方法—前向和后向可达集算法,对可达集的过近似方法作了系统的阐述。最后详细介绍了模型验证的国内外研究状况和常用的模型验证工具。针对混杂系统连续子系统和离散子系统相互作用的特点,研究了混杂自动机模、多面体混杂自动机和混杂I/O自动机的建模方法;对于混杂系统的流管道过近似问题,给出了齐诺多面体(zonotopes)的基于中心点和生成元(generators)的表达式和过近似算法,分析了该算法的保守性、封闭性、集合交并处理能力以及收敛性。通过比较凸多面体过近似和齐诺多面体过近似算法的适用对象、计算方法、过近似保守性和随维数增长的计算复杂度,对两种算法的优劣和特点进行了详细的分析。针对常压炉加热炉系统(线性混杂系统)和汽车自适应巡航系统(非线性混杂系统)建立数学模型,抽象出验证问题,给出ACTL验证规范。使用PHAVer和CheckMate验证工具分别对上述两种系统建立混杂I/O自动机模型和阈值切换系统模型,应用齐诺多面体流管道过近似方法和凸多面体流管道过近似方法进行模型检验,对系统的状态可达性和运行安全性进行了分析,并给出验证结论。通过上述结论,分析验证工具CheckMate和PHAVer的保守性、消耗时间和内存空间占用率,对上述两种验证工具的验证效果进行了比较。更多还原

【Abstract】 Hybrid systems formal verification is a mathematically-based technology for specifying the hybrid system’s safety porperty. In recent ten years, model verification technology is the main method of formal verification. Model verification is to verify if a system satisfies the designing requirements by traversal search algorithms using computer to automatically check all states space through and convergently or over-approximately computing possible trajectories.In this thesis, the conception and characters of modeling verification has been firstly introduced, and then the useful modeling methods such as hybrid automaton, hybrid Petri net, hierarchical structure and duration calculus. The front computing method, backward computing method and over-approximated method for reachable sets have been systematically anglicized. Finally introduce the native and abroad researching status and useful modeling tools.Due to the character of hybrid system that not only include continuous subsystem and discrete subsystem, investigate the hybrid automaton, polyhedron hybrid automaton and hybrid input and output automaton. For the problem of over-approximated flow pipe, the new over-approximated polyhedron zonotopes which represent the reachable sets based on the center and generators. Analyze the conservative and close property, intersection and convergence. Through comparing adaptive system, computing method and computing complexity, tells the advantages and disadvantages from convex hull and zonotopes.Build mathematic model, abstract the verification questions, provide the ACTL specification for atmospheric pressure oven heating system (linear system) and automobile adaptive cruise system (nonlinear system). Use PHAVer and CheckMate to construct the hybrid system respectively, apply zonotopes polyhedral and convex hull to over-approximated flow pipe for verifing models, analyzing the state reachability and safety property for the above mentioned hybrid system. Through analyzing the conservative property, time consumption and output file size, comparing the advantages and disadvantages of CheckMate and PHAVer.更多还原