  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.
