论文摘要
混成系统是一类有广泛应用的系统,目前主要用混成自动机对其进行建模,对混成自动机进行可达性检验是保障混成系统质量的主要手段。目前对于混成系统的可达性分析主要有两类主要方法：一种是经典模型检验的方法,主要通过迭代的几何计算从初始状态集得到最终的可达状态集；另一种是基于SMT的有界模型检验的方法,它将混成自动机一定步长阈值内的行为编码为SMT问题,然后通过求解该问题得到相应的可达性。但这两种方法都要一次性面对完整的状态空间或阈值内的整体状态空间,导致它们能够求解的问题规模非常受限,无法应用于实际的验证需求。为了控制单次验证复杂度,相关研究者已经给出了一种基于线性规划的面向路径的线性混成自动机可达性分析方法,通过这种方法,每次只需要验证单条路径的可达性,因此可以对非常复杂的自动机和路径进行验证。作为一个直观的扩展,使用深度优先遍历算法遍历并生成步长小于一定阈值的所有路径,然后采用面向路径的可达性分析方法对单条路径的可达性分别进行验证。尽管这一方法展现了很好的性能和扩展性,但是如果待验证的路径数量巨大的话,整个验证过程仍然会非常耗时。为了解决这一问题,本文给出了如下优化方法：·基于IIS制导的深度优先搜索的有界可达性分析方法。只有在当前路径与可达性规约相关时,才使用面向路径的可达性分析方法对其进行验证；当一条路径被判定为不可满足时,通过线性规划的相关技术得到导致不可达的路径片段,并以此指导深度优先搜索过程的剪枝操作。·基于双向深度优先搜索的有界可达性分析方法。针对由于图结构的复杂性导致的很多明显包含不可达路径片段的路径被多次遍历的问题,首先给出基于反向深度优先搜索的有界可达性分析方法,并在此基础上将它与正向深度优先搜索算法整合,给出了基于双向深度优先搜索的有界可达性方法。我们通过将以上方法在相关的有界可达性检验工具BACH上进行集成实现,进而给出了新的版本BACH (V4.0)。我们将新版本的BACH与当前主流的验证工具进行了比较,实验结果表明我们的工具有着更好的性能和扩展性,并且对于某些问题,可以给出可判定的不可达结果。另一方面,作为一种比混成系统更为复杂的形态,信息物理融合系统是一个综合计算、网络和物理环境的多维复杂系统。它广泛应用于众多的安全关键领域。因此,对它的安全性验证就显得尤为重要。由于大多数该类系统都包含了连续状态变化和离散逻辑控制的交互过程,所以可以采用混成自动机对其进行建模。但是由于它与周围环境极强的交互性和动态性,导致模型中大量的参数只能在运行时动态获取,这导致经典的模型检验方法不再适用,而只能采用在线的验证方法。因此,基于以上给出的混成系统的可达性分析方法和验证工具,本文提出了一种对动态信息物理融合系统进行在线建模和验证的方法。该方法通过预先对系统进行抽象建模,然后通过周期性的获取系统快照得到运行时参数并以此来实例化模型,从而得到一个在有限短期未来可以使用的实例化模型,并通过对此模型的验证来保障系统安全性；此外,为了满足在线验证的实时性要求、提高验证效率,又给出了基于解域复用技术的增量式验证的方法和思路。
论文目录
相关论文文献
标签：混成系统论文; 模型检验论文; 信息物理融合系统论文; 可达性分析论文; 在线建模与验证论文;