Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational Objects

Nick Feng, Lina Marsso, Marsha Chechik

TL;DR

This work implemented the proposed proof support on top of the state-of-the-art FOL* satisfiability checker to generate proofs of UNSAT and validated the approach by applying the proof-based diagnoses to explain the causes of well-formedness issues of normative requirements of software systems.

Abstract

Satisfiability-based automated reasoning is an approach that is being successfully used in software engineering to validate complex software, including for safety-critical systems. Such reasoning underlies many validation activities, from requirements analysis to design consistency to test coverage. While generally effective, the back-end constraint solvers are often complex and inevitably error-prone, which threatens the soundness of their application. Thus, such solvers need to be validated, which includes checking correctness and explaining (un)satisfiability results returned by them. In this work, we consider satisfiability analysis based on First-Order Logic with relational objects (FOL*) which has been shown to be effective for reasoning about time- and data-sensitive early system designs. We tackle the challenge of validating the correctness of FOL* unsatisfiability results and deriving diagnoses to explain the causes of the unsatisfiability. Inspired by the concept of proofs of UNSAT from SAT/SMT solvers, we define a proof format and proof rules to track the solvers' reasoning steps as sequences of derivations towards UNSAT. We also propose an algorithm to verify the correctness of FOL* proofs while filtering unnecessary derivations and develop a proof-based diagnosis to explain the cause of unsatisfiability. We implemented the proposed proof support on top of the state-of-the-art FOL* satisfiability checker to generate proofs of UNSAT and validated our approach by applying the proof-based diagnoses to explain the causes of well-formedness issues of normative requirements of software systems.

Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational Objects

TL;DR

This work implemented the proposed proof support on top of the state-of-the-art FOL* satisfiability checker to generate proofs of UNSAT and validated the approach by applying the proof-based diagnoses to explain the causes of well-formedness issues of normative requirements of software systems.

Abstract

Satisfiability-based automated reasoning is an approach that is being successfully used in software engineering to validate complex software, including for safety-critical systems. Such reasoning underlies many validation activities, from requirements analysis to design consistency to test coverage. While generally effective, the back-end constraint solvers are often complex and inevitably error-prone, which threatens the soundness of their application. Thus, such solvers need to be validated, which includes checking correctness and explaining (un)satisfiability results returned by them. In this work, we consider satisfiability analysis based on First-Order Logic with relational objects (FOL*) which has been shown to be effective for reasoning about time- and data-sensitive early system designs. We tackle the challenge of validating the correctness of FOL* unsatisfiability results and deriving diagnoses to explain the causes of the unsatisfiability. Inspired by the concept of proofs of UNSAT from SAT/SMT solvers, we define a proof format and proof rules to track the solvers' reasoning steps as sequences of derivations towards UNSAT. We also propose an algorithm to verify the correctness of FOL* proofs while filtering unnecessary derivations and develop a proof-based diagnosis to explain the cause of unsatisfiability. We implemented the proposed proof support on top of the state-of-the-art FOL* satisfiability checker to generate proofs of UNSAT and validated our approach by applying the proof-based diagnoses to explain the causes of well-formedness issues of normative requirements of software systems.
Paper Structure (15 sections, 2 theorems, 15 equations, 4 figures, 5 tables, 2 algorithms)

This paper contains 15 sections, 2 theorems, 15 equations, 4 figures, 5 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Background
  3. Proof of UNSAT
  4. FOL$^*$ Proof of Unsatisfiability
  5. Interfacing with the Background Theories
  6. FOL$^*$ Derivation Rules
  7. Derivation Macros
  8. Checking FOL$^*$ Proof of Unsatisfiability
  9. Diagnosing FOL$^*$ Unsatisfiability
  10. Supporting Proof of UNSAT for LEGOS
  11. Evaluation
  12. Related Work
  13. Conclusion
  14. FOL$^*$ Derivation Rules
  15. Expansion of Derivation Macros

Key Result

theorem 1

Let a set of FOL$^*$ formulas $R$ and a proof $L=d_1 \ldots d_n$ be given. Suppose $s_0$ is the initial proof state for $R$ and $s_n = s_0\circ d_1 \circ \ldots d_n$ is the final proof state after applying every derivation rule in $L$. If (1) every derivation step is sound, (2) $s_n:=(R_n, F_n, D_n)

Figures (4)

  • Figure 1: FOL$^{*+}$ semantics. $D_r$ defines the set of all relational objects of class $r$ in $D$.
  • Figure 2: The full list of FOL$^*$-specific derivation rules with their names, enabling condition $PC_{\textit{Name}}$, and the dependencies of the derived resources (i.e., $\textbf{Dep}(r)$ where $r$ is a resource derived by an application of the rule Name). $\overline{l}$ refers to the complement of the literal $l$ (e.g., $\overline{\textit{DEF}(\phi)}$).
  • Figure 3: Proof of UNSAT for $\phi$ in Example \ref{['example:proof']}. For each derivation step, $\#$ is the step number, Name is the name of the applied derivation rule, Dependencies is the dependant resources $Dep'$ for each step, and Effect is the resulting state after the derivation. The resources in blue are newly derived in each step.
  • Figure 4: Redundancy diagnosis example.

Theorems & Definitions (13)

  • definition 1: State Satisfiability
  • definition 2: Derivation Soundness
  • theorem 1: Partial Soundness
  • definition 3
  • definition 4
  • definition 5
  • definition 6: Definition Variable
  • definition 7: Proof-Specific UNSAT Diagnosis
  • definition 8: Active Atoms
  • definition 9: Atom-level Proof-Specific Diagnosis
  • ...and 3 more