Analyzing and Debugging Normative Requirements via Satisfiability Checking

• DOI: 10.48550/arxiv.2401.05673
• Publication Date: 2024-01-01
• Authors: Nick Feng; Lina Marsso; Sinem Getir Yaman; Yesugen Baatartog...; Reem Ayad; Victória Oldembur...; Beverley Townsend; Isobel Standen; Ioannis Stefanakos; Calum Imrie; Genaína Nunes Rod...; Ana Cavalcanti; Radu Călinescu; Marsha Chećhik
• Keywords: Sociotechnical system; Workaround; USable; Underpinning

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, cultural (SLEEC) norms values of their stakeholders. Normative non-functional requirements (N-NFRs) are used capture these by setting SLEEC-relevant boundaries for system behavior. Since N-NFRs need be specified multiple stakeholders 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 analysis debugging. N-Check employs satisfiability checking identify broad spectrum well-formedness issues (WFI), conflicts, redundancy, restrictiveness, insufficiency, yielding diagnostics which pinpoint causes user-friendly way that enables understand fix them. We show effectiveness usability our through nine case studies teams ethicists, philosophers, psychologists, safety analysts, engineers analyse debug 233 comprising 62 underpinning operation ranging from assistive-care robots tree-disease detection drones manufacturing collaborative robots.