摘要:

摘要:安全案例提供清晰、全面和可靠的论据, 说明系统在特定环境下的操作满足可接受的安全性. 在受监管的安全攸关领域, 如汽车、航空和核能等领域, 认证机构通常要求系统经过严格的安全评估程序, 以确保其符合一个或多个安全标准. 在系统开发中应用安全案例是一种新兴的技术手段, 以结构化和全面的方式表达安全攸关系统的安全属性. 对安全案例的4个基本构建步骤: 确定目标、收集证据、构建论证和评估安全案例, 进行简要介绍. 然后聚焦于构建论证这一关键步骤, 详细介绍现有的8种安全案例表达形式, 包括目标结构符号(GSN)、声明-论点-证据(CAE)、结构化安全案例元模型(SACM)等, 并分析了它们的优缺点. 由于安全案例所需材料的显著复杂性, 软件工具通常被用作构建和评估安全案例的实用方法. 比较7种用于安全案例开发和评估的工具, 包括astah system safety、gsn2x、NOR-STA、Socrates、ASCE、D-Case Editor和AdvoCATE. 此外, 还深入探讨了安全案例构建中所面临的多重挑战, 这些挑战包括数据的可靠性和完整性、复杂性和不确定性的管理、监管和标准的不一致、人因工程、技术的快速发展以及团队和跨学科合作6个方面. 最后, 展望安全案例的未来研究方向, 揭示其潜在应用和研究问题.

摘要:人工智能技术已被广泛应用于生活中的各个领域. 然而, 神经网络作为人工智能的主要实现手段, 在面对训练数据之外的输入或对抗攻击时, 可能表现出意料之外的行为. 在自动驾驶、智能医疗等安全攸关领域, 这些未定义行为可能会对生命安全造成重大威胁. 因此, 使用完备验证方法证明神经网络的性质, 保障其行为的正确性显得尤为重要. 为了提高验证效率, 各种完备神经网络验证工具均提出各自的优化方法, 但并未充分探索这些方法真正起到的作用, 后来的研究者难以从中找出最有效的优化方向. 介绍神经网络验证领域的通用技术, 并提出一个完备神经网络验证的通用框架. 在此框架中, 重点讨论目前最先进的工具在约束求解、分支选择与边界计算这3个核心部分上的所采用的优化方法. 针对各个工具本身的性能和核心加速方法, 设计一系列实验, 旨在探究各种加速方式对于工具性能的贡献, 并尝试寻找最有效的加速策略和更具潜力的优化方向, 为研究者提供有价值的参考.

摘要:并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度, 在现实中有着非常广泛的应用. 但是并发程序与并发系统往往难以保证其实现的正确性, 实际应用程序运行中的错误会带来严重的后果. 同时, 并发程序执行时的不确定性会给其正确性验证带来巨大的困难. 在形式化验证方法中, 人们可以通过交互式定理证明器严格地对并发程序进行验证. 对在交互式定理证明中可用于描述并发程序正确性的验证目标进行总结, 它们包括霍尔三元组、可线性化、上下文精化和逻辑原子性. 交互式定理证明方法中常用程序逻辑对程序进行验证, 分析基于并发分离逻辑、依赖保证逻辑、关系霍尔逻辑等理论研究的系列成果与相应形式化方案, 并对使用这些方法的程序验证工具和程序验证成果进行总结.

摘要:航母舰载机弹药保障作业的智能规划作为一种高效能航保作业调度方法, 是助推航母工程先进技术建设发展的重要途径之一. 高安全攸关属性下作业规划方案的正确性保证已经逐渐成为制约其实际应用部署安全的关键技术瓶颈. 针对方案正确性验证中存在的弹药保障系统难建模、作业执行行为难描述、形式验证工具难实现等挑战, 基于分离逻辑的思想, 提出一种弹药保障系统的行为模型, 并利用定理证明器Coq对作业规划方案进行形式化验证. 首先提出一个符合弹药保障作业特征的序列化双层资源堆模型; 基于该模型, 构造一套可用于描述作业执行行为的建模语言及其操作语义; 最后在Coq中实现一种证明辅助工具. 通过几个典型弹药保障作业规划方案的交互式证明实例, 验证工具的可用性与工程实用性.

摘要:已有的基于点区间优先级时间Petri网分析实时嵌入式多核系统的工作, 存在以下不足: (1)点区间优先级时间Petri网只考虑每个任务的执行时间是一个固定值的情况, 而更多的实际应用中每个任务的执行时间是在一个区间范围内, 因此不能模拟这些应用; (2)没有实现从任务依赖图到点区间优先级时间Petri网的自动转化, 不便于工程设计人员使用; (3)没有考虑任务间互斥访问共享变量的情况. 为此, 定义了优先级时间Petri网(Pri-TPN)以弥补第1个不足; 定义带有资源分配与优先级的任务依赖图(TDG-RAP)以弥补第3个不足; 给出从TDG-RAP到Pri-TPN的转化规则与算法以弥补第2个不足, 以及基于Pri-TPN分析任务最坏执行时间与系统死锁的算法; 开发工具软件, 方便工程设计人员使用.

摘要:可线性化被公认为并发对象正确性标准, 但其已被证明不能作为含有随机语句的并发对象的正确性标准. 为此, Golab等人提出了强可线性化概念, 它在可线性化的定义上增加了前缀保持性质, 对并发对象具有更强的约束性. 关于强可线性化的研究集中在使用特定的基本对象构造满足强可线性化性质的并发对象的可行性. 对常见的并发对象的强可线性化性质的检测和验证方面的研究较为少见. 从并发对象的验证算法和证否方法两个方面研究了强可线性化性质. 首先, 细化强可线性化性质, 将它细分为固定生效点和单纯帮助两类, 并证明固定生效点是已有的固定可线性化点概念的扩展. 其次, 提出两种强可线性化的验证算法, 其中一种基于固定可线性化点, 另一种基于固定生效点. 最后, 给出一个构造性的证明并发对象违背强可线性化的证明方法, 依据该方法证明了Herlihy&Wing队列、一种单读单写寄存器实现和一种并发快照实现违反强可线性化性质.

摘要:DH坐标系在机器人运动学分析中发挥着重要的作用. 在基于DH坐标系构建的机器人控制系统中, 机器人结构的复杂性使得构建安全的控制系统成为一个难题, 仅依靠人工方法可能导致系统漏洞和安全风险, 从而危及机器人的安全. 形式化方法通过演绎推理与代码抽取实现了对软硬件系统的设计、开发及验证. 基于此, 设计基于DH标定的机器人正向运动学的形式化验证框架. 在Coq中构建机器人运动理论的形式化证明, 并验证控制算法的正确性以确保机器人的运动安全. 首先, 对DH坐标系进行形式化建模, 构建相邻坐标系间转换矩阵的形式化定义, 并验证该转换矩阵与复合螺旋运动的等价性; 其次, 构建机械臂正向运动学的形式化定义, 并对机械臂运动的可分解性进行形式化验证; 再次, 对工业机器人中常见连杆结构及机器人进行形式化建模, 并完成正向运动学的形式化验证; 最后, 实现Coq到OCaml的代码抽取, 并对抽取的代码进行分析与验证.

摘要:操作系统在许多安全攸关领域为软件系统提供关键性底层支撑, 操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障, 造成巨大经济损失或危及人身安全. 为了减少此类安全事故的发生, 对操作系统正确性进行验证十分必要. 传统测试手段无法穷尽系统中的所有潜在错误, 因而操作系统验证有必要使用具有严格数学理论基础的形式化方法. 在操作系统中, 互斥量可协调多任务对资源的访问, 是一种常用的任务同步方式, 其功能正确性对于保障多任务应用的正确性十分关键. 基于定理证明方法, 在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模, 给出其接口函数的形式化规范, 并实现这些接口函数的功能正确性验证.

摘要:随着区块链技术在各行各业的广泛应用, 区块链系统的架构变得越来越复杂, 这也增加了安全问题的数量. 目前, 在区块链系统中采用了模糊测试、符号执行等传统的漏洞检测方法, 但这些技术无法有效检测出未知的漏洞. 为了提高区块链系统的安全性, 提出基于形式化方法的区块链系统漏洞检测模型VDMBS (vulnerability detection model for blockchain systems), 所提模型综合系统迁移状态、安全规约和节点间信任关系等多种安全因素, 同时提供基于业务流程执行语言BPEL (business process execution language)的漏洞模型构建方法. 最后, 用NuSMV在基于区块链的电子投票选举系统上验证所提出的漏洞检测模型的有效性, 实验结果表明, 与现有的5种形式化测试工具相比, 所提出的VDMBS模型能够检测出更多的区块链系统业务逻辑漏洞和智能合约漏洞.

摘要:动态规划是一种递归求解问题最优解的方法, 主要通过求解子问题的解并组合这些解来求解原问题. 由于其子问题之间存在大量依赖关系和约束条件, 所以验证过程繁琐, 尤其对命令式动态规划类算法程序正确性验证是一个难点. 基于动态规划类算法Isabelle/HOL函数式建模与验证, 通过证明命令式动态规划类算法程序与其的等价性, 避免证明正确性时处理复杂的依赖关系和约束条件, 提出命令式动态规划类算法程序设计框架及其机械化验证. 首先, 根据动态规划类算法的优化方法(备忘录方法)和性质(最优子结构性质和子问题重叠性质)描述问题规约、归纳递推关系式和形式化构造出循环不变式, 并且基于递推关系式生成IMP (minimalistic imperative programming language)代码; 其次, 将问题规约、循环不变式和生成的IMP代码输入VCG (verification condition generator), 自动生成正确性的验证条件; 然后, 在Isabelle/HOL定理证明器中对验证条件进行机械化验证. 算法首先设计为命令式动态规划类算法的一般形式, 并进一步实例化得到具体算法. 最后, 例证所提框架的有效性, 为动态规划类算法的自动化推导和验证提供参考价值.

摘要:Trie结构是一种使用搜索关键字来组织信息的搜索树, 可用于高效地存储和搜索字符串集合. Nipkow等人给出了实现Trie的Isabelle建模与验证, 然而其Trie在存储和操作时存在大量的冗余, 导致空间利用率不高, 且仅考虑英文单模式下查找. 为此, 基于索引即键值的思想提出了Trie+结构, 相较于传统的索引与键值分开存储的结构能减少50%的存储空间, 大大提高了空间利用率. 并且, 对Trie+结构的查找、插入、删除等操作给出了函数式建模及其严格的机械化验证, 保证操作的正确性和可靠性. 进一步, 提出一种匹配算法的通用验证规约, 旨在解决一系列的匹配算法正确性验证问题. 最后, 基于Trie+结构与匹配算法通用验证规约, 建模和验证了函数式中英文混合多模式匹配算法, 发现并解决了现有研究中的基于完全哈希Trie的多模式匹配算法的模式串前缀终止的Bug. 该Trie+结构以及验证规约在提高Trie结构空间利用率和验证匹配算法中, 有一定的理论和应用价值.

摘要:在民机自动飞行过程中, 自动飞行系统模式转换是影响安全的重要因素, 随着现代民机机载系统的功能与复杂度的快速增长, 在需求阶段对自动飞行系统模式转换的安全性分析和验证成为重要的挑战. 飞行模式转换的复杂性不仅体现在自动飞行过程中必需的多重飞行模式之间的交互关系, 还体现在模式转换与外部环境之间复杂的数据与控制交联关系, 这些交联关系同时隐含了飞行模式转换的安全性质, 这些特征提高了形式化方法的应用难度. 提出一种领域特定的建模验证框架: 首先, 提出面向自动飞行系统模式转换的领域需求建模语言MTRDL和基于该语言扩展于SysML上的建模方法; 其次, 提出基于安全需求模板的安全性质辅助规约方法; 最后, 通过对某机型的若干条目化需求的实例研究, 证明所提方法在自动飞行系统模式转换需求验证中的有效性.

摘要:许多复杂的嵌入式系统都是混合关键系统(mixed-criticality system, MCS). MCS通常需要在指定的关键性(criticality)等级状态下运行, 但是它们可能会受到一些危害的影响, 这些危害可能会导致随机错误和突发错误, 进一步导致执行线程中止, 甚至导致系统故障. 目前的研究仅集中于对MCS的可调度性分析, 未能进一步分析系统安全性, 未能考虑线程之间的依赖关系. 以随机错误和突发错误为研究对象, 提出一种集成故障传播分析的基于架构的MCS安全分析方法. 使用架构分析和设计语言(architecture analysis and design language, AADL)刻画构件依赖关系. 为了弥补AADL的不足, 创建新的AADL属性(AADL突发错误属性), 并提出新的线程状态机(突发错误行为线程状态机)语义来描述带有突发错误的线程执行过程. 为了将概率模型检查应用于安全分析, 提出模型转换规则和组装方法, 从AADL模型推导出PRISM模型. 建立了两个公式, 分别获得定量安全属性以验证故障发生的概率, 以及定性安全属性以生成相应的正例来求出故障传播路径来进行故障传播分析. 最后, 以动力艇自动驾驶仪(power boat autopilot, PBA)系统为例, 验证了该方法的有效性.

摘要:无限字自动机的确定化是理论计算机研究重要的一部分, 在形式化验证, 时序逻辑, 模型检测等方面有重要应用. 自Büchi自动机提出半个世纪以来, 其自动机的确定化算法始终是其中的基础. 有别于当初只是在理论上对其大小上下界的探索, 利用日新月异的高性能计算机技术不失为一种有效的辅助手段. 为了深入研究非确定性Büchi自动机确定化算法的实现过程, 希望重点研究确定化过程中的索引能否继续被优化的问题, 实现确定化研究工具NB2DR. 可以对非确定性Büchi自动机进行高效的确定化, 并通过工具提供的分析其确定化过程来达到对其确定化算法改进的目的. 通过对生成的确定性无限字自动机的索引的深入分析来探索相关索引的理论. 该工具还实现了可以根据需要的Büchi自动机的大小与字母表参数, 生成确定化的Rabin自动机族, 亦可以反向根据需要的指定索引的大小来生成全部Büchi自动机族, 测试生成无限字自动机的等价性等功能.

摘要:事实验证旨在检查一个文本陈述是否被给定的证据所支持. 由于表格结构上具有依赖性、内容上具有隐含性, 以表格作为证据的事实验证任务仍面临很多挑战. 现有工作或者利用逻辑表达式来解析基于表格证据的陈述, 或者设计表格感知神经网络来编码陈述-表格对, 以此实现基于表格的事实验证任务. 但是, 这些方法没有充分利用陈述背后隐含的表格信息, 从而导致模型的推理性能下降, 并且基于表格证据的中文陈述具有更加复杂的语法和语义, 也给模型推理带来更大的困难. 为此, 提出基于胶囊异构图注意力网络(CapsHAN)的中文表格型数据事实验证方法, 所提方法能充分理解陈述的结构和语义, 进而挖掘和利用陈述所隐含的表格信息, 有效提升基于表格的事实验证任务准确性. 具体而言, 首先通过对陈述进行依存句法分析和命名实体识别来构建异构图, 接着对该图采用异构图注意力网络和胶囊图神经网络进行学习和理解, 然后将得到的陈述文本表示与经过编码的表格文本表示进行拼接, 最后完成结果的预测. 更进一步, 针对现有中文表格型事实验证数据集匮乏而难以支持基于表格的事实验证方法性能评价的难题, 首先对主流TABFACT和INFOTABS表格事实验证英文数据集进行中文转化, 并且专门针对中文表格型数据的特点构建了基于UCL国家标准的数据集UCLDS, 该数据集将维基百科信息框作为人工注释的自然语言陈述的证据, 并被标记为蕴含、反驳或中立3类. UCLDS在同时支持单表和多表推理方面比传统TABFACT和INFOTABS数据集更胜一筹. 在上述3个中文基准数据集上的实验结果表明, 所提模型的表现均优于基线模型, 证明该模型在基于中文表格的事实验证任务上的优越性.

摘要:睡眠过程中的人体呼吸波形检测对于智慧康养和医疗保健应用至关重要, 结合不同的呼吸波形模式可以实现睡眠质量分析和呼吸系统疾病检测. 传统基于接触式设备的呼吸感知方法会给用户带来诸多不便, 与其相比, 非接触式感知方法更适合进行连续性监测. 然而, 在睡眠过程中由于设备部署、睡眠姿态以及人体运动都具有随机性, 严重限制了非接触呼吸感知方案在日常生活中的使用. 为此, 提出一种基于脉冲超宽带(impulse radio-ultra wide band, IR-UWB)的睡眠状态下人体呼吸波形检测方法. 所提方法以睡眠状态下人体呼吸时其胸腔起伏导致无线脉冲信号传播路径的周期性变化为基础, 进而生成细粒度的人体呼吸波形, 实现呼吸波形的实时输出以及呼吸速率的高精度估计. 首先, 为了从接收无线射频信号中获取人体呼吸时的胸腔位置, 提出一个基于IR-UWB信号的呼吸能量比指标来实现目标位置估计. 然后, 通过提出基于I/Q复平面的向量投影方法和基于呼吸向量圆周位置的投影信号选择方法, 从反射信号中提取到人体呼吸特征波形. 最后, 结合变分编码器-解码器网络来实现睡眠状态下细粒度的呼吸波形恢复. 通过在不同条件下进行大量实验测试, 结果表明所提方法在睡眠状态下监测的人体呼吸波形与商用呼吸带获得的真实波形高度相似, 其呼吸速率的平均估计误差为0.229 bpm, 可实现高精度的睡眠状态下人体呼吸波形检测.

摘要:对于安全可靠的机器学习系统, 具备检测训练集分布外 (out-of-distribution, OOD) 样本的能力十分必要. 基于似然的生成式模型由于训练时不需要样本标签, 是一类非常受欢迎的OOD检测方法. 然而, 近期研究表明通过似然来检测OOD样本往往会失效, 并且失效原因与解决方案的探究仍较少, 尤其是对于文本数据. 从模型层面和数据层面分析文本上失效的原因: 生成式模型的泛化性不足和文本先验概率的偏差. 在此基础上, 提出一种新的OOD文本检测方法Pobe. 针对生成式模型泛化性不足的问题, 引入KNN检索的方式, 来提升模型的泛化性. 针对文本先验概率偏差的问题, 设计一种偏差校准策略, 借助预训练语言模型改善概率偏差对OOD检测的影响, 并通过贝叶斯定理证明策略的合理性. 通过在广泛的数据集上进行实验, 证明所提方法的有效性, 其中, 在8个数据集上的平均AUROC值超过99%, FPR95值低于1%.

摘要:属性级情感分类任务旨在判断句子针对给定属性的情感极性, 因其广泛应用而备受关注. 该任务的关键在于识别给定属性相关的上下文描述, 并根据上下文内容判断发文者针对相应属性的情感倾向. 统计发现, 大约30%的评论中并不包含关于给定属性的明确情感描述, 但仍然传达了清晰的情感倾向, 这被称为隐式情感表达. 近年来, 基于注意力机制的神经网络方法在情感分析中得到了成功应用. 但该类方法只能捕捉属性相关的显式情感描述, 而缺乏对隐含情感的有效分析和挖掘, 且往往将属性词与句子上下文分别建模, 使得属性词的表示缺乏上下文语义. 针对以上两个问题, 提出一种交叉融合属性局部和句子全局上下文信息的属性级情感分类方法, 并根据隐式和显式情感表达句子不同的分类难度采用课程学习提高模型的分类性能. 实验表明, 所提方法不仅对显式情感表达句子的属性情感倾向识别准确率高, 而且能够有效学习隐式情感表达句子的情感类别.

摘要:现有的超图网络表示方法需要分析全批量节点和超边以实现跨层递归扩展邻域, 这会带来巨大的计算开销, 且因过度扩展导致更低的泛化精度. 为解决这一问题, 提出一种基于重要性采样的超图表示方法. 首先, 它将节点和超边看作是两组符合特定概率测度的独立同分布样本, 用积分形式解释超图的结构特征交互; 其次, 设计带可学习参数的邻域重要性采样规则, 根据节点和超边的物理关系和特征计算采样概率, 逐层递归采集固定数目的对象, 构造一个更小的采样邻接矩阵; 最终, 利用蒙特卡洛方法近似估计整个超图的空间特征. 此外, 借鉴PINN的优势, 将需要缩减的方差作为物理约束加入到超图神经网络中, 以获取更具泛化能力的采样规则. 多个数据集上的广泛实验表明, 所提出的方法能够获得更准确的超图表示结果, 同时具有更快的收敛速度.

摘要:多视图聚类在图像处理、数据挖掘和机器学习等领域引起了越来越多的关注. 现有的多视图聚类算法存在两个不足, 一是在图构造过程中只考虑每个视图数据之间的成对关系生成亲和矩阵, 而缺乏邻域关系的刻画; 二是现有的方法将多视图信息融合和聚类的过程相分离, 从而降低了算法的聚类性能. 为此, 提出一种更为准确和鲁棒的基于二部图的联合谱嵌入多视图聚类算法. 首先, 基于多视图子空间聚类的思想构造二部图进而产生相似图, 接着利用相似图的谱嵌入矩阵进行图融合, 其次, 在融合过程中考虑每个视图的重要性进行权重约束, 进而引入聚类指示矩阵得到最终的聚类结果. 提出的模型将二部图、嵌入矩阵与聚类指示矩阵约束在一个框架下进行优化. 此外, 提供一种求解该模型的快速优化策略, 该策略将优化问题分解成小规模子问题, 并通过迭代步骤高效解决. 提出算法和已有的多视图聚类算法在真实数据集上进行实验分析. 实验结果表明, 相比已有方法, 提出算法在处理多视图聚类问题上是更加有效和鲁棒的.

摘要:随着互联网信息技术的高速发展, 线上学习资源的爆炸式增长引起了“信息过载”与“学习迷航”问题. 在缺乏专家指导的场景中, 用户难以明确自己的学习需求并从海量的学习资源中选择合适的内容进行学习. 教育领域推荐方法能够基于用户的历史学习行为提供学习资源的个性化推荐, 因此该方法近年来受到大量研究人员的广泛关注. 然而, 现有的教育领域推荐方法在学习需求感知时忽略了对知识点之间复杂关系的建模, 同时缺乏考虑用户学习需求的动态性变化, 导致推荐的学习资源不够精准. 针对上述问题, 提出一种基于静态与动态学习需求感知的知识点推荐方法, 通过静态感知与动态感知相结合的方式建模复杂知识关联下的用户学习行为. 对于静态学习需求感知, 设计一种基于知识点先修后继元路径引导的注意力图卷积网络, 通过建模知识点之间先修后继关系的复杂约束, 能够消除其他非学习需求因素的干扰, 从而精准地捕获用户在细粒度知识点层面上的静态学习需求; 对于动态学习需求感知, 所提方法以课程为单元聚合知识点嵌入以表征用户在不同时刻的知识水平, 然后采用循环神经网络建模编码用户的知识水平序列, 能够有效地挖掘用户知识水平变化中蕴含的动态学习需求; 最后, 对获得的静态与动态学习需求进行融合, 在同一框架下建模静态与动态学习需求之间的兼容性, 促进这两种学习需求相互补充, 以实现细粒度的个性化知识点推荐. 实验表明, 在两个公开数据集上, 所提方法能够有效地感知用户的学习需求并提供个性化的知识点推荐, 在多种评估指标上优于主流的推荐方法.

摘要:不一致数据子集修复问题是数据清洗领域的重要研究问题, 现有方法大多是基于完整性约束规则的, 采用最小删除元组数量原则进行子集修复. 然而, 这种方法没有考虑删除元组的质量, 导致修复准确性较低. 为此, 提出规则与概率相结合的子集修复方法, 建模不一致元组概率使得正确元组的平均概率大于错误元组的平均概率, 求解删除元组概率和最小的子集修复方案. 此外, 为了减小不一致元组概率计算的时间开销, 提出一种高效的错误检测方法, 减小不一致元组规模. 真实数据和合成数据上的实验结果验证所提方法的准确性优于现有最好方法.

摘要:数据库性能受数据库配置参数的影响, 参数设置的好坏会直接反映到数据库性能表现上, 因此, 数据库调参方法的优劣至关重要. 然而, 传统的数据库调参方法存在诸多局限性, 例如无法充分利用历史调参数据、浪费时间人力资源等. 而反事实解释方法是一种对原数据进行少量修改, 从而将原预测改变为期望预测的方法, 其起到的是建议的作用. 这种作用可以用于数据库配置优化, 即对数据库配置进行少量修改, 从而使得数据库的性能表现得到优化. 因此, 提出面向数据库配置优化的反事实解释方法, 对于在特定负载条件下性能表现不佳的数据库, 所提方法可以对数据库配置进行修改, 生成相应的数据库配置反事实, 从而优化数据库性能. 进行两种实验, 分别用于评估反事实解释方法的优劣以及验证其优化数据库的效果, 实验结果表明: 综合各个评估指标, 提出的反事实解释方法要优于其他的经典反事实解释方法, 并且生成的反事实能够确实有效地提高数据库性能.