Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Analyzing and Debugging Normative Requirements via Satisfiability Checking

Nick Feng, Lina Marsso, Sinem Getir Yaman, Yesugen Baatartogtokh, Reem Ayad, Victória Oldemburgo de Mello, Beverley Townsend, Isobel Standen, Ioannis Stefanakos, Calum Imrie, Genaína Nunes Rodrigues, Ana Cavalcanti, Radu Calinescu, Marsha Chechik

TL;DR

This work tackles the challenge of eliciting and validating normative non-functional requirements (N-NFRs) that encode social, legal, ethical, and cultural (SLEEC) norms. It introduces N-Check, a SAT-based pipeline that converts SLEEC DSL rules into FOL$^*$ constraints to detect well-formedness issues (redundancy, vacuous and situational conflicts, restrictiveness, insufficiency) and to generate non-technical diagnostic traces. A key contribution is the combination of emptiness-based analyses with causal FOL$^*$ proofs to identify root causes and provide actionable guidance for non-technical stakeholders, aided by the LEGOS-SLEEC tool. The approach is validated on nine real-world case studies, covering 233 N-NFRs and 62 issues, demonstrating effective detection and practical usefulness for elicitation, reasoning, and debugging in ethical, safe, and compliant system design. Overall, N-Check enables on-the-fly analysis and patch-driven refinement of normative requirements, bridging technical and non-technical perspectives in modern socio-technical systems.

Abstract

As software systems increasingly interact with humans in application domains such as transportation and healthcare, they raise concerns related to the social, legal, ethical, empathetic, and cultural (SLEEC) norms and values of their stakeholders. Normative non-functional requirements (N-NFRs) are used to capture these concerns by setting SLEEC-relevant boundaries for system behavior. Since N-NFRs need to be specified by multiple stakeholders with widely different, non-technical expertise (ethicists, lawyers, regulators, end users, etc.), N-NFR elicitation is very challenging. To address this challenge, we introduce N-Check, a novel tool-supported formal approach to N-NFR analysis and debugging. N-Check employs satisfiability checking to identify a broad spectrum of N-NFR well-formedness issues (WFI), such as conflicts, redundancy, restrictiveness, insufficiency, yielding diagnostics which pinpoint their causes in a user-friendly way that enables non-technical stakeholders to understand and fix them. We show the effectiveness and usability of our approach through nine case studies in which teams of ethicists, lawyers, philosophers, psychologists, safety analysts, and engineers used N-Check to analyse and debug 233 N-NFRs comprising 62 issues for the software underpinning the operation of systems ranging from assistive-care robots and tree-disease detection drones to manufacturing collaborative robots.

Analyzing and Debugging Normative Requirements via Satisfiability Checking

TL;DR

This work tackles the challenge of eliciting and validating normative non-functional requirements (N-NFRs) that encode social, legal, ethical, and cultural (SLEEC) norms. It introduces N-Check, a SAT-based pipeline that converts SLEEC DSL rules into FOL constraints to detect well-formedness issues (redundancy, vacuous and situational conflicts, restrictiveness, insufficiency) and to generate non-technical diagnostic traces. A key contribution is the combination of emptiness-based analyses with causal FOL proofs to identify root causes and provide actionable guidance for non-technical stakeholders, aided by the LEGOS-SLEEC tool. The approach is validated on nine real-world case studies, covering 233 N-NFRs and 62 issues, demonstrating effective detection and practical usefulness for elicitation, reasoning, and debugging in ethical, safe, and compliant system design. Overall, N-Check enables on-the-fly analysis and patch-driven refinement of normative requirements, bridging technical and non-technical perspectives in modern socio-technical systems.

Abstract

As software systems increasingly interact with humans in application domains such as transportation and healthcare, they raise concerns related to the social, legal, ethical, empathetic, and cultural (SLEEC) norms and values of their stakeholders. Normative non-functional requirements (N-NFRs) are used to capture these concerns by setting SLEEC-relevant boundaries for system behavior. Since N-NFRs need to be specified by multiple stakeholders with widely different, non-technical expertise (ethicists, lawyers, regulators, end users, etc.), N-NFR elicitation is very challenging. To address this challenge, we introduce N-Check, a novel tool-supported formal approach to N-NFR analysis and debugging. N-Check employs satisfiability checking to identify a broad spectrum of N-NFR well-formedness issues (WFI), such as conflicts, redundancy, restrictiveness, insufficiency, yielding diagnostics which pinpoint their causes in a user-friendly way that enables non-technical stakeholders to understand and fix them. We show the effectiveness and usability of our approach through nine case studies in which teams of ethicists, lawyers, philosophers, psychologists, safety analysts, and engineers used N-Check to analyse and debug 233 N-NFRs comprising 62 issues for the software underpinning the operation of systems ranging from assistive-care robots and tree-disease detection drones to manufacturing collaborative robots.
Paper Structure (22 sections, 9 theorems, 11 figures, 6 tables)

This paper contains 22 sections, 9 theorems, 11 figures, 6 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Normalized Representation of SLEEC DSL
  4. FOL$^*$ Satisfiability Checking
  5. Well-Formedness Properties
  6. Well-formedness and Satisfiability
  7. Well-formedness via Emptiness Checking
  8. Encoding SLEEC DSL Rules & Facts in FOL$^*$
  9. Situational Conflicts via Satisfiability
  10. The N-Check Approach
  11. Diagnosis for Well-formedness
  12. Causal FOL$^*$ Proof
  13. Diagnosis for Redundancy, Vacuous and Situational Conflict, and Restrictiveness
  14. Other Diagnoses
  15. Evaluation
  16. ...and 7 more sections

Key Result

Lemma 1

Let a set of rules $\textit{Rules}$ be given. A rule $r \in \textit{Rules}$ is vacuously conflicting if and only if $\mathcal{L}(\textit{Rules}) \cap \mathcal{L}(\textsc{Trig}(r))$ is empty.

Figures (11)

  • Figure 1: Overview of the N-Check approach.
  • Figure 2: Five traces from the dressing robot example. $\sigma_0^2$ is a partial trace, from 0 to 2, used to illustrate situational-conflicts.
  • Figure 3: The relationship between different states of obligations.
  • Figure 4: Redundancy diagnosis for Ex. \ref{['exmaple:redudent']}: a redundant rule $r5$ together with the set of rules $\{r6, r7\}$ with which $r5$ is redundant. Redundant clauses are highlighted.
  • Figure 5: Insufficiency diagnosis for Ex. \ref{['example:inssuficent']}: a trace where a concern is raised while respecting the rules.
  • ...and 6 more figures

Theorems & Definitions (44)

  • Example 1
  • Example 2
  • Definition 1: Behaviour defined by $\textit{Rules}$
  • Example 3
  • Definition 2: Redundancy
  • Example 4
  • Definition 3: Vacuous Conflict
  • Example 5
  • Definition 4: Fact
  • Definition 5: Restrictiveness
  • ...and 34 more