Analyzing and Debugging Normative Requirements via Satisfiability Checking
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 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 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, such as, assistive-care robots and tree-disease detection drones to manufacturing collaborative robots.
BibTeX
@inproceedings{Feng-al:ICSE24,
author = {Nick Feng and
Lina Marsso and
Sinem Getir Yaman and
Yesugen Baatartogtokh and
Reem Ayad and
Vict{\'{o}}ria Oldemburgo de Mello and
Beverley A. Townsend and
Isobel Standen and
Ioannis Stefanakos and
Calum Imrie and
Gena{\'{\i}}na Nunes Rodrigues and
Ana Cavalcanti and
Radu Calinescu and
Marsha Chechik},
title = {Analyzing and Debugging Normative Requirements via Satisfiability Checking},
booktitle = {ICSE},
pages = {214:1--214:12},
publisher = {{ACM}},
year = {2024},
}