基于插值的多核限界模型检测技术研究

发布时间：2023-06-28 03:50

　　在智能时代,随着信息系统的规模和复杂度日益增大,人们对系统运行时的安全性和可靠性的要求越来越高。限界模型检测技术作为自动检验系统的有效手段,在提高系统可信性上发挥着重要作用。限界模型检测与插值序列相结合可以完成限定边界外属性的验证,进而实现无界模型检测。然而,插值序列的引入会增大模型编码的复杂程度,影响模型检测器整体的性能。针对这个问题,本文提出了基于插值的多核限界模型检测方法。本文的主要工作和创新点如下:首先,本文提出基于插值和状态空间划分的属性验证算法,将问题分解并利用多核技术并行求解。模型状态空间中的状态迁移路径被划分为路径簇,再利用限界模型检测和基于插值序列的可达性分析方法对路径簇进行验证。其次,利用路径簇中存在不动点的性质,本文提出路径簇剪枝算法,缩小待搜索状态空间的规模以提高检测效率。最后,为了进一步改进算法,本文提出了增量编码和验证假设两种优化方法。增量编码的思想是定量增加检测限界,减少约束求解器的调用次数。验证假设的思想是在模型检测中利用验证历史信息,将已验证过的属性加入到命题公式中,提高插值的求解效率。本文提出的基于插值的多核限界模型检测方法应用于层次状态变迁矩阵描述...

【文章页数】：65 页

【学位级别】：硕士

【文章目录】：
摘要
Abstract
1 绪论
    1.1 研究背景
    1.2 国内外研究现状
        1.2.1 模型检测方法
        1.2.2 插值验证方法
    1.3 研究内容
    1.4 论文结构
2 相关理论背景
    2.1 限界模型检测
    2.2 层次状态变迁矩阵
    2.3 线性时序逻辑
    2.4 插值定理
    2.5 本章小结
3 基于插值的多核限界模型检测算法
    3.1 主要思想
    3.2 限界模型检测
        3.2.1 限界增量编码
        3.2.2 状态空间搜索
    3.3 基于插值的分析
    3.4 模型分簇
        3.4.1 路径簇划分
        3.4.2 多核检测
    3.5 本章小结
4 面向活性属性的检测方法
    4.1 套索检测
    4.2 活性属性转化
    4.3 模型编码与验证
    4.4 本章小结
5 验证与实验结果分析
    5.1 实验环境与工具
    5.2 实验方案概述
    5.3 实验结果分析
        5.3.1 基于插值的模型检测实验
        5.3.2 限界增量检测对比实验
        5.3.3 多核模型检测实验
        5.3.4 活性属性实验
    5.4 本章小结
结论
参考文献
攻读硕士学位期间发表学术论文情况
致谢



本文编号：3835923