高级检索

    融合基数约束与单次入队的基于模型诊断方法

    A Model-Based Diagnosis Method for Integrating Cardinality Constraints and Enqueueing at Once

    • 摘要: 基于模型诊断(MBD)在不同的环境中有越来越多的用途,包括软件故障定位,电子表格的调试,Web服务和硬件设计,以及生物系统的分析等. 受这些不同用途的启发,近年来MBD算法改进成效显著. 然而,对体系庞大、结构复杂的系统,需要对现有方法进一步改进. 由于求解诊断解在计算上具有挑战性,因此相继提出了一些通过压缩模型的MBD算法来提高诊断效率,如基于统治的多观测压缩模型算法(dominated-based compacted model with multiple observations,D-CMMO). 对于给定多个观测值且注入1个以上错误,需要大量时间的诊断问题,提出了一个新的诊断模型(cardinality-constrained compacted model,CCM)来解决. 基于基数约束的压缩模型算法使用2种方法对求解过程进行优化:首先,利用系统观测的故障输出和故障组件数量之间的约束关系来限制目标解的范围; 其次,通过对假设集采用单次入队方法, 进而有效提升MaxSAT(maximum satisfiability)求解器的性能. 此外,在ISCAS85和ITC99基准测试用例上的实验结果表明,与目前最新的MBD求解【方法】D-CMMO 相比,上述2种优化方法有效缩小了MBD问题的求解范围,降低 MaxSAT 求解器搜索目标解的难度,进而能在更短的时间内返回一个诊断解. 在平均状况下,CCM方法相比D-CMMO方法在求解效率上分别提升64.5%和92.8%.

       

      Abstract: Model-Based Diagnosis (MBD) finds a growing number of uses in different settings, which include software fault localization, debugging of spread sheets, web services, and hardware designs, but also the analysis of biological systems, among many others. Motivated by these different uses, there have been significant improvements made to MBD algorithms in recent years. Nevertheless, the analysis of larger and more complex systems motivates further improvements to existing approaches. Since computing diagnosis is computationally challenging, some MBD algorithms by compacting the model are presented successively, such as Dominated-based Compacted Model with Multiple Observations (D-CMMO) approach. In this paper, we propose one new diagnosis model, namely, Cardinality-Constrained Compacted Model (CCM), to solve the problem in which a considerable amount of time is needed when multiple observations are given and more than one fault is injected. CCM uses two methods to optimize the process of solving MBD. Firstly, we propose to utilize relationship of faulty system-outs and faulty components to limit the scope of target solution. Secondly, the performance of the MaxSAT (Maximum Satisfiability) solver is effectively improved by enqueueing all assumptions at once. Furthermore, experiment evaluations on ISCAS85 and ITC99 benchmarks show that compared with D-CMMO, the latest encoding algorithms for MBD, the above two optimization methods effectively reduce the scope of MBD problem, reduce the difficulty of searching for the target solution by the MaxSAT solver, and thus returned diagnostic solution in a shorter time. On average, the solving efficiency of CCM method is improved by 64.5% and 92.8% compared to D-CMMO method respectively.

       

    /

    返回文章
    返回