Analyzing and Debugging Normative Requirements via Satisfiability Checking

TY - GEN

T1 - Analyzing and Debugging Normative Requirements via Satisfiability Checking

AU - Feng, Nick

AU - Marsso, Lina

AU - Getir Yaman, Sinem

AU - Townsend, Bev

AU - Baatartogtokh, Yesugen

AU - Ayad, Reem

AU - Oldemburgo de Mello, Victória

AU - Standen, Isobel

AU - Stefanakos, Ioannis

AU - Imrie, Calum Corrie

AU - Nunes Rodrigues, Genaína

AU - Cavalcanti, Ana Lucia Caneca

AU - Calinescu, Radu

AU - Chechik, Marsha

N1 - Publisher Copyright: © 2024 ACM.

PY - 2024/4/12

Y1 - 2024/4/12

N2 - 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 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.

AB - 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 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.

KW - Requirement Engineering

KW - Satisfiability

UR - http://www.scopus.com/inward/record.url?scp=85196820186&partnerID=8YFLogxK

U2 - 10.1145/3597503.3639093

DO - 10.1145/3597503.3639093

M3 - Conference contribution

AN - SCOPUS:85196820186

T3 - Proceedings - International Conference on Software Engineering

SP - 2643

EP - 2654

BT - 46th International Conference on Software Engineering (ICSE 2024)

PB - IEEE Computer Society

T2 - 44th ACM/IEEE International Conference on Software Engineering, ICSE 2024

Y2 - 14 April 2024 through 20 April 2024

ER -