基于SAT求解器的故障树最小割集求解算法

故障树分析广泛应用于核工业、航空航天和交通控制等安全攸关领域的安全性分析。求解故障树的最小割集是故障树分析的关键步骤。目前,对于大规模故障树的最小割集的求解方法主要是将故障树转化为二元决策图之后求解,其主要缺点在于算法在时间和空间上的消耗严重依赖良好的变量顺序。为了减少存储资源并加快求解速度,提出了一种基于可满足性问题的故障树最小割集求解算法。首先,将求解故障树最小割集问题转化为求解布尔可满足性问题。然后,利用可满足性问题求解器,通过迭代分析求得最小可满足解集合,即为对应故障树的最小割集。实验表明,本文算法求得的最小割集准确、有效并且在空间和时间上的消耗均要优于传统的基于二元决策图的故障树最小割集求解算法。     

套索边界条件：一种可指导目标冲突修复的分歧描述

在需求工程中,分歧的目标冲突分析旨在识别、评估和修复分歧。分歧是由于域属性和目标不适配,使得系统在边界条件下无法同时满足所有目标。边界条件以线性时态逻辑的形式描述分歧。由于任意形式的边界条件缺乏可解释性,且评估和修复分歧需要大量人工评估和设计,所以目前边界条件的定义不利于高效地、自动化地评估和修复分歧。为此,首先提出一个可解释的边界条件——套索边界条件,直观地描述了系统由于一些特定的前提条件而产生分歧的情况;然后,设计了一个基于逐步弱化的套索边界条件识别算法LBCI,通过弱化线性时态逻辑公式逐步满足边界条件;最后,在基准数据集上评估了套索边界条件和LBCI的有效性。实验结果显示,套索边界条件增强了分歧的可解释性和对修复分歧有一定的指导作用。