混杂系统模型验证工具的验证效果分析
发布时间:2021-02-03 00:25
混杂系统的形式验证技术是利用数学分析方法对混杂系统的安全性进行验证。近十年来,模型验证技术是形式验证研究的主要方法。模型验证技术是指,利用计算机强大的计算功能自动地对混杂系统的数学模型进行整个状态空间中进行遍历搜索,对系统所有可能的运行轨迹进行收敛计算或过近似计算,以检验系统的实现方案是否满足系统的设计要求。论文首先介绍了模型验证的概念和特点,常用的混杂系统建模方法如混杂自动机、混杂Petri网、层次结构和时段演算。分析了可达集的两种计算方法—前向和后向可达集算法,对可达集的过近似方法作了系统的阐述。最后详细介绍了模型验证的国内外研究状况和常用的模型验证工具。针对混杂系统连续子系统和离散子系统相互作用的特点,研究了混杂自动机模、多面体混杂自动机和混杂I/O自动机的建模方法;对于混杂系统的流管道过近似问题,给出了齐诺多面体(zonotopes)的基于中心点和生成元(generators)的表达式和过近似算法,分析了该算法的保守性、封闭性、集合交并处理能力以及收敛性。通过比较凸多面体过近似和齐诺多面体过近似算法的适用对象、计算方法、过近似保守性和随维数增长的计算复杂度,对两种算法的优劣和特...
【文章来源】:合肥工业大学安徽省 211工程院校 教育部直属院校
【文章页数】:80 页
【学位级别】:硕士
【部分图文】:
CheckMate模块
域的详细说明,请参见参数输入部分。连续系统切换模块和该模块的参数如图3.2所示:图3.2 切换连续系统模块和参数对话框3.2 多面体阈值事件模块(Polyhedral Threshold Block,PTHB)图 3.3 多面体阈值模块和参数对话框
多面体阈值模块和参数对话框
本文编号:3015607
【文章来源】:合肥工业大学安徽省 211工程院校 教育部直属院校
【文章页数】:80 页
【学位级别】:硕士
【部分图文】:
CheckMate模块
域的详细说明,请参见参数输入部分。连续系统切换模块和该模块的参数如图3.2所示:图3.2 切换连续系统模块和参数对话框3.2 多面体阈值事件模块(Polyhedral Threshold Block,PTHB)图 3.3 多面体阈值模块和参数对话框
多面体阈值模块和参数对话框
本文编号:3015607
本文链接:https://www.wllwen.com/projectlw/xtxlw/3015607.html