基于归纳不变式的混成系统安全性验证

论文摘要

随着嵌入式系统在安全攸关领域的广泛应用，嵌入式系统的研究也逐步升温。由于混成系统既可以描述嵌入式系统离散的控制逻辑，又可以描述其连续的硬件行为，因此成为嵌入式系统理想的形式化模型。安全性验证问题是混成系统研究中最具挑战性的问题之一。由于混成系统中存在连续行为，离散系统的安全性验证方法无法应用到混成系统，这就要求人们研究针对混成系统安全性验证的方法。本文基于归纳不变式的方法研究混成系统安全性验证，分别从归纳条件的评价准则、归纳条件的定义以及归纳不变式的生成方法三个方面进行了研究。本论文的主要贡献如下：初步建立了一套形式化的混成系统归纳条件评价准则。该准则有助于理解归纳条件的本质特征，并指导建立更好的归纳条件和求解方法，为后面归纳不变式的研究奠定理论基础。提出了一种基于指数条件和半定规划的归纳不变式(称为屏障证书)生成方法。基于指数条件的归纳不变式可以为系统的可达集形成一个更加精确的过近似，因此可以验证非安全集合与可达集紧密的安全性属性；该条件还具有凸性，从而能够利用半定规划实现高效的不变式求解。提出了一种基于完备条件和量词消去的归纳不变式生成方法。相对于前一种方法，该方法具有完备性，从而拥有更大的验证能力。与已有的完备归纳条件相比，本文的完备归纳条件可以很容易地被改写，从而获得一簇具有不同保守性和计算复杂度的充分归纳条件，因此提供了一种在验证能力和计算复杂度之间进行权衡的手段。设计了基于量词消去和SMT的归纳不变式求解算法。实现了一个混成系统归纳不变式的生成工具HIIDiscoverer，能够有效地求解混成系统归纳不变式。

论文目录

• 摘要
• Abstract
• 主要符号对照表
• 第1章 绪论
• 1.1 研究背景与意义
• 1.2 研究历史与现状
• 1.2.1 符号可达性分析
• 1.2.2 抽象
• 1.2.3 归纳不变式
• 1.3 研究思路
• 1.4 论文贡献
• 1.5 论文结构
• 第2章 混成系统归纳条件的评价准则
• 2.1 引言
• 2.2 预备知识
• 2.2.1 连续动态系统
• 2.2.2 混成系统
• 2.2.3 李导数
• 2.3 归纳不变式
• 2.3.1 安全性验证
• 2.3.2 归纳条件
• 2.4 归纳条件的正确性
• 2.5 归纳条件的完备性
• 2.6 归纳条件的相对保守性
• 2.7 归纳条件的凸性
• 2.8 本章小结
• 第3章 基于指数条件和半定规划的归纳不变式生成方法
• 3.1 引言
• 3.2 屏障证书的归纳条件
• 3.2.1 连续系统的屏障证书条件
• 3.2.2 混成系统的屏障证书条件
• 3.2.3 切换式自治系统的屏障证书条件
• 3.3 屏障证书的构造方法
• 3.3.1 连续系统指数条件的平方和形式
• 3.3.2 混成系统指数条件的平方和形式
• 3.3.3 切换式自治系统指数条件的平方和形式
• 3.4 案例研究
• 3.4.1 连续系统-例1
• 3.4.2 连续系统-例2
• 3.4.3 混成系统-例3
• 3.5 本章小结
• 第4章 基于完备条件和量词消去的归纳不变式生成方法
• 4.1 引言
• 4.2 多项式理想理论
• 4.3 一组完备的连续归纳条件
• 4.3.1 半代数归纳条件的基本形式
• 4.3.2 完备的归纳条件
• 4.3.3 充分的归纳条件
• 4.4 混成归纳条件
• 4.5 归纳不变式的计算方法
• 4.6 案例研究
• 4.7 本章小结
• 第5章 混成系统验证工具实现
• 5.1 引言
• 5.2 验证工具的设计与实现
• 5.2.1 初始化
• 5.2.2 归纳条件预处理
• 5.2.3 平方和求解
• 5.2.4 平方和验证
• 5.2.5 平方和规约
• 5.3 实例分析
• 5.3.1 模型
• 5.3.2 验证
• 5.3.3 实验结果
• 5.4 本章小结
• 第6章 总结与展望
• 6.1 工作总结
• 6.2 研究展望
• 参考文献
• 致谢
• 个人简历、在学期间发表的学术论文与研究成果