A computational system is called autonomous if it is able to make its own decisions, or take its own actions, without human supervision or control. The capability and spread of such systems have reached the point where they are beginning to touch much of everyday life. However, regulators grapple with how to deal with autonomous systems, for example how could we certify an Unmanned Aerial System for autonomous use in civilian airspace? We here analyse what is needed in order to provide verified reliable behaviour of an autonomous system, analyse what can be done as the state-of-the-art in automated verification, and propose a roadmap towards developing regulatory guidelines, including articulating challenges to researchers, to engineers, and to regulators. Case studies in seven distinct domains illustrate the article.@en

This extended abstract summarises the contributions from the journal article Fisher et al.@en

The issue of explainability for autonomous systems is becoming increasingly prominent. Several researchers and organisations have advocated the provision of a “Why did you do that?” button which allows a user to interrogate a robot about its choices and actions. We take previous work on debugging cognitive agent programs and apply it to the question of supplying explanations to end users in the form of answers to why-questions. These previous approaches are based on the generation of a trace of events in the execution of the program and then answering why-questions using the trace. We implemented this framework in the agent infrastructure layer and, in particular, the Gwendolen programming language it supports – extending it in the process to handle the generation of applicable plans and multiple intentions. In order to make the answers to why-questions comprehensible to end users we advocate a two step process in which first a representation of an explanation is created and this is subsequently converted into natural language in a way which abstracts away from some events in the trace and employs application specific predicate dictionaries in order to translate the first-order logic presentation of concepts within the cognitive agent program in natural language. A prototype implementation of these ideas is provided.

@en

Increasingly sophisticated mathematical modelling processes from Machine Learning are being used to analyse complex data. However, the performance and explainability of these models within practical critical systems requires a rigorous and continuous verification of their safe utilisation. Working towards addressing this challenge, this paper presents a principled novel safety argument framework for critical systems that utilise deep neural networks. The approach allows various forms of predictions, e.g., future reliability of passing some demands, or confidence on a required reliability level. It is supported by a Bayesian analysis using operational data and the recent verification and validation techniques for deep learning. The prediction is conservative – it starts with partial prior knowledge obtained from lifecycle activities and then determines the worst-case prediction. Open challenges are also identified.

@en

In future inspections of offshore assets utilizing robots, robots will not only be expected to collate new data from their payload of instruments, but they will also be expected to interact with the infrastructure being inspected, undertake remedial tasks and engage with embedded monitoring systems of the asset. This increasing level of interaction and deployment frequency of robot inspections requires an understanding of how we can embed safe and trusted operational architectures within robots. Currently, robots can undertake constrained semi-autonomous inspections, using predetermined tasks (missions) with minimum supervision. However, the challenge is that the state of the world changes with time as does the condition of the robot. Therefore, robots must be able to undertake adaptive measures to support optimal outcomes during autonomous missions. In this paper, we propose an initial architecture to the safe verification and validation of health condition and certification of robotic and autonomous inspection systems for offshore assets. Our first contribution relates to the verification and validation architecture, which takes into account risks associated with asset inspection, safety protocols, evolving ambient changes, as well as the inherent state of health of the robot. The second part of our paper looks to how prognostic analytics can be used to support robot resilience in terms of sensor drift and accurate state of health estimates of critical sub-systems. Initial results demonstrate that methods such as relevance vector machines and Bayesian networks can be used to accurately mitigate risks to autonomy.

@en

The battery is a key component of autonomous robots. Its performance limits the robot’s safety and reliability. Unlike liquid-fuel, a battery, as a chemical device, exhibits complicated features, including (i) capacity fade over successive recharges and (ii) increasing discharge rate as the state of charge (SOC) goes down for a given power demand. Existing formal verification studies of autonomous robots, when considering energy constraints, formalise the energy component in a generic manner such that the battery features are overlooked. In this paper, we model an unmanned aerial vehicle (UAV) inspection mission on a wind farm and via probabilistic model checking in PRISM show (i) how the battery features may affect the verification results significantly in practical cases; and (ii) how the battery features, together with dynamic environments and battery safety strategies, jointly affect the verification results. Potential solutions to explicitly integrate battery prognostics and health management (PHM) with formal verification of autonomous robots are also discussed to motivate future work.

@en

Robots are increasingly used to carry out critical missions in extreme environments that are hazardous for humans. This requires a high degree of operational autonomy under uncertain conditions, and poses new challenges for assuring the robot's safety and reliability. In this paper, we develop a framework for probabilistic model checking on a layered Markov model to verify the safety and reliability requirements of such robots, both at pre-mission stage and during runtime. Two novel estimators based on conservative Bayesian inference and imprecise probability model with sets of priors are introduced to learn the unknown transition parameters from operational data. We demonstrate our approach using data from a real-world deployment of unmanned underwater vehicles in extreme environments.

@en

Autonomous systems are increasingly being used in safety-and mission-critical domains, including aviation, manufacturing, healthcare and the automotive industry. Systems for such domains are often verified with respect to essential requirements set by a regulator, as part of a process called certification. In principle, autonomous systems can be deployed if they can be certified for use. However, certification is especially challenging as the condition of both the system and its environment will surely change, limiting the effective use of the system. In this paper we discuss the technological and regulatory background for such systems, and introduce an architectural framework that supports verifiably-correct dynamic self-certification by the system, potentially allowing deployed systems to operate more safely and effectively.

@en

We address the question of how an agent can adapt its behavior to comply with newly adopted norms. This is particularly relevant in the case of open systems where agents may enter and leave norm-governed social contexts not known at design time. This requires norms to be explicitly and separately stated and presented to an agent as rules to which it then can try to adapt its behavior.
We propose a formal semantic framework that specifies an execution mechanism for such socially adaptive agents. This framework is based on expressing norms using Linear Temporal Logic. The formality of the framework allows us to rigorously study its norm compliance properties. A weak form of norm compliance allows agents to abort execution in order to prevent norm violation. In this paper we investigate a stronger notion of norm compliance that is evaluated over infinite traces. We show that it is not possible for all agents to be strongly compliant with any arbitrary set of norms. We then investigate situations when strong norm compliance can be guaranteed.@en