Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Swarms. <s> While autonomous systems offer great promise in terms of capability and flexibility, their reliability is particularly hard to assess. This paper describes research to apply formal verification methods to languages used to develop autonomy software. In particular, we describe tools that automatically convert autonomy software into formal models that are then verified using model checking. This approach has been applied to MPL code for the Livingstone fault diagnosis system and to TDL task descriptions for mobile robot systems. Our long-term objective is to create tools that enable engineers and roboticists to use formal verification as part of the normal software development cycle. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Swarms. <s> The term swarm has been applied to many systems (in biology, engineering, computation, etc.) as they have some of the qualities that the English-language term swarm denotes. With the growth of the various area of swarm research, the swarm terminology has become somewhat confusing. In this paper, we reflect on this terminology to help clarify its association with various robotic concepts. <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Swarms. <s> Swarm robotics is a novel approach to the coordination of large numbers of relatively simple robots which takes its inspiration from social insects. This paper proposes a definition to this newly emerg- ing approach by 1) describing the desirable properties of swarm robotic systems, as observed in the system-level functioning of social insects, 2) proposing a definition for the term swarm robotics, and putting for- ward a set of criteria that can be used to distinguish swarm robotics research from other multi-robot studies, 3) providing a review of some studies which can act as sources of inspiration, and a list of promising domains for the utilization of swarm robotic systems. <s> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Swarms. <s> The swarm intelligence literature frequently asserts that swarms exhibit high levels of robustness. That claim is, however, rather less frequently supported by empirical or theoretical analysis. But what do we mean by a 'robust' swarm? How would we measure the robustness or – to put it another way – fault-tolerance of a robotic swarm? These questions are not just of academic interest. If swarm robotics is to make the transition from the laboratory to real-world engineering implementation, we would need to be able to address these questions in a way that would satisfy the needs of the world of safety certification. This paper explores fault-tolerance in robot swarms through Failure Mode and Effect Analysis (FMEA) and reliability modelling. The work of this paper is illustrated by a case study of a wireless connected robot swarm, employing both simulation and real-robot laboratory experiments. <s> BIB004 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Swarms. <s> It is a characteristic of swarm robotics that modelling the overall swarm behaviour in terms of the low-level behaviours of individual robots is very difficult. Yet if swarm robotics is to make the transition from the laboratory to real-world engineering realisation such models would be critical for both overall validation of algorithm correctness and detailed parameter optimisation. We seek models with predictive power: models that allow us to determine the effect of modifying parameters in individual robots on the overall swarm behaviour. This paper presents results from a study to apply the probabilistic modelling approach to a class of wireless connected swarms operating in unbounded environments. The paper proposes a probabilistic finite state machine (PFSM) that describes the network connectivity and overall macroscopic behaviour of the swarm, then develops a novel robot-centric approach to the estimation of the state transition probabilities within the PFSM. Using measured data from simulation the paper then carefully validates the PFSM model step by step, allowing us to assess the accuracy and hence the utility of the model. <s> BIB005 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Swarms. <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> BIB006 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Swarms. <s> We model the dynamics of self-organized robot aggregation inspired by a study on the aggregation of gregarious arthropods. In swarms of German cockroaches, aggregation into clusters emerges solely from local interactions between the individuals, whereas the probabilities of joining or leaving a cluster are a function of the cluster size. We propose a non-spatial population dynamics model that keeps track of the number of robots in clusters of specific size using control parameters of the individual robots and the probability of detecting another robot in the environment. The model is able to quantitatively and qualitatively predict the dynamics observed in extensive realistic multi-robot simulation, and provides qualitative agreement with data obtained from aggregation of Blattela germanica larvae. In particular, we show by analysis, numerical and realistic simulation that the emergence of a single aggregate requires a minimal communication range between individuals. <s> BIB007 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Swarms. <s> We have recently started an effort to combine a state of the art tool for developing functional modules of robotic systems (G^e^noM) with a component based framework for implementing embedded real-time systems (BIP). Unlike some works which study the connection between formal approaches and the highest (decisional) level of the robot software architecture, where deliberative activities such as planning, diagnostics, and execution control are conducted, we tackle the problem of using formal methods for developing modules of the functional level of robots. Little attention has been drawn to the development of these modules whose robustness is paramount to the robustness of the overall platform. To this end, we have successfully developed the G^e^noM/BIP component based design approach and applied it to the functional level of a complex exploration rover. Here, we report on this work, and show how we: (i) produce a very fine grained formal computational model of the robot functional level; (ii) run the BIP engine on the real robot, which executes and enforces the model semantics at runtime; and (iii) check the model offline for deadlock-freedom, as well as other safety properties. Moreover, we also extended this paradigm in a number of promising directions: (i) introduced a real-time BIP engine which can now use and control a timed BIP model; (ii) distributed the model and the engine over multiple CPUs; (iii) proposed a user-friendly language for specifying constraints on the model; and (iv) linked the model with a temporal plan execution controller. Interestingly, although our approach was initially proposed for the lowest level of robot architectures, these more recent extensions now allow us to model and manage the deliberation taking place at the decisional layer. <s> BIB008 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Swarms. <s> Currently, the control software of swarm robotics systems is created by ad hoc development. This makes it hard to deploy these systems in real-world scenarios. In particular, it is difficult to maintain, analyse, or verify the systems. Formal methods can contribute to overcome these problems. However, they usually do not guarantee that the implementation matches the specification, because the system’s control code is typically generated manually. Also, there is cultural resistance to apply formal methods; they may be perceived as an additional step that does not add value to the final product. To address these problems, we propose supervisory control theory for the domain of swarm robotics. The advantages of supervisory control theory, and its associated tools, are a reduction in the amount of ad hoc development, the automatic generation of control code from modelled specifications, proofs of properties over generated control code, and the reusability of formally designed controllers between different robotic platforms. These advantages are demonstrated in four case studies using the e-puck and Kilobot robot platforms. Experiments with up to 600 physical robots are reported, which show that supervisory control theory can be used to formally develop state-of-the-art solutions to a range of problems in swarm robotics. <s> BIB009 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Swarms. <s> Work in swarm robotics typically focuses on the bottom-up design of local rules for individual robots that create emergent swarm behaviors. In this paper, we take a top-down approach and consider the following problem: how can we specify a desired collective behavior and automatically synthesize decentralized controllers that can be distributed over robots to achieve the collective objective in a provably correct way? We propose a formal specification language for the high-level description of swarm behaviors on both swarm and individual levels. We present algorithms for automated synthesis of decentralized controllers and synchronization skeletons that describe how groups of robots must coordinate to satisfy the specification. We demonstrate our algorithms on a case study. <s> BIB010
A robot swarm is a decentralized collection of robots that work together BIB002 , often taking inspiration from swarms of ants or bees. Robot swarms generally contain robots that are adaptive, large in number, not grouped together, relatively incapable or inefficient, and able to send and communicate locally BIB003 . However, these criteria are not exhaustive, and should simply be used to decide to what degree the term "swarm robotics" might apply  . Formal methods have obvious benefits for specifying the behavior of swarm robot systems, because field tests and simulations only cover a particular instance of the swarm's behavior BIB006 . However, the large number of robots in a swarm can explode the state space and thus hinder verification using conventional model-checking approaches BIB006 . A further issue is scalability: if you prove a property for a swarm of n robots, does the property hold for n ± 1 robots? Robot swarms are often used for their resilience. Winfield and Nembrini BIB004 examined the fault tolerance of robot swarms navigating using the alpha algorithm and found that robustness arises from the inherent properties of a swarm: simple parallel robots, operating in a fully distributed way, with high redundancy. Of particular interest, they found that the partial failure of a robot was more problematic than a robot's total failure. In their example, a robot that was fully functioning, apart from its wheels not turning, anchored the swarm in place. Determining if failures will propagate through the swarm and determining a lower bound on the number of robots that must remain functioning for the swarm to complete its mission is an active area of research  . Kouvaros and Lomuscio  present an approach that uses temporal logic and fault injection to determine the ratio of faulty to functioning robots in a swarm navigating using the alpha algorithm. They specify temporal-epistemic properties and then they find the threshold at which the swarm no longer satisfies these properties. Crucially, their approach is designed to work with swarms where the number of agents is unknown at design time. Programs for robot swarms are often developed in an ad hoc manner, using trial and error. The developers tend to follow a bottom-up approach that involves programming individual robots before combining them to form a swarm that displays a certain set of behaviors  BIB009 BIB010 . This development process can reduce the effectiveness of formal engineering approaches; the application of formal methods often does not guarantee that the implementation matches the specification, because the programs are built manually from the specification BIB009 . Winfield et al. BIB005 present a straightforward approach to modeling the macroscopic behavior of the swarm using a PFSM. First, they estimate the transition probabilities in the PFSM; then, they validate these probabilities by simulations in Player/Stage. BIB008 Markov chains have been used to model the probabilities of members of a robot swarm joining or leaving aggregates of robots BIB007 . The probabilities were a function of the size of the aggregate, and were based on a biological study of cockroach aggregation. The model was used to predict the probability of a swarm aggregating, without capturing spatial information. Despite the limitation of assuming that an aggregate can only grow or shrink linearly, they conclude that robots need a minimal speed or sensor range to enable aggregation. Rouff et al. compared four different specification formalisms (Communicating Sequential Processes (CSP), Weighted Synchronous CCS (WSCCS), Unity Logic, and X-Machines) for specifying and verifying emergent swarm behavior  . They concluded that a blending of these formalisms offered the best approach to specify emergent swarm behavior as none was sufficient in isolation. It is thus clear that only the use of multiple, specialized tools and methodologies can achieve a high level of confidence in software for robot swarms and, more generally, software for robotic systems  . For example, the NASA Remote Agent uses specialized languages for each of the planner, executive, and fault diagnosis components BIB001 . We explore the use of integrated formal methods for the specification and verification of robotic systems in Section 6.4.