Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Approaches <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> Summary of Approaches <s> Formal methods use mathematical models for analysis and verification at any part of the program life-cycle. We describe the state of the art in the industrial use of formal methods, concentrating on their increasing use at the earlier stages of specification and design. We do this by reporting on a new survey of industrial use, comparing the situation in 2009 with the most significant surveys carried out over the last 20 years. We describe some of the highlights of our survey by presenting a series of industrial projects, and we draw some observations from these surveys and records of experience. Based on this, we discuss the issues surrounding the industrial adoption of formal methods. Finally, we look to the future and describe the development of a Verified Software Repository, part of the worldwide Verified Software Initiative. We introduce the initial projects being used to populate the repository, and describe the challenges they address. <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Approaches <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> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Approaches <s> Abstract Developing advanced robotics applications is now facing the safety issue for users, the environment, and the robot itself, which is a main limitation for their deployment in real life. This safety could be justified by the use of dependability techniques as it is done in other safety-critical applications. However, due to specific robotic properties (such as continuous human–robot physical interaction or non deterministic decisional layer), many techniques need to be adapted or revised. This paper reviews the main issues, research work and challenges in the field of safety-critical robots, linking up dependability and robotics concepts. <s> BIB004
This section discussed the formal verification approaches in the literature as summarized in Table 4 . The most popular approach is model checking, which is reflected in the dominance of temporal logics and state-transition systems for the specification of robotic systems (Section 5, Table 2 ). We speculate that the prevalence of model checking in the literature may be because it is easy for developers to understand and trust who do not have a formal methods background since it is automatic and conceptually similar to exhaustive testing. Frameworks for verifiable robotic systems were the next most popular approach, and most of these incorporated a bespoke model checker. However, it is not clear, in practice, just how effective these in-built verification tools are. As outlined earlier, iFMs are necessary in the verification of robotic systems due to their size and complexity. This is an active area of research with tools still under development. We anticipate that, in the future, this approach will feature more in the verification of autonomous robotic systems. The least popular approaches were theorem proving and runtime monitoring. In general, theorem provers require specialist knowledge to use and we believe that this is why it is currently not as popular as other approaches. Although effective in the running system, runtime monitoring is often seen as a separate step in the verification process after static verification has taken place and provides little in the way of design-time benefits. 7 CONCLUSION Section 1.2 discussed related surveys and differentiated them from our work. Our work incorporates the topics of formal methods for self-adaptive systems (surveyed in  ) and swarms (from   ). We also identify work from several categories that a survey on safety-critical robotics BIB004 lists as areas to focus on. Specifically, these are modeling of a robot's physical environment, formal verification of robotic systems, correct-by-construction controller synthesis, and being able to provide certification evidence. This last point is particularly important and is a key focus in the current literature. Finally, the work that we have surveyed is squarely within the category of verifying applications for internal correctness, one of three main challenges for the automatic verification of autonomous systems BIB001 . Some of the current literature focuses on the external correctness of the software, for example, how it will safely interact with a robotic software framework like ROS or G en oM. However, the suggestions that special-purpose language interpreters or compilers must verify has not been borne out, as many robotic applications are written in general-purpose languages such as Python, Java, or C++. This, of course, leaves the tools for these languages to be verified, a larger challenge due to the generality of the languages. Section 1.1 outlined the research questions that this article investigates. In this section, we use the results of our survey to derive potential answers to these research questions. The answers also provide the structure for a discussion of our observations of the current state of the literature. RQ1 asked what the challenges are when formally specifying and verifying (autonomous) robotic systems. We identified two types of challenge: those external to the robotic system, discussed in Section 3, and those internal to the robotic system, discussed in Section 4. The external challenges that we identified are modeling the robotic system's external environment and providing sufficient evidence for public trust and certification. The internal challenges that we identified are the use of agent-based, multirobot, and adaptive/reconfigurable systems. Reconfigurability is key to safely deploying robots in hazardous environments and vastly more work needs to materialize to ensure the safety of reconfigurable autonomous systems. Therefore, we see a clear link between a robotic system reacting to the changes in its external environment and reconfigurable systems. Similarly, rational agent-based systems that can explain their reasoning provide a good route for providing evidence for public trust or certification bodies. This is because they enable the crucial transparency that trust and certification need. An example of the transparency required is the ethical black box proposed by  , which records the sensor input and internal state of the system. A rational agent can provide reasons for its choices based on the input and internal state information. RQ2 asked what are the current formal methods used for tackling the challenges identified by answering RQ1. Our analysis, presented in Section 5 and Section 6, shows that temporal logics, state-transition systems, and model checkers are the most prominent formalisms and approaches in the literature over the past decade. We speculate that this is due to the fact that temporal logics and state-transition systems allow abstract specification, which is useful earlier in the development process, and because model checking as an approach is generally easy to explain to stakeholders who do not have experience using formal methods. RQ3 asked what the limitations are of the best-practice formalisms and approaches to verification that were identified in the answer to RQ2. One limitation appears to be a resistance to adopting formal methods in robotic systems development BIB003 . The perception is that applying formal methods is a complicated additional step in the engineering process, which prolongs the development process while not adding to the value of the final product. A lack of appropriate tools also often impedes the application of formal methods. These are long-standing opinions, for example, the authors of  , which was published 19 years prior to BIB003 . There are, however, notable examples of industrial uses of formal methods, such as those examined in BIB002 . The wide variety of tools for the same formalism (indicated in Table 3 ) also points to a problem: the lack of interoperability between formalisms. Often, models or specifications of similar components are incompatible and locked into a particular tool. This suggests that a common framework for translating between, relating, or integrating different formalisms would prove useful in smoothing the conversion between formalisms or tools. Further, this would serve a growing need to capture the behavior of complex systems using a heterogeneous set of formalisms, each suited to the component being modeled or the properties of interest. This is currently an open problem in formal methods for robotic systems. As mentioned in Section 3, there is a lack of clear guidance when it comes to choosing a suitable formal method for a particular system. With respect to autonomous robotic systems, Table 1 lists the formalisms/tools used and the corresponding case study that was presented in the surveyed literature. This provides some guidance when choosing an appropriate formal method for a given system, but we leave a more detailed analysis of this as future work. Another limitation faced by formal methods for robotic systems (and more generally) is that of formalizing the last link, the step between a formal model and program code. We found few examples of formal methods for robotics that also produced runnable program code from a specification, and, in these examples, it was often unclear as to how the code relates back to the original specification model. Such last link translation steps require a formal underpinning to ensure that the model is represented by the code. The lack of clarity about this limitation points to another: a lack of open sharing of models, code, and realistic case studies that are not tuned for a particular formalism. Field tests and experiments using simulations are both useful tools for robotic systems development, but formal verification is crucial, especially at the early stages of development when field tests of the control software are infeasible (or dangerous). A focused research effort on the combination or integration of formal methods should improve their use in robotic systems development, because no one formalism is capable of adequately capturing that all aspects of a robotic system behave as expected. Ensuring that these tools are usable by developers and providing similar features in an IDE would also improve their uptake by simplifying their use. Work in this area could lead to an Integrated Verification Environment, allowing the use of different formalisms using the same developer front end, connecting them to their respective tools, and providing helpful IDE-like support. We have identified a number of threats to validity for this work, and we have taken measures to mitigate them where possible. In particular, researcher bias was minimized by explicitly stating the scope and research questions at the beginning of the review and having two researchers analyze the search results in tandem. Restricting our search to those papers published within the last 10 years may affect the completeness of our search results; however, by "snowballing" we have explored and discussed papers that did not fall within this range throughout the narrative in this report. Furthermore, our use of Google Scholar limits our search to those papers that were found using Google's algorithms. Again, our use of "snowballing" helps to mitigate this threat. This article has analysed the current state-of-the-art literature particular to the formal specification and verification of autonomous robotic systems. To this end, this survey identifies future directions in this field.