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.

Autonomous systems are often used in applications where environmental and internal changes may lead to requirement violations. Adapting to these changes proactively, i.e., before the violations occur, is preferable to recovering from the failures that may be caused by such violations. However, proactive adaptation needs methods for predicting requirement violations timely, accurately, and with acceptable overheads. To address this need, we present a method that allows autonomous systems to predict violations of performance, dependability and other nonfunctional requirements, and therefore take preventative measures to avoid or otherwise mitigate them. Our method for pre dicting these autonomou s sys t em disrupti o ns (PRESTO) comprises a design time stage and a run-time stage. At design-time, we use parametric model checking to obtain algebraic expressions that formalise the relationships between the nonfunctional properties of the requirements of interest (e.g., reliability, response time, and energy use) and the parameters of the system and its environment. At run-time, we predict future changes in these parameters by applying piece-wise linear regression to online data obtained through monitoring, and we use the algebraic expressions to predict the impact of these changes on the system requirements. We demonstrate the application of PRESTO through simulation in case studies from two different domains.

Normative non-functional requirements specify constraints 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 complementary 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 operationalization through a range of real-world case studies.

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.

Recent advances in generative AI and machine learning have stirred up fears about the unbridled adoption of autonomous, self-adaptive decision mechanisms in socio-technical systems. This vision paper explores the critical relationship between software-intensive systems and the empowerment of humans as individuals and society. We highlight the need for human empowerment within the context of self-adaptive socio-technical systems (SASTSs), which require mechanisms for balancing of diverse needs, values, and ethics on the individual, community, and societal levels. We propose an architecture comprised of Connector and Mediator elements, and third-party auditing, to support interactions and ensure preservation of human needs, values, and ethics. We use an example of Robot-Assisted A&E Triage system to motivate and illustrate our work and discuss some open challenges for future research.

A growing range of applications use autonomous agents such as AI and robotic systems to perform tasks deemed dangerous, tedious or costly for humans. To truly succeed with these tasks, the autonomous agents must perform them without violating the social, legal, ethical, empathetic, and cultural (SLEEC) norms of their users and operators. We introduce SLEECVAL, a tool for specification and validation of rules that reflect these SLEEC norms. Our tool supports the specification of SLEEC rules in a DSL [1] we co-defined with the help of ethicists, lawyers and stakeholders from health and social care, and uses the CSP refinement checker FDR4 to identify redundant and conflicting rules in a SLEEC specification. We illustrate the use of SLEECVAL for two case studies: an assistive dressing robot, and a firefighting drone.

Deep neural networks (DNNs) are increasingly used in safety-critical autonomous systems as perception components processing high-dimensional image data. Formal analysis of these systems is particularly challenging due to the complexity of the perception DNNs, the sensors (cameras), and the environment conditions. We present a case study applying formal probabilistic analysis techniques to an experimental autonomous system that guides airplanes on taxiways using a perception DNN. We address the above challenges by replacing the camera and the network with a compact abstraction whose transition probabilities are computed from the confusion matrices measuring the performance of the DNN on a representative image data set. As the probabilities are estimated based on empirical data, and thus are subject to error, we also compute confidence intervals in addition to point estimates for these probabilities and thereby strengthen the soundness of the analysis. We also show how to leverage local, DNN-specific analyses as run-time guards to filter out mis-behaving inputs and increase the safety of the overall system. Our findings are applicable to other autonomous systems that use complex DNNs for perception.

Despite considerable research efforts on handling uncertainty in self-adaptive systems, a comprehensive understanding of the precise nature of uncertainty is still lacking. This paper summarises the findings of the 2023 Bertinoro Seminar on Uncertainty in Self- Adaptive Systems, which aimed at thoroughly investigating the notion of uncertainty, and outlining open challenges associated with its handling in self-adaptive systems. The seminar discussions were centered around five core topics: (1) agile end-toend handling of uncertainties in goal-oriented self-adaptive systems, (2) managing uncertainty risks for self-adaptive systems, (3) uncertainty propagation and interaction, (4) uncertainty in self-adaptive machine learning systems, and (5) human empowerment under uncertainty. Building on the insights from these discussions, we propose a research agenda listing key open challenges, and a possible way forward for addressing them in the coming years.

The fairness of human‐related software has become critical with its widespread use in our daily lives, where life‐changing decisions are made. However, with the use of these systems, many erroneous results emerged. Technologies have started to be developed to tackle unexpected results. As for the solution to the issue, companies generally focus on algorithm‐oriented errors. The utilized solutions usually only work in some algorithms. Because the cause of the problem is not just the algorithm; it is also the data itself. For instance, deep learning cannot establish the cause–effect relationship quickly. In addition, the boundaries between statistical or heuristic algorithms are unclear. The algorithm's fairness may vary depending on the data related to context. From this point of view, our article focuses on how the data should be, which is not a matter of statistics. In this direction, the picture in question has been revealed through a scenario specific to “vulnerable and disadvantaged” groups, which is one of the most fundamental problems today. With the joint contribution of computer science and social sciences, it aims to predict the possible social dangers that may arise from artificial intelligence algorithms using the clues obtained in this study. To highlight the potential social and mass problems caused by data, Gerbner's “cultivation theory” is reinterpreted. To this end, we conduct an experimental evaluation on popular algorithms and their data sets, such as Word2Vec, GloVe, and ELMO. The article stresses the importance of a holistic approach combining the algorithm, data, and an interdisciplinary assessment.

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.

Developing resilient autonomous systems requires an interdisciplinary approach that can understand performance variability and respond to critical events when they occur. Resilience within autonomous systems must also account for social norms as well as broader ethical and legal considerations. Within this paper we outline the importance of embedding Social, Legal, Ethical, Empathetic and Cultural (SLEEC) constraints within the development of future autonomous systems. A novel methodological approach is presented that combines Human Factors methods with Computer Science techniques to generate the environmental and situational requirements in combination with a computer rule-based requirements language. This approach also provides a possible structure for capturing contextual and situational information from key stakeholders in the development of autonomous systems. This structure will enable engagement with the stakeholders with respect to key elements identified from this interdisciplinary approach in a responsible way to ensure that future autonomous systems are user centred. The approach is domain independent, but it is applied here to the case of an autonomous assistive dressing robot that aids a user in a dressing task, with a specific critical event that requires a SLEEC resilient response

In this article, we introduce a probabilistic verification algorithm for stochastic regular expressions over a probabilistic extension of the Action based Computation Tree Logic (ACTL*). The main results include a novel model checking algorithm and a semantics on the probabilistic action logic for stochastic regular expressions (SREs). Specific to our model checking algorithm is that SREs are defined via local probabilistic functions. Such functions are beneficial since they enable to verify properties locally for sub-components. This ability provides a flexibility to reuse the local results for the global verification of the system; hence, the framework can be used for iterative verification. We demonstrate how to model a system with an SRE and how to verify it with the probabilistic action based logic and present a preliminary performance evaluation with respect to the execution time of the reachability algorithm.

This special issue contains articles selected from CS&P 2018, the 27th Workshop on Concurrency, Specification, and Programming. CS&P deals with formal specification of concurrent and parallel systems, mathematical models for describing such systems, and programming and verification concepts for their implementation. The workshop is one of a series of events organised every even year by Humboldt University of Berlin and every odd year by Warsaw University. Dating back to the midseventies, CS&P has become an important forum for researchers from European and Asian countries. CS&P 2018 was held at Humboldt University Berlin-Adlershof, Germany, in September 24-26, 2018, and featured 20 papers accepted for presentation by the program committee. After the conference, six outstanding papers were selected by the Steering Committee based on the previous reviews and the quality of the presentations. Their authors were given time to integrate the reviewer’s and audience’s feedback, as well as to substantially improve and extend their contributions. After the second round of reviewing by additional experts, during the pandemic year of 2020 the authors polished and finalized their contributions, to yield the mature articles which can be found in this special issue.

Trends such as globalisation, standardisation and shorter life-cycles place great demands on the flexibility of the software industry. In order to compete and cooperate on an international scale, a constantly decreasing time to market and an increasing level of quality are essential. Testing is at the moment the most important and mostly used quality assurance technique applied in industry. However, the complexity of software and hence of their development amount is increasing. Modern systems get larger and more complex, as they connect large amounts of components that interact in many different ways and have constantly changing and different types of requirements (functionality, dependability, usability, performance etc.). Data processing that impacts all aspects of our life is increasingly distributed over clouds and devices. This leads to new concerns, such as availability, security, and privacy, which are aspects that also needs to be tested. Consequently, the development of cost-effective and high-quality systems opens new challenges that cannot be faced only with traditional testing approaches, and specifically manual testing is simply insufficient and unreliable to manage the speed needed, and ensure the coverage of ever-changing systems. New techniques for systematization and automation of testing throughout the software and system life-cycle are required.

Successful system evolution is dependent on knowledge about the system itself, its past and its present, as well as the environment of the system. This chapter presents several approaches to automate the acquisition of knowledge about the system's past, for example past evolution steps, and its present, for example models of its behaviour. Based on these results, further approaches support the validation and verification of evolution steps, as well as the recommendation of evolutions to the system, as well as similar systems. The approaches are illustrated using the joint automation production system case study, the Pick and Place Unit (PPU) and Extended Pick and Place Unit (xPPU).

During the whole life-cycle of software-intensive systems in safety-critical domains, system models must consistently co-evolve with quality evaluation models like fault trees. However, performing these co-evolution steps is a cumbersome and often manual task. To understand this problem in detail, we have analyzed the evolution and mined common changes of architecture and fault tree models for a set of evolution scenarios of a part of a factory automation system called Pick and Place Unit. On the other hand, we designed a set of intra- and inter-model transformation rules which fully cover the evolution scenarios of the case study and which offer the potential to semi-automate the co-evolution process. In particular, we validated these rules with respect to completeness and evaluated them by a comparison to typical visual editor operations. Our results show a significant reduction of the amount of required user interactions in order to realize the co-evolution. (C) 2018 Elsevier Inc. All rights reserved.

State elimination has been proposed in the literature as a viable technique for transforming finite state automata (or finite state machines) into equivalent regular expressions. In this TTC case, we consider this well-known technique as a model transformation problem, aiming at evaluating the suitability, performance and scalability of dedicated model transformation techniques w.r.t. this problem.