Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s>  <s> In this paper we assess the feasibility of using formal methods, and model checking in particular, for the certification of Unmanned Aircraft Systems (UAS) within civil airspace. We begin by modelling a basic UAS control system in PROMELA, and verify it against a selected subset of the CAA's Rules of the Air using the SPIN model checker. Next we build a more advanced UAS control system using the autonomous agent language Gwendolen, and verify it against the small subset of the Rules of the Air using the agent model checker AJPF. We introduce more advanced autonomy into the UAS agent and show that this too can be verified. Finally we compare and contrast the various approaches, discuss the paths towards full certification, and present directions for future research. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s>  <s> Human‐robot teams are likely to be used in a variety of situations wherever humans require the assistance of robotic systems. Obvious examples include healthcare and manufacturing, in which people need the assistance of machines to perform key tasks. It is essential for robots working in close proximity to people to be both safe and trustworthy. In this paper we examine formal verification of a high-level planner/scheduler for autonomous personal robotic assistants such as CareO-bot R . We describe how a model of Care-O-bot and its environment was developed using Brahms, a multiagent workflow language. Formal verification was then carried out by translating this to the input language of an existing model checker. Finally we present some formal verification results and describe how these could be complemented by simulation-based testing and realworld end-user validation in order to increase the practical and perceived safety and trustworthiness of robotic assistants. <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s>  <s> The development and deployment of Autonomous Vehicles (AVs) on our roads is not only realistic in the near future but can also bring significant benefits. In particular, it can potentially solve several problems relating to vehicles and traffic, for instance: (i) possible reduction of traffic congestion, with the consequence of improved fuel economy and reduced driver inactivity; (ii) possible reduction in the number of accidents, assuming that an AV can minimise the human errors that often cause traffic accidents; and (iii) increased ease of parking, especially when one considers the potential for shared AVs. In order to deploy an AV there are significant steps that must be completed in terms of hardware and software. As expected, software components play a key role in the complex AV system and so, at least for safety, we should assess the correctness of these components. In this paper, we are concerned with the high-level software component(s) responsible for the decisions in an AV. We intend to model an AV capable of navigation; obstacle avoidance; obstacle selection (when a crash is unavoidable) and vehicle recovery, etc, using a rational agent. To achieve this, we have established the following stages. First, the agent plans and actions have been implemented within the Gwendolen agent programming language. Second, we have built a simulated automotive environment in the Java language. Third, we have formally specified some of the required agent properties through LTL formulae, which are then formally verified with the AJPF verification tool. Finally, within the MCAPL framework (which comprises all the tools used in previous stages) we have obtained formal verification of our AV agent in terms of its specific behaviours. For example, the agent plans responsible for selecting an obstacle with low potential damage, instead of a higher damage obstacle (when possible) can be formally verified within MCAPL. We must emphasise that the major goal (of our present approach) lies in the formal verification of agent plans, rather than evaluating real-world applications. For this reason we utilised a simple matrix representation concerning the environment used by our agent. <s> BIB003
are complex, inherently hybrid, systems, combining both hardware and software; they often require close safety, legal, and ethical considerations. Autonomous robotics are increasingly being used in commonplace scenarios, such as driverless cars BIB003 , pilotless aircraft BIB001 , and domestic assistants  BIB002 . While for many engineered systems testing, either through real deployment or via simulation, is deemed sufficient, the unique challenges of autonomous robotics, their dependence on sophisticated software control and decision making, and their increasing deployment in safety-critical scenarios require a stronger form of verification. This leads us toward using formal methods, which are mathematically based techniques for the specification and verification of software systems, to ensure the correctness of, and provide sufficient evidence for the certification of, robotic systems. We contribute an overview and analysis of the state of the art in formal specification and verification of autonomous robotics. Section 1.1 outlines the scope, research questions, and search criteria for our survey. Section 1.2 describes related work concerning formal methods for robotics and differentiates them from our work. We recognize the important role that middleware architectures and non-and semiformal techniques have in the development of reliable robotics and we briefly summarize some of these techniques in Section 2. The specification and verification challenges raised by autonomous robotic systems are discussed next: Section 3 describes the challenges of their context (the external challenges) and Section 4 describes the challenges of their organization (the internal challenges). Section 5 discusses the formalisms used in the literature for specification and verification of autonomous robotics. Section 6 characterizes the approaches to formal specification and verification of autonomous robotics found in the literature. Finally, Section 7 discusses the results of our survey and presents our observations on the future directions of formal methods for autonomous robotic systems.