混合系统的算法分析

论文摘要

混合系统(Hybrid System)能够有效地捕获嵌入式系统中离散和连续成分之间的动态交互作用。它架起了计算机科学、控制工程和数学之间的桥梁,为嵌入式系统提供了形式化的分析和合成方法。形式化验证是混合系统的一个重要研究方向。它可以检验混合系统是否在任何环境下都能安全运行,对于保证系统的安全性起着至关重要的作用。可达性分析和可达集的计算是混合系统形式化验证的基础。本文的主要研究内容如下:1.设计了通用的前向可达性分析算法,并给出了正确性验证。然后在基于模型整合计算的平台ReachLab中实现了前向可达性分析算法模型,并运用ReachLab提供的翻译器来自动产生可执行的基于水平集工具包的Matlab代码,在Matlab环境下进行可达集的计算。2.引进符号计算(symbolic computation)来精确地求解混合系统的可达集,然后运用量词消去法(quantifier elimination)消去可达集描述中的量词,得到精确的可达集。3.定义了误差的计算方法,结合符号计算求解的可达集,对基于水平集内核计算得到的结果进行误差分析,并提出了如何调整水平集内核的参数得到更准确的结果。

论文目录

• 摘要
• Abstract
• 目录
• 第一章 绪论
• 1.1 研究背景
• 1.2 研究现状、意义
• 1.3 研究内容
• 第二章 混合系统的基本理论
• 2.1 混合自动机（Hybrid Automaton）
• 2.2 迁移系统（Transition System）
• 2.3 混合自动机的操作语义
• 2.4 可达性分析
• 2.5 混合系统形式化分析
• 2.5.1 模型检验
• 2.5.2 计算树逻辑
• 2.5.3 相关工具介绍
• 第三章 计算平台:ReachLab
• 3.1 特定域建模语言（Domain Specific Modeling Language,DSML）
• 3.2 混合系统分析和设计语言（Hybrid System Analysis and Design Language,HADL）
• 3.3 计算平台:ReachLab
• 3.4 水平集工具包（Level set toolbox）
• 第四章 可达性分析算法的设计与应用
• 4.1 可达性分析的引出
• 4.2 前向可达性分析算法的设计
• 4.3 前向可达性分析算法的实现
• 4.4 前向可达性分析算法的正确性验证
• 4.4.1 可达集的符号化表示
• 4.4.2 量词消去（Quantifier Elimination）
• 4.4.3 算法的正确性验证
• 4.5 前向可达性分析算法的应用
• 4.6 在ReachLab中进行形式化分析
• 第五章 误差分析
• 5.1 误差分析方法
• 第六章 结语
• 6.1 全文总结
• 6.2 展望
• 参考文献
• 致谢