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

TL;DR

This paper introduces a SAT solver-based method for analyzing high-level requirements to detect contradictions efficiently, aiming to reduce review time in aviation software verification.

Contribution

It presents a novel, language-independent approach for contradiction detection in structured requirements using logical transformation and SAT solving.

Findings

Significant reduction in review time for requirements verification.

Effective detection of contradictions in non-natural language requirements.

Method demonstrates practical efficiency in aviation standards compliance.

Abstract

DO-178C stands out as a guiding standard for aviation system development processes. This standard not only mandates ensuring the consistency of requirements in the software verification process but also recognizes it as a mandatory element. The main objective of this study is to introduce a method for analyzing and identifying inconsistencies between high-level requirements using information obtained from a data dictionary. This method aims to transform high-level requirements into logical expressions and then thoroughly examine them using a SAT Solver to detect inconsistencies. While methods focused on identifying inconsistencies among requirements often appear in the literature, this study presents a novel approach to detect contradictions between non-natural language, systematically structured, and language-independent requirements. The goal of this approach is to significantly reduce the review time of high-level requirements in the software verification process. Evaluations indicate that the use of this method results in substantial time savings in the inconsistency detection process.