Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Integrated Formal Methods <s> The use of swarm technologies has become prevalent in a variety of application domains: medical, bioinformatics, military/defense, surveillance, even internet television broadcasting. Future NASA missions will exploit such technologies to enable spacecraft to be sent where heretofore it was impossible, to ensure greater protection of space assets, and to increase the likelihood of mission success. We describe some of the basic concepts of swarms, and discuss the requirements of a formal method suitable for use with swarm-based systems. We also present some findings of our FAST (Formal Approaches to Swarm Technologies) project, which is attempting to identify a suitable integrated formal method for this task. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Integrated Formal Methods <s> This article deals with the problem of dynamic role-playing in Multi-Agent organisations. The approach presented uses a formal specification notation and is based upon a formal framework which defines the concepts of role, interaction and organisation. Within this framework the problem of dynamic role-playing specification is related to the merging of specifications. The formal notation used composes Object-Z and Statecharts. The main features of this approach are: enough expressive power to represent Multi-Agents dynamic aspects, tools for specification analysis and mechanisms allowing the refinement of a high level specification into a low level specification which can be easily implemented. The last part of this paper presents an application with the specification of a reactive and cooperative MAS model named Satisfaction Altruism. An analysis of the specification validates the agents' behaviours. <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Integrated Formal Methods <s> This paper presents an experience report on the specification and the validation of a real case study in the context of the industrial CRISTAL project. The case study concerns a platoon of a new type of urban vehicles with new functionalities and services. It is specified using the combination, named CSP||B, of two well-known formal methods, and validated using the corresponding support tools. This large --- both distributed and embedded --- system typically corresponds to a multi-level composition of components that have to cooperate. We identify some lessons learned, showing how to develop and verify the specification and check some properties in a compositional way using theoretical results and support tools to validate this complex system. <s> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Integrated Formal Methods <s> Organic computing systems are systems which have the capability to autonomously (re-)organize and adapt themselves. The benefit of such systems with self-x properties is that they are more dependable, as they can compensate for some failures. They are easier to maintain, because they can automatically configure themselves and are more convenient to use because of automatic adaptation to new situations. While organic computing systems have a lot of desired properties, there still exists only little knowledge on how they can be designed and built.In this paper an approach for specification and construction of a class of organic computing systems is presented, called the (RIA). The core idea is that the behaviour of an organic computing system can be split into productive phases and self-x phases. This allows for a generic description of how ``organic'' aspects can be specified and implemented. The approach will be illustrated by applying it to a design methodology for organic computing systems and further refining it to an explicit case study in the domain of production automation. <s> BIB004 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Integrated Formal Methods <s> Ensuring fault tolerance of satellite systems is critical for achieving goals of the space mission. Since the use of redundancy is restricted by the size and the weight of the on-board equipments, the designers need to rely on dynamic reconfiguration in case of failures of some components. In this paper we propose a formal approach to development of dynamically reconfigurable systems in Event-B. Our approach allows us to build the system that can discover possible reconfiguration strategy and continue to provide its services despite failures of its vital components. We integrate probabilistic verification to evaluate reconfiguration alternatives. Our approach is illustrated by a case study from aerospace domain. <s> BIB005 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Integrated Formal Methods <s> The paper describes a design specification process for the development of novel and intelligent surgical robots. Nowadays, surgical robots are usually controlled by the surgeons manually by using teleoperation. The possibility to carry out simple surgical actions automatically has been the subject of academical research, but very few real-world applications exist. The main objective of this research is to address realistic case studies and develop systems and methods to provide surgeons with autonomous robotic assistants, performing basic surgical actions by combining sensing, dexterity and cognitive capabilities. This goal can only be achieved by means of a formal and rigorous assesment of surgical requirements, so that they can be analysed and translated into behavioral specifications for an autonomous robotic system. Therefore, the paper describes the application of Requirements Engineering to surgical knowledge formalization and propose a methodology for the transformation of requirements into formal models of robotic tasks. <s> BIB006 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Integrated Formal Methods <s> The formal development of multi-agent systems MAS may involve consideration of system functionality at three distinct levels of abstraction. The macro level focusses on the system's overall, global behaviour, independently of how the agents of the system operate and interact. The meso level focusses on agent interactions, and the micro level on the operation of individual agents. While Object-Z with its high-level support for component-based specifications is well suited to modelling MAS at the macro and meso levels, it can become cumbersome at the micro level where the low-level mechanisms required for dealing with asynchronous communication between agents and timing constraints need to be explicitly defined. In this paper we introduce MAZE, an extension of Object-Z supporting i action refinement to facilitate the development process from the macro to micro level, and ii a number of syntactic conventions to facilitate micro-level specification. The syntactic conventions are shorthands for existing Object-Z notation and so require no redefinition of Object-Z's semantics. <s> BIB007 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Integrated Formal Methods <s> The coordination of multiple autonomous vehicles into convoys or platoons is expected on our highways in the near future. However, before such platoons can be deployed, the new autonomous behaviors of the vehicles in these platoons must be certified. An appropriate representation for vehicle platooning is as a multi-agent system in which each agent captures the "autonomous decisions" carried out by each vehicle. In order to ensure that these autonomous decision-making agents in vehicle platoons never violate safety requirements, we use formal verification. However, as the formal verification technique used to verify the agent code does not scale to the full system and as the global verification technique does not capture the essential verification of autonomous behavior, we use a combination of the two approaches. This mixed strategy allows us to verify safety requirements not only of a model of the system, but of the actual agent code used to program the autonomous vehicles. <s> BIB008 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Integrated Formal Methods <s> Designing robotic systems can be very challenging, yet controllers are often specified using informal notations with development driven primarily by simulations and physical experiments, without relation to abstract models of requirements. The ability to perform formal analysis and replicate results across different robotic platforms is hindered by the lack of well-defined formal notations. In this paper we present a timed state-machine based formal notation for robotics that is informed by current practice. We motivate our work with an example from swarm robotics and define a compositional CSP-based discrete timed semantics suitable for refinement. Our results support verification and, importantly, enable rigorous connection with sound simulations and deployments. <s> BIB009 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Integrated Formal Methods <s> Robotic systems are multi-dimensional entities, combining both hardware and software, that are heavily dependent on, and influenced by, interactions with the real world. They can be variously categorised as embedded, cyber-physical, real-time, hybrid, adaptive and even autonomous systems, with a typical robotic system being likely to contain all of these aspects. The techniques for developing and verifying each of these system varieties are often quite distinct. This, together with the sheer complexity of robotic systems, leads us to argue that diverse formal techniques must be integrated in order to develop, verify, and provide certification evidence for, robotic systems. Furthermore, we propose the fast evolving field of robotics as an ideal catalyst for the advancement of integrated formal methods research, helping to drive the field in new and exciting directions and shedding light on the development of large-scale, dynamic, complex systems. <s> BIB010 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Integrated Formal Methods <s> The spread of autonomous systems into safety-critical areas has increased the demand for their formal verification, not only due to stronger certification requirements but also to public uncertainty over these new technologies. However, the complex nature of such systems, for example, the intricate combination of discrete and continuous aspects, ensures that whole system verification is often infeasible. This motivates the need for novel analysis approaches that modularise the problem, allowing us to restrict our analysis to one particular aspect of the system while abstracting away from others. For instance, while verifying the real-time properties of an autonomous system we might hide the details of the internal decision-making components. In this paper we describe verification of a range of properties across distinct dimensions on a practical hybrid agent architecture. This allows us to verify the autonomous decision-making, real-time aspects, and spatial aspects of an autonomous vehicle platooning system. This modular approach also illustrates how both algorithmic and deductive verification techniques can be applied for the analysis of different system subcomponents. <s> BIB011
Integrated Formal Methods (iFMs) refer to the integration of multiple formal methods, or a formal method with a semi-or nonformal approach, that complement each other. While still difficult, iFMs can capture several dimensions of a system at once (e.g., static and dynamic behavior) for easy analysis. In our previous work, we argue that robotic systems provide the impetus for addressing the challenges of integration; furthermore, because robotic systems are inherently hybrid, they need iFMs BIB010 . An early example of this need is a study concluding that no single formalism was suitable for applying to a robot swam and a combination of four formalisms would be the best approach BIB001 . The challenges presented in Section 4 are often best tackled using iFMs. However, our literature search found no generic approaches for applying iFMs to robotics. Here, we discuss some notable bespoke examples. To enable both refinement-based development and probabilistic checking, BIB005 uses both Event-B and a probabilistic language to check reconfigurable architectures for an onboard satellite system. The work in  combines FSP and π ADL to capture safety and liveness properties of multiagent robotic systems. The FSP specifications of the relevant safety and liveness properties are transformed into LTSs, and then the agent programs and architecture (described in π ADL) are checked to see if they satisfy the required properties. The work in BIB007 combines MAZE (an extension of Object-Z for multiagent systems) and Back's action refinement to enable top-down development of robot swarms. In BIB008 , an agent controlling a car is verified using AJPF, and the timing properties are verified using Uppaal. This is extended in BIB011 with a spatial reasoning calculus. The work verifies the cooperation between the vehicles and the abstract behavior of the physical vehicle. Another platooning driverless car is modeled using an integrated formalism combining CSP and B (CSP B) BIB003 . Similarly, OZS combines Object-Z BIB002 and Statecharts  ; it has been used to describe the state and behavior of systems to formalize part of the Satisfaction-Altruism Model  . This model captures the dynamic set of roles that a robot in a multirobot team can perform. The roles define the interaction pattern of the robot. OZS has an operational semantics, which enables theorem proving. In BIB002 , the authors describe verification of their model using the SAL model checker and the STeP theorem prover. They also indicate an intent to provide a way to refine OZS models to code for deployment on robots. These bespoke examples integrate two or more formal methods to obtain an approach to verification with their combined benefits. There are also examples that integrate a formalism with a nonformal notation. For example, an approach for deriving formal specifications from the real-time UML profile UML-RT  captures UML-RT subsystems as processes in the timed CSP derivative, CSP+T. This also provides UML-RT with a semantics in CSP+T. RoboChart is a robotic system design notation that integrates CSP with a graphical timed statemachine notation BIB009 . The integration displayed by RoboChart provides a generic formal notation for robotic systems, which is an approach that yields a reusable and stable formal method. This reusable, stable, and generic approach to iFMs is key to the success of iFMs, not just for robotic systems but more generally as well. Integrating diverse formalisms into a holistic framework remains an open problem, waiting to be solved. In the area of automated surgical robotics the combination of UML, LTL, and Alloy has been used to model and reason about a number of surgical operations BIB006 . The work employs a goaloriented methodology where a UML model relates goal requirements to the "high-level structural and behavioral decomposition of the intelligent robotic system." A number of experts (medical professionals) were interviewed and their responses were used to construct a goal model that was converted into a set of formal properties using the Alloy language where each goal is formally defined in LTL. This model is then checked by the KodKod SAT solver. The UML model can then be translated into executable code using the Orocos framework. The Restore Invariant Approach (RIA) uses invariants to specify productive states and to use constraint solving techniques whenever the system is not operational to find new configurations to make the system operational again BIB004 . This work targets self-adaptive and agent-based systems. It was used in the specification and verification of an adaptive production cell that was made up of three drill robots and two autonomous transportation units that connect them. Here, the authors make use of class diagrams with Object Constraint Language (OCL) constraints, the Microsoft Robotics Studio simulator, the JADEX multiagent framework, and the Alloy constraint solver.