Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> This paper studies a general methodology and an associated tool for translating AADL (Architecture Analysis and Design Language) and annex behavior specification into the BIP (Behavior Interaction Priority) language. This allows simulation of systems specified in AADL and application to these systems of formal verification techniques developed for BIP, e.g. deadlock detection. We present a concise description of AADL and BIP followed by the presentation of the translation methodology illustrated by a Flight Computer example. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <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> Approach References Total <s> This paper presents the behaviour-based control architecture iB2C ( i ntegrated B ehaviour- B ased C ontrol) used for the development of complex robotic systems. The specification of behavioural components is described as well as the integration of behaviour coordination and hierarchical abstraction. It is considered how the design process can be supported by guidelines and by tools for development as well as analysis. Finally some application platforms are presented. <s> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> Autonomous robots are complex systems that require the interaction/cooperation of numerous heterogeneous software components. Nowadays, robots are getting closer to humans and as such are becoming critical systems which must meet safety properties including in particular logical, temporal and real-time constraints. We present an evolution of the LAAS Architecture for Autonomous System and its tool GenoM. This evolution is based on the BIP (Behaviors Interactions Priorities) component based design framework which has been successfully used in other domains (e.g. embedded systems). In this study, we show how we seamlessly integrate BIP in the preexisting methodology. We present the componentization of the functional level of a robot, the synthesis of an execution controller as well as validation techniques for checking essential safety properties. This approach has been integrated in the LAAS architecture and we have performed a number of experiment in simulation but also on a real robot (DALA). <s> BIB004 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <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> BIB005 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> Autonomous robots are complex systems that require the interaction/cooperation of numerous heterogeneous software components. Nowadays, robots are critical systems and must meet safety properties including in particular temporal and real-time constraints. We present a methodology for modeling and analyzing a robotic system using the BIP component framework integrated with an existing framework and architecture, the LAAS Architecture for Autonomous System, based on GenoM. The BIP componentization approach has been successfully used in other domains. In this study, we show how it can be seamlessly integrated in the preexisting methodology. We present the componentization of the functional level of a robot, the synthesis of an execution controller as well as validation techniques for checking essential “safety” properties. <s> BIB006 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> We here address the modelling and analysis of human-agent teamwork, specifically in the context of proposed astronaut-robot collaboration in future space missions. We are particularly interested in modelling such systems at a level that allows formal verification techniques to be applied, and hence carry out sophisticated analysis of the reliability and effectiveness of the teams before the system is deployed in real scenarios. In this paper we describe our ongoing research in this area. <s> BIB007 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> Michigan/AFRL Collaborative Center on Control Sciences, AFOSR (grant no. FA 8650-07-2-3744) <s> BIB008 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> The paper addresses formal systems verification of autonomous underwater vehicles (AUV). The verification process includes hybrid system modelling and formulation of the discrete representation using natural language programming (sEnglish) via compositional abstraction - employing data, perception and action abstraction methods; the translation of the discrete abstraction into interpreted script programming language (ISPL) of a mainstream multi-agent model checker (MCMAS) for reachability verification of undesirable states, and ultimately the bridging into the discrete event system representation in Stateflow formalism. Using this technique, modelling and model checking can include the complete physical system of the autonomous vehicle, its multi-agent software on board and also the human interface represented as an agent. <s> BIB009 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> This paper presents a formal specification-based software monitoring approach that can dynamically and continuously monitor the behaviors of a target system and explicitly recognize undesirable behaviors in the implementation with respect to its formal specification. The key idea of our approach is in building a monitoring module that connects a specification animator with a program debugger. The requirements information about expected dynamic behaviors of the target system are gathered from the formal specification animator, while the actual behaviors of concrete implementations of the target system are obtained through the program debugger. Based on the information obtained from both sides, the judgement on the conformance of the concrete implementation with respect to the formal specification is made timely while the target system is running. Furthermore, the proposed formal specification-based software monitoring technique does not embed any instrumentation codes to the target system nor does it annotate the target system with any formal specifications. It can detect implementation errors in a real-time manner, and help the developers and users of the system to react to the problems before critical failure occurs. <s> BIB010 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <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> BIB011 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> Self-adaptive software systems are an emerging class of systems that adjust their behavior at runtime to achieve certain functional or quality of service objectives. The construction of such systems has shown to be significantly more challenging than traditional systems, partly because researchers and practitioners have been struggling with the lack of a precise method of describing, comparing, and evaluating alternative architectural choices. In this paper, we introduce a reference model, entitled FOrmal Reference Model for Self-adaptation (FORMS), which intends to alleviate this pressing issue. FORMS consists of a small number of formally specified modeling primitives that correspond to the key variation points within self-adaptive software systems, and a set of relationships that guide their composition. We present our experiences with applying FORMS to several existing systems, which not only demonstrates its ability to precisely illuminate their underlying characteristics, but also its potential as a method of rigorously specifying architectural patterns for this domain. <s> BIB012 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> A robot swarm is a collection of simple robots designed to work together to carry out some task. Such swarms rely on: the simplicity of the individual robots; the fault tolerance inherent in having a large population of often identical robots; and the self-organised behaviour of the swarm as a whole. Although robot swarms are being deployed in increasingly sophisticated areas, designing individual control algorithms that can guarantee the required global behaviour is difficult. In this paper we apply and assess the use of formal verification techniques, in particular that of model checking, for analysing the emergent behaviours of robotic swarms. These techniques, based on the automated analysis of systems using temporal logics, allow us to analyse all possible behaviours and so identify potential problems with the robot swarm conforming to some required global behaviour. To show this approach we target a particular swarm control algorithm, and show how automated temporal analysis can help to refine and analyse such an algorithm. <s> BIB013 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <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> BIB014 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> In this paper, we propose a new workflow for the design of composite systems. Contrary to existing approaches, which build on traditional techniques for single-component systems, our methodology is incremental in terms of both the design and the verification process. The approach exploits the hierarchy between components and can detect errors at an early stage of the design. As a second contribution of the paper, we apply our methodology to automatically generate C code to coordinate the various modules of an autonomous robot. To the best of our knowledge, this is the first time that such a coordination code is generated automatically. <s> BIB015 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> Verification of component-based systems still suffers from limitations such as state space explosion since a large number of different components may interact in an heterogeneous environment. Those limitations entail the need for complementary verification methods such as runtime verification based on dynamic analysis and prone to scalability. In this paper, we integrate runtime verification into the BIP (Behavior, Interaction, and Priority) framework. BIP is a powerful component-based framework for the construction of heterogeneous systems. Our method augments BIP systems with monitors checking a user-provided specification. This method has been implemented in RV-BIP, a prototype tool that we used to validate the whole approach on a robotic application. <s> BIB016 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> Recent work in robotics has applied formal verification tools to automatically generate correct-by-construction controllers for autonomous robots. However, when it is not possible to create such a controller, these approaches do not provide the user with feedback on the source of failure, making the experience of debugging a specification somewhat ad hoc and unstructured, and a source of frustration for the user. This paper describes an extension to the LTLMoP toolkit for robot mission planning that encloses the control-generation process in a layer of automated reasoning to identify the cause of failure, and targets the users attention to flawed portions of the specification. <s> BIB017 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> An alternative to deploying a single robot of high complexity can be to utilise robot swarms comprising large numbers of identical, and much simpler, robots. Such swarms have been shown to be adaptable, fault-tolerant and widely applicable. However, designing individual robot algorithms to ensure effective and correct overall swarm behaviour is actually very difficult. While mechanisms for assessing the effectiveness of any swarm algorithm before deployment are essential, such mechanisms have traditionally involved either computational simulations of swarm behaviour, or experiments with robot swarms themselves. However, such simulations or experiments cannot, by their nature, analyse all possible swarm behaviours. In this paper, we will develop and apply the use of automated probabilistic formal verification techniques to robot swarms, involving an exhaustive mathematical analysis, in order to assess whether swarms will indeed behave as required. In particular we consider a foraging robot scenario to which we apply probabilistic model checking. <s> BIB018 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> In this paper, we propose a novel top-down design method for the development of collective behaviors of swarm robotics systems called property-driven design. Swarm robotics systems are usually designed and developed using a code-and-fix approach, that is, the developer devises, tests and modifies the individual robot behaviors until a desired collective behavior is obtained. The code-and-fix approach can be very time consuming and relies completely on the ingenuity and expertise of the designer. The idea of property-driven design is that a swarm robotics system can be described by specifying formally a set of desired properties. In an iterative process similar to test-driven development, the developer produces a model of the system that satisfies the desired properties. Subsequently, the system is implemented in simulation and using real robots. Property-driven design helps to minimize the risk of developing a system that does not satisfy the required properties, and to promote the reuse of hardware independent models. In this paper, we start by giving a general description of the method. We then present a possible way to apply it by using Discrete Time Markov Chains (DTMC) and Probabilistic Computation Tree Logic* (PCTL*). Finally, we conclude by presenting the application of the proposed method to the design and development of a swarm robotics system performing aggregation. <s> BIB019 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> A robot swarm is a collection of simple robots designed to work together to carry out some task. Such swarms rely on the simplicity of the individual robots; the fault tolerance inherent in having a large population of identical robots; and the self-organised behaviour of the swarm as a whole. Although robot swarms present an attractive solution to demanding real-world applications, designing individual control algorithms that can guarantee the required global behaviour is a difficult problem. In this paper we assess and apply the use of formal verification techniques for analysing the emergent behaviours of robotic swarms. These techniques, based on the automated analysis of systems using temporal logics, allow us to analyse whether all possible behaviours within the robot swarm conform to some required specification. In particular, we apply model-checking, an automated and exhaustive algorithmic technique, to check whether temporal properties are satisfied on all the possible behaviours of the system. We target a particular swarm control algorithm that has been tested in real robotic swarms, and show how automated temporal analysis can help to refine and analyse such an algorithm. <s> BIB020 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> We present a new Interprocess Communication (IPC) mechanism and library. Ach is uniquely suited for coordinating drivers, controllers, and algorithms in complex robotic systems such as humanoid robots. Ach eliminates the Head-of-Line Blocking problem for applications that always require access to the newest message. Ach is efficient, robust, and formally verified. It has been tested and demonstrated on a variety of physical robotic systems, and we discuss the implementation on our humanoid robot Golem Krang. Finally, the source code for Ach is available under an Open Source permissive license. <s> BIB021 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> We propose a methodology for decentralized multi-agent control from Linear Temporal Logic (LTL) specifications. Each agent receives an independent specification to formally synthesize its own hybrid controller. Mutual satisfiability is not a priori guaranteed. Due to limited communication, the agents utilize meeting events to exchange their controller automata and verify satisfiability through model checking. Local interaction only when common atomic propositions exist reduces the overall computational cost, facilitating scalability. Provably correct collision avoidance and convergence is ensured by Decentralized Multi-Agent Navigation Functions. <s> BIB022 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <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> BIB023 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> We present a computational framework for automatic synthesis of control and communication strategies for a robotic team from task specifications that are given as regular expressions about servicing requests in an environment. We assume that the location of the requests in the environment and the robot capacities and cooperation requirements to service the requests are known. Our approach is based on two main ideas. First, we extend recent results from formal synthesis of distributed systems to check for the distributability of the task specification and to generate local specifications, while accounting for the service and communication capabilities of the robots. Second, by using a technique that is inspired by linear temporal logic model checking, we generate individual control and communication strategies. We illustrate the method with experimental results in our robotic urban-like environment. <s> BIB024 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <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> BIB025 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> The challenges of pervasive and mobile computing environments, which are highly dynamic and unpredictable, have motivated the development of self-adaptive software systems. Although noteworthy successes have been achieved on many fronts, the construction of such systems remains significantly more challenging than traditional systems. We argue this is partially because researchers and practitioners have been struggling with the lack of a precise vocabulary for describing and reasoning about the key architectural characteristics of self-adaptive systems. Further exacerbating the situation is the fact that existing frameworks and guidelines do not provide an encompassing perspective of the different types of concerns in this setting. In this article, we present a comprehensive reference model, entitled FOrmal Reference Model for Self-adaptation (FORMS), that targets both issues. FORMS provides rigor in the manner such systems can be described and reasoned about. It consists of a small number of formally specified modeling elements that correspond to the key concerns in the design of self-adaptive software systems, and a set of relationships that guide their composition. We demonstrate FORMS's ability to precisely describe and reason about the architectural characteristics of distributed self-adaptive software systems through its application to several existing systems. FORMS's expressive power gives it a potential for documenting reusable architectural solutions (e.g., architectural patterns) to commonly encountered problems in this area. <s> BIB026 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> In this paper we analyse a swarm robotics system using Bio-PEPA. Bio-PEPA is a process algebra language originally developed to analyse biochemical systems. A swarm robotics system can be analysed at two levels: the macroscopic level, to study the collective behaviour of the system, and the microscopic level, to study the robot-to-robot and robot-to- environment interactions. In general, multiple models are necessary to analyse a system at different levels. However, developing multiple models increases the effort needed to analyse a system and raises issues about the consistency of the results. Bio-PEPA, instead, allows the researcher to perform stochastic simulation, fluid flow (ODE) analysis and statistical model checking using a single description, reducing the effort necessary to perform the analysis and ensuring consistency between the results. Bio-PEPA is well suited for swarm robotics systems: by using Bio-PEPA it is possible to model distributed systems and their space- time characteristics in a natural way. We validate our approach by modelling a collective decision-making behaviour. <s> BIB027 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <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> BIB028 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> Nowadays, robots interact more frequently with a dynamic environment outside limited manufacturing sites and in close proximity with humans. Thus, safety of motion and obstacle avoidance are vital safety features of such robots. We formally study two safety properties of avoiding both stationary and moving obstacles: (i) passive safety, which ensures that no collisions can happen while the robot moves, and (ii) the stronger passive friendly safety in which the robot further maintains sufficient maneuvering distance for obstacles to avoid collision as well. We use hybrid system models and theorem proving techniques that describe and formally verify the robot’s discrete control decisions along with its continuous, physical motion. Moreover, we formally prove that safety can still be guaranteed despite location and actuator uncertainty. <s> BIB029 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> We applied quantified differential-dynamic logic (QdL) to analyze a control algorithm designed to provide directional force feedback for a surgical robot. We identified problems with the algorithm, proved that it was in general unsafe, and described exactly what could go wrong. We then applied QdL to guide the development of a new algorithm that provides safe operation along with directional force feedback. Using \KeYmaeraD (a tool that mechanizes QdL), we created a machine-checked proof that guarantees the new algorithm is safe for all possible inputs. <s> BIB030 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> Self-adaptation enables a software system to deal autonomously with uncertainties, such as dynamic operating conditions that are difficult to predict or changing goals. A common approach to realize self-adaptation is with a MAPE-K feedback loop that consists of four adaptation components: Monitor, Analyze, Plan, and Execute. These components share Knowledge models of the managed system, its goals and environment. To provide guarantees of the adaptation goals, state of the art approaches propose using formal models of the knowledge. However, less attention is given to the formalization of the adaptation components themselves, which is important to provide guarantees of correctness of the adaptation behavior (e.g., does the execute component execute the plan correctly?). We propose Active FORmal Models for Self-adaptation (ActivFORMS) that uses an integrated formal model of the adaptation components and knowledge models. The formal model is directly executed by a virtual machine to realize adaptation, hence active model. The contributions of ActivFORMS are: (1) the approach assures that the adaptation goals that are verified offline are guaranteed at runtime, and (2) it supports dynamic adaptation of the active model to support changing goals. We show how we have applied ActivFORMS for a small-scale robotic system. <s> BIB031 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <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> BIB032 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> We present ROSRV, a runtime verification framework for robotic applications on top of the Robot Operating System (ROS [8]), a widely used open-source framework for robot software development. ROSRV aims to address the safety and security issues of robots by providing a transparent monitoring infrastructure that intercepts and monitors the commands and messages passing through the system. Safety and security properties can be defined in a formal specification language, and are ensured by automatically generated monitors. ROSRV integrates seamlessly with ROS—no change in ROS nor the application code is needed. ROSRV has been applied and evaluated on a commercial robot. <s> BIB033 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> Ensuring that autonomous systems work ethically is both complex and difficult. However, the idea of having an additional ‘governor’ that assesses options the system has, and prunes them to select the most ethical choices is well understood. Recent work has produced such a governor consisting of a ‘consequence engine’ that assesses the likely future outcomes of actions then applies a Safety/Ethical logic to select actions. Although this is appealing, it is impossible to be certain that the most ethical options are actually taken. In this paper we extend and apply a well-known agent verification approach to our consequence engine, allowing us to verify the correctness of its ethical decision-making. <s> BIB034 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> The focus of the paper is how to model autonomous behaviours of heterogeneous multi-agent systems such that it can be verified that they will always operate within predefined mission requirements and constraints. This is done by using formal methods with an abstraction of the behaviours modelling and model checking for their verification. Three case studies are presented to verify the decision-making behaviours of heterogeneous multi-agent system using a convoy mission scenario. The multi-agent system in a case study has been extended by increasing the number of agents and function complexity gradually. For automatic verification, model checker for multi-agent systems (MCMAS) is adopted due to its novel capability to accommodate the multi-agent system and successfully verifies the targeting behaviours of the team-level autonomous systems. The verification results help retrospectively the design of decision-making algorithms improved by considering additional agents and behaviours during three steps of sce... <s> BIB035 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> Designing software systems that have to deal with dynamic operating conditions, such as changing availability of resources and faults that are difficult to predict, is complex. A promising approach to handle such dynamics is self-adaptation that can be realized by a MAPE-K feedback loop (Monitor-Analyze-Plan-Execute plus Knowledge). To provide evidence that the system goals are satisfied, given the changing conditions, the state of the art advocates the use of formal methods. However, little research has been done on consolidating design knowledge of self-adaptive systems. To support designers, this paper contributes with a set of formally specified MAPE-K templates that encode design expertise for a family of self-adaptive systems. The templates comprise: (1) behavior specification templates for modeling the different components of a MAPE-K feedback loop (based on networks of timed automata), and (2) property specification templates that support verification of the correctness of the adaptation behaviors (based on timed computation tree logic). To demonstrate the reusability of the formal templates, we performed four case studies in which final-year Masters students used the templates to design different self-adaptive systems. <s> BIB036 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> It is essential for robots working in close proximity to people to be both safe and trustworthy. We present a case study on formal verification for a high-level planner/scheduler for the Care-O-bot, an autonomous personal robotic assistant. We describe how a model of the Care-O-bot and its environment was developed using Brahms, a multiagent workflow language. Formal verification was then carried out by automatically translating this model to the input language of an existing model checker. Four sample properties based on system requirements were verified. We then refined the environment model three times to increase its accuracy and the persuasiveness of the formal verification results. The first refinement uses a user activity log based on real-life experiments, but is deterministic. The second refinement uses the activities from the user activity log nondeterministically. The third refinement uses “conjoined activities” based on an observation that many user activities can overlap. The four samples properties were verified for each refinement of the environment model. Finally, we discuss the approach of environment model refinement with respect to this case study. <s> BIB037 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Approach References Total <s> Abstract Autonomous systems such as unmanned vehicles are beginning to operate within society. All participants in society are required to follow specific regulations and laws. An autonomous system cannot be an exception. Inevitably an autonomous system will find itself in a situation in which it needs to not only choose to obey a rule or not, but also make a complex ethical decision. However, there exists no obvious way to implement the human understanding of ethical behaviour in computers. Even if we enable autonomous systems to distinguish between more and less ethical alternatives, how can we be sure that they would choose right? We consider autonomous systems with a hybrid architecture in which the highest level of reasoning is executed by a rational (BDI) agent. For such a system, formal verification has been used successfully to prove that specific rules of behaviour are observed when making decisions. We propose a theoretical framework for ethical plan selection that can be formally verified. We implement a rational agent that incorporates a given ethical policy in its plan selection and show that we can formally verify that the agent chooses to execute, to the best of its beliefs, the most ethical available plan. <s> BIB038
Model Checking BIB011 , BIB027 , BIB018 , BIB019 , BIB013 , BIB020 ,  , BIB031 [51], BIB002 , BIB032 , BIB037 , BIB021 , BIB022 , BIB014 ,  , BIB003 , BIB001 , BIB015 ,  , BIB004 , BIB023 , BIB024 , BIB007 , BIB008 , BIB028 , BIB038 , BIB034 , BIB014 ,  , BIB035 , BIB009 32 Theorem Proving BIB029 , BIB002 , BIB030 3 Runtime Monitoring BIB033 , BIB016 , BIB010 3 Integrated Formal Methods BIB036 , BIB001 ,  , BIB025 , BIB002 , BIB005 ,  , BIB010 8 Formal Software Frameworks/ Architectures BIB016 , BIB017 , BIB015 , BIB026 , BIB006 ,  , BIB004 ,  , BIB003 , BIB012 10 Note: Some of the surveyed papers use more than one approach. describe a system's behavior, each state of which is then checked to see if a temporal logic property holds. This is shown in Table 3 , where model checkers are the most used formal verification tool. Despite state-transition systems and temporal logics dominating the literature found, Table 3 shows that there are still a wide variety of tools being used for these formalisms. This may be because different model checkers capture different features, such as time or probability. But this possibly presents a challenge to the sharing and extension of formal models.