Abstract Autonomous agents are increasingly deployed in sensitive, human-centric domains—such as healthcare, assistive care, and emergency response—where their decision-making must align with complex human norms. These translate into Social, Legal, Ethical, Empathetic, and Cultural (SLEEC) requirements that are often nuanced and context-dependent, challenging traditional software engineering paradigms. Our tutorial paper presents a comprehensive, tool-supported methodology for managing the SLEEC requirements lifecycle, covering elicitation, well-formedness validation, and conformance verification of software design models against SLEEC requirements. We demonstrate the use of our methodology and associated tools through application to a robot-assisted dressing system, providing a guide for researchers and engineers to bridge the gap between abstract human norms and verifiable system designs.

Autonomous agents are increasingly being proposed for use in healthcare, assistive care, education, and other applications governed by complex human-centric norms. To ensure compliance with these norms, the rules they induce need to be unambiguously defined, checked for consistency, and used to verify the agent. In this paper, we introduce a framework for formal specification, validation and verification of social, legal, ethical, empathetic and cultural (SLEEC) rules for autonomous agents. Our framework comprises: (i) a language for specifying SLEEC rules and rule defeaters (that is, circumstances in which a rule does not apply or an alternative form of the rule is required); (ii) a formal semantics (defined in the process algebra tock-CSP) for the language; and (iii) methods for detecting conflicts and redundancy within a set of rules, and for verifying the compliance of an autonomous agent with such rules. We show the applicability of our framework for two autonomous agents from different domains: a firefighter UAV, and an assistive-dressing robot.

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.

Normative non-functional requirements specify con-straints that a system must observe in order to avoid violations of social, legal, ethical, empathetic, and cultural norms. As these requirements are typically defined by non-technical system stakeholders with different expertise and priorities (ethicists, lawyers, social scientists, etc.), ensuring their well-formedness and consistency is very challenging. Recent research has tackled this challenge using a domain-specific language to specify normative requirements as rules whose consistency can then be analysed with formal methods. In this paper, we propose a complemen-tary approach that uses Large Language Models to extract semantic relationships between abstract representations of system capabilities. These relations, which are often assumed implicitly by non-technical stakeholders (e.g., based on common sense or domain knowledge), are then used to enrich the automated reasoning techniques for eliciting and analyzing the consistency of normative requirements. We show the effectiveness of our approach to normative requirements elicitation and operational-ization through a range of real-world case studies. An extended version of this paper, which includes appendices is available at https://arxiv.org/abs/2404.12335

As software and cyber-physical systems interacting with humans become prevalent in domains such as healthcare, education and customer service, software engineers need to consider normative (i.e., social, legal, ethical, empathetic and cultural) requirements. However, their elicitation is challenging, as they must reflect the often conflicting or redundant views of stakeholders ranging from users and operators to lawyers, ethicists and regulators. To address this challenge, we introduce a tool-supported Formal framework for normaTive requirements elicitation (FormaTive). It allows specification of normative rules for a software system in an intuitive high-level language, and automates: (i) the mapping of the rules to an internal formal representation; (ii) their analysis to identify rule conflicts, redundancies, and concerns; and (iii) the synthesis of feedback enabling users to understand and resolve problems.