Logical analysis and contradiction detection in high-level requirements during the review process using sat-solver

DO-178C是航空系统开发过程中的指导标准。该标准不仅要求在软件验证过程中确保需求的一致性，而且将其视为强制性要素。本研究的主要目标是介绍一种使用数据字典获取的信息来分析和识别高层需求之间不一致性的方法。该方法旨在将高层需求转化为逻辑表达式，然后使用SAT求解器进行彻底检查以检测不一致性。虽然文献中经常出现专注于识别需求之间不一致性的方法，但本研究提出了一种新方法来检测非自然语言、系统结构化和语言无关的需求之间的矛盾。该方法的目标是显著减少软件验证过程中高层需求的审核时间。评估表明，使用该方法可以大大节省不一致性检测过程中的时间。

本文旨在介绍一种分析和识别高级需求之间不一致性的方法，以便在软件验证过程中显著减少高级需求的审查时间。这种方法旨在通过使用数据字典中获取的信息，将高级需求转化为逻辑表达式，然后使用SAT求解器进行彻底的检查，以检测不一致性。

本文提出了一种新的方法，可以检测非自然语言、系统化结构和与语言无关的需求之间的矛盾，从而大大减少了高级需求的审查时间。

本文的亮点在于提出了一种新的方法，可以显著减少高级需求的审查时间。通过使用数据字典中获取的信息，将高级需求转化为逻辑表达式，然后使用SAT求解器进行彻底的检查，以检测不一致性。实验结果表明，使用这种方法可以节省大量的时间，并且在软件验证过程中具有广泛的应用前景。

最近在这个领域中，还有一些相关的研究，例如“基于模型的需求工程方法的一致性检查”和“用于检测软件需求不一致性的一种新方法”。