基于约束凸多面体和抽象加细技术的混合系统的模型检测

本项目以模型检测技术在确保嵌入式系统的可靠性和安全性中的应用为研究背景，以提高嵌入式混合系统可达集的计算效率为切入点，探索约束凸多面体结构表示混合系统的无穷状态空间，研究抽象加细方法进行复杂混合系统的间接验证。基于计算机科学，优化数学以及控制学等学科的相关理论，以符号化方法为基本研究方法，建立一种约束凸多面体结构，即选构凸线性多面体的一种子类表示和处理矩形混合系统的无穷状态空间；以该结构为基础，利用经典的线性规划算法和约束求解规则计算矩形混合系统的可达状态集，构建模型检测规则，从而建立矩形混合系统完整的自动验证理论和算法；构造近似转换和互模拟关系把线性和非线性混合系统转换为矩形混合系统进行间接验证；构造基于优化技术的抽象加细规则提高转换效率和精确度；开发相应的验证支持工具，以确保混合系统的可靠性和安全性，并为混合系统的设计提供修正的反馈。

本项目研究混合系统的可靠性和安全性验证技术。研究约束凸多面体结构表示和处理矩形混合系统的无穷状态空间；以该结构为基础，研究矩形混合系统的可达状态集计算算法和模型检测规则，从而建立矩形混合系统完整的自动验证理论和算法；研究近似转换算法把线性和非线性混合系统转换为矩形混合系统进行间接验证。.研究成果：(1) 构建了PLTL公式到非确定性自动机的转换算法，建立了扩展区间时序逻辑的统一模型检测规则和投影时序逻辑的完备公理系统，从而建立了离散状态系统的验证理论；(2) 构建了一种约束凸多面体模型和一种多速率图表的数据结构表示和处理多速率混合系统的无穷状态空间,建立了多速率混合系统基于稠密的时间区间时序逻辑的模型检测算法；(3) 通过对混合区域放开不等式约束条件进行扩展，建立了非初始化的矩形混合系统的无穷状态空间搜索模型；定义了一种称作矩形图表的数据结构表示扩展的混合区域的并，来降低非初始化的矩形混合系统可达性分析的算法复杂度；(4) 通过构造两种类型的模型检测操作，建立了矩形混合系统基于全部的时间计算树逻辑公式的模型检测算法，通过转换为实时系统基于区间时序逻辑的模型检测问题，解决了矩形混合系统基于混合时序逻辑的模型检测问题；(5) 通过构建非线性空间的闭包矩形，给出了非线性混合系统到矩形混合系统的一个近似转换算法进行近似验证；(6) 作为验证问题的扩展和应用场景，对工作流、UML序列图的可靠性验证、多核调度算法及验证等问题展开了研究，并取得的大量的研究成果。