Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Model Checking <s> We describe a method for using abstraction to reduce the complexity of temporal-logic model checking. Using techniques similar to those involved in abstract interpretation, we construct an abstract model of a program without ever examining the corresponding unabstracted model. We show how this abstract model can be used to verify properties of the original program. We have implemented a system based on these techniques, and we demonstrate their practicality using a number of examples, including a program representing a pipelined ALU circuit with over 10 1300 states. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Model Checking <s> The majority of the work carried out in the formal methods community throughout the last three decades has (for good reasons) been devoted to special languages designed to make it easier to experiment with mechanized formal methods such as theorem provers and model checkers. In this paper, we give arguments for why we believe it is time for the formal methods community to shift some of its attention towards the analysis of programs written in modern programming languages. In keeping with this philosophy, we have developed a verification and testing environment for Java, called Java PathFinder (JPF), which integrates model checking, program analysis and testing. Part of this work has consisted of building a new Java Virtual Machine that interprets Java bytecode. JPF uses state compression to handle large states, and partial order reduction, slicing, abstraction and run-time analysis techniques to reduce the state space. JPF has been applied to a real-time avionics operating system developed at Honeywell, illustrating an intricate error, and to a model of a spacecraft controller, illustrating the combination of abstraction, run-time analysis and slicing with model checking. <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Model Checking <s> The state explosion problem remains a major hurdle in applying symbolic model checking to large hardware designs. State space abstraction, having been essential for verifying designs of industrial complexity, is typically a manual process, requiring considerable creativity and insight.In this article, we present an automatic iterative abstraction-refinement methodology that extends symbolic model checking. In our method, the initial abstract model is generated by an automatic analysis of the control structures in the program to be verified. Abstract models may admit erroneous (or "spurious") counterexamples. We devise new symbolic techniques that analyze such counterexamples and refine the abstract model correspondingly. We describe aSMV, a prototype implementation of our methodology in NuSMV. Practical experiments including a large Fujitsu IP core design with about 500 latches and 10000 lines of SMV code confirm the effectiveness of our approach. <s> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Model Checking <s> Michigan/AFRL Collaborative Center on Control Sciences, AFOSR (grant no. FA 8650-07-2-3744) <s> BIB004 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Model Checking <s> Robot swarms provide a way for a number of simple robots to work together to carry out a task. While swarms have been found to be adaptable, fault-tolerant and widely applicable, designing individual robot algorithms so as to ensure effective and correct swarm behaviour is very difficult. In order to assess swarm effectiveness, either experiments with real robots or computational simulations of the swarm are usually carried out. However, neither of these involve a deep analysis of all possible behaviours. In this paper we will utilise automated formal verification techniques, involving an exhaustive mathematical analysis, in order to assess whether our swarms will indeed behave as required. <s> BIB005 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Model Checking <s> In this paper, we develop a computational framework for fully automatic deployment of a team of unicycles from a global specification given as an LTL formula over some regions of interest. Our hierarchical approach consists of four steps: (i) the construction of finite abstractions for the motions of each robot, (ii) the parallel composition of the abstractions, (iii) the generation of a satisfying motion of the team; (iv) mapping this motion to individual robot control and communication strategies. The main result of the paper is an algorithm to reduce the amount of inter-robot communication during the fourth step of the procedure. <s> BIB006 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Model Checking <s> I l l u S t r a t I o n b y a l I C I a k u b I S t a /a n D r I J b o r y S a S S o C I a t e S in This arTiCle we consider the question: How should autonomous systems be analyzed? in particular, we describe how the confluence of developments in two areas—autonomous systems architectures and formal verification for rational agents—can provide the basis for the formal verification of autonomous systems behaviors. We discuss an approach to this question that involves: 1. Modeling the behavior and describing the interface (input/output) to an agent in charge of making decisions within the system; 2. Model checking the agent within an unrestricted environment representing the “real world” and those parts of the systems external to the agent, in order to establish some property, j; 3. Utilizing theorems or analysis of the environment, in the form of logical statements (where necessary), to derive properties of the larger system; and 4. if the agent is refined, modify (1), but if environmental properties are clarified, modify (3). Autonomous systems are now being deployed in safety, mission, or business critical scenarios, which means a thorough analysis of the choices the core software might make becomes crucial. But, should the analysis and verification of autonomous software be treated any differently than traditional software used in critical situations? Or is there something new going on here? Autonomous systems are systems that decide for themselves what to do and when to do it. Such systems might seem futuristic, but they are closer than we might think. Modern household, business, and industrial systems increasingly incorporate autonomy. There are many examples, all varying in the degree of autonomy used, from almost pure human control to fully autonomous activities with minimal human interaction. Application areas are broad, ranging from healthcare monitoring to autonomous vehicles. But what are the reasons for this increase in autonomy? Typically, autonomy is used in systems that: 1. must be deployed in remote environments where direct human control is infeasible; 2. must be deployed in hostile environments where it is dangerous for humans to be nearby, and so difficult for humans to assess the possibilities; 3. involve activity that is too lengthy Verifying autonomous systems Doi:10.1145/2494558 <s> BIB007 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Model Checking <s> In this paper we propose a generic framework for real-time motion planning based on model-checking and revision. The task specification is given as a Linear Temporal Logic formula over a finite abstraction of the robot motion. A preliminary motion plan is first generated based on the initial knowledge of the system model. Then real-time information obtained during the runtime is used to update the system model, verify and further revise the motion plan. The implementation and revision of the motion plan are performed in real-time. This framework can be applied to partially-known workspaces and workspaces with large uncertainties. Computer simulations are presented to demonstrate the efficiency of the framework. <s> BIB008 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Model Checking <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> BIB009 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Model Checking <s> The use of unmanned aircraft for civil applications is expected to increase over the next decade, particularly in so-called dull, dirty, and dangerous missions. Unmanned aircraft will undoubtedly require some form of autonomy to ensure safe operations for all airspace users. However, to be used for civil applications, unmanned aircraft must gain regulatory approval in a process known as “certification”. This paper presents a proof-of-concept approach to the generation of certification evidence for autonomous unmanned aircraft based on a combination of formal verification and flight simulation. In particular, a class of autonomous systems controlled by rational agents is examined, and we give examples of 23 different properties, based on the rules of the air and notions of airmanship, which can be used in the formal model checking of rational agents controlling autonomous unmanned aircraft. Our techniques can be based on either 1) implicit models of the aircraft’s physical environment specified in terms of... <s> BIB010 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Model Checking <s> The emergent global behaviours of robotic swarms are important for them to achieve their navigation task goals. These emergent behaviours can be verified to assess their correctness, through techniques like model checking. Model checking exhaustively explores all possible behaviours, based on a discrete model of the system, such as a swarm in a grid. A common problem in model checking is the state-space explosion that arises when the states of the model are numerous. We propose a novel implementation of symmetry reduction, in the form of encoding navigation algorithms relatively with respect to a reference, exploiting the symmetrical properties of swarms in grids. We applied the relative encoding to a swarm navigation algorithm, Alpha, modelled for the NuSMV model checker. A comparison of the state-space and verification results with an absolute (or global) and a relative encoding of the Alpha algorithm highlights the advantages of our approach, allowing model checking both larger grid sizes and higher numbers of robots, and consequently verifying more complex emergent behaviours. For example, a property was verified for a grid with 3 robots and a maximum allowed size of \(8 \times 8\) cells in a global encoding, whereas this size was increased to \(16 \times 16\) using a relative encoding. Also, the time to verify a property for a swarm of 3 robots in a \(6 \times 6\) grid was reduced from almost 10 hours to only 7 minutes. Our approach is transferable to other swarm navigation algorithms. <s> BIB011 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Model Checking <s> A new agent architecture called Limited Instruction Set Agent (LISA) is introduced for autonomous control. The new architecture is based on previous implementations of AgentSpeak and it is structurally simpler than its predecessors with the aim of facilitating design-time and run-time verification methods. The process of abstracting the LISA system to two different types of discrete probabilistic models (DTMC and MDP) is investigated and illustrated. The LISA system provides a tool for complete modelling of the agent and the environment for probabilistic verification. The agent program can be automatically compiled into a Discrete-Time Markov Chain (DTMC) or a Markov Decision Process (MDP) model for verification with PRISM. The automatically generated PRISM model can be used for both design-time and run-time verification. The run-time verification is investigated and illustrated in the LISA system as an internal modelling mechanism for prediction of future outcomes. <s> BIB012 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Model Checking <s> Robot software controllers are often concurrent and time critical, and requires modern engineering approaches for validation and verification. With this motivation, we have developed a tool and techniques for graphical modelling with support for automatic generation of underlying mathematical definitions for model checking. It is possible to check automatically both general properties, like absence of deadlock, and specific application properties. We cater both for timed and untimed modelling and verification. Our approach has been tried in examples used in a variety of robotic applications. <s> BIB013 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Model Checking <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> BIB014
Model checking is the most widely used approach to verifying robotic systems; it has been used with temporal logics  BIB012 , process algebras BIB013 , and programs BIB014 BIB007 . Arguably, the popularity of model checking owes something to the volume of publications that we found using temporal logic ( Table 2) , which are often used in model-checking approaches. Further, we see two main reasons for actively choosing model checking. First, model checkers are automatic, which makes them relatively easy to use; second, the concept of checking every state in a model to see if a required property holds is relatively easy to explain to stakeholders without formal methods experience. Some model checkers can handle timed models (e.g., Uppaal) or probabilistic models (e.g., PRISM). This can be very useful for dealing with robotic systems; timing constraints are often required for safe behavior and probability can be helpful when encoding the physical environment of the robot. Both of these features can improve confidence in the results. The input to a program model checker (such as AJPF) is the program code itself, so checking it for properties involves symbolically executing the code and assessing each execution against the required property BIB002 . Model checking exhaustively explores the state space, so one must be careful about the input models and properties to be checked. State explosion can be crippling to verification efforts using model checking. Webster et al. BIB009 report requiring 10 4 MB of memory to verify each individual safety property of their domestic assistant robot model. Similar state explosion problems are present in models of swarm robotic systems BIB005 . Various standard approaches can mitigate state space explosion and keep models tractable BIB003 BIB001 . For example, for swarms, symmetry reduction BIB011 or abstracting the swarm to a single state machine with a counting abstraction can help BIB010 . Model checking has been used to build behavior specifications (e.g., robot movement plans). One approach uses model checking to build robot motion plans that satisfy properties specified in a deterministic subset of μ-calculus BIB004 . A behavioral specification is built up incrementally, and checked after each expansion, until it moves the robot to its goal and satisfies the required properties. Similarly, in BIB008 , a BA representing the robot's environment is model-checked for an accepting path satisfying an LTL specification. The accepting path is used to synthesize a motion controller, which is then revised at runtime by repeated model checking and synthesis. Kloetzer et al. BIB006 use model checking to find traces of a transition system describing the behavior of a robot team that satisfy an LTL-X formula. This trace is used to generate the communication and control strategy for each robot in the team. Clearly, model checking is a flexible approach: it has been used for a variety of formalisms that can describe concurrent, timed, and probabilistic systems, and has been used in verification efforts for a variety of robotic systems. The increasing access to computational power and memory, combined with clever ways to reduce the state space, maintain the popularity of model checking in the literature. The need to carefully craft a model for a particular model checker adds to the modeling time and reduces the portability of models between tools. However, the automation and relative simplicity of the model-checking approach to verifying robotic systems mean that it remains a focus for research.