Analyzing and Debugging Normative Requirements via Satisfiability Checking

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution


As software systems increasingly interact with humans in appli-
cation domains such as transportation and healthcare, they raise
concerns related to the social, legal, ethical, empathetic, and cul-
tural (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 behav-
ior. 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 difficult task, 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, such as conflicts, redundancy,
restrictiveness, and insufficiency, yielding diagnostics that pinpoint
their causes in a user-friendly way that enables non-technical stake-
holders 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, such as, assistive-care robots and tree-disease detection
drones to manufacturing collaborative robots.
Original languageEnglish
Title of host publication46th International Conference on Software Engineering (ICSE 2024)
Publication statusPublished - 2024

Cite this