Specification and Analysis of Ethical Requirements in Autonomous Systems Using Abstract State Machines

Autonomous systems are increasingly required to comply with ethical norms and human values, motivating the need for rigorous methods to specify and analyze ethical requirements. Social, Legal, Ethical, Empathetic, and Cultural (SLEEC) rules provide a structured means to encode such requirements; however, ensuring their correctness and well-formedness calls for formal specification and systematic, tool-supported analysis. This paper presents an approach based on Abstract State Machines (ASMs) and the ASMETA tool set for the formal specification and well-formedness analysis of SLEEC requirements. We formally define the semantics of the SLEEC domain-specific language, enabling systematic validation of SLEEC models through conflicts and redundancies detection. Moreover, we extend the core when–then–unless structure of a SLEEC rule with response delays and with a clause unless–until to support the temporary suspension of a rule. The validated ASMETA-based SLEEC model is directly executable and can be readily adopted as a runtime model to support the subsequent phase, namely the operationalization of ethical requirements in autonomous systems.