Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Other Formalisms <s> We present a methodology for modeling heterogeneous real-time components. ::: Components are obtained as the superposition of three layers : ::: Behavior, specified as a set of transitions; Interactions between transitions ::: of the behavior; Priorities, used to choose amongst possible interactions. ::: A parameterized binary composition operator is used to compose components layer by layer. ::: ::: We present the BIP language for the description and composition of layered components as well ::: as associated tools for executing and analyzing components on a dedicated platform. The language ::: provides a powerful mechanism for structuring interactions involving rendezvous and broadcast. ::: We show that synchronous and timed systems are particular classes of components. Finally, we ::: provide examples showing the utility of the BIP framework in heterogeneous component ::: modeling. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Other Formalisms <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> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Other Formalisms <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> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Other Formalisms <s> Self-adaptive systems have the capability to autonomously modify their behaviour at run-time in response to changes in their environment. Self-adaptation is particularly necessary for applications that must run continuously, even under adverse conditions and changing requirements; sample domains include automotive systems, telecommunications, and environmental monitoring systems. While a few techniques have been developed to support the monitoring and analysis of requirements for adaptive systems, limited attention has been paid to the actual creation and specification of requirements of self-adaptive systems. As a result, self-adaptivity is often constructed in an ad-hoc manner. In this paper, we argue that a more rigorous treatment of requirements explicitly relating to self-adaptivity is needed and that, in particular, requirements languages for self-adaptive systems should include explicit constructs for specifying and dealing with the uncertainty inherent in self-adaptive systems. We present RELAX, a new requirements language for self-adaptive systems and illustrate it using examples from the smart home domain. <s> BIB004 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Other Formalisms <s> We present a computational framework for automatic synthesis of control and communication strategies for a robotic team from task specifications given as regular expressions about servicing requests in an environment. 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 inspired from LTL model checking, we generate individual control and communication strategies. We illustrate the method with experimental results in our Robotic Urban-Like Environment. <s> BIB005 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Other Formalisms <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> BIB006 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Other Formalisms <s> In this paper we describe a verification system for multi-agent programs. This is the first comprehensive approach to the verification of programs developed using programming languages based on the BDI (belief-desire-intention) model of agency. In particular, we have developed a specific layer of abstraction, sitting between the underlying verification system and the agent programming language, that maps the semantics of agent programs into the relevant model-checking framework. Crucially, this abstraction layer is both flexible and extensible; not only can a variety of different agent programming languages be implemented and verified, but even heterogeneous multi-agent programs can be captured semantically. In addition to describing this layer, and the semantic mapping inherent within it, we describe how the underlying model-checker is driven and how agent properties are checked. We also present several examples showing how the system can be used. As this is the first system of its kind, it is relatively slow, so we also indicate further work that needs to be tackled to improve performance. <s> BIB007 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Other Formalisms <s> D-Finder 2 is a new tool for deadlock detection in concurrent systems based on effective invariant computation to approximate the effects of interactions among modules. It is part of the BIP framework, which provides various tools centered on a component-based language for incremental design. The presented tool shares its theoretical roots with a previous implementation, but was completely rewritten to take advantage of a new version of BIP and various new results on the theory of invariant computation. The improvements are demonstrated by comparison with previous work and reports on new results on a practical case study. <s> BIB008 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Other Formalisms <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> BIB009 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Other Formalisms <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> BIB010 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Other Formalisms <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> BIB011 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Other Formalisms <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> BIB012 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Other Formalisms <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> BIB013 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Other Formalisms <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> BIB014
Besides those described in the previous sections, a number of other formalisms and approaches feature in the literature. Some of these formalisms are used to specify the system and others are used to specify the properties the system is being checked for. In the literature we found, each of the studies that used "other" formalisms only specify either the system or the properties, not both. As previously mentioned in Section 4.1, autonomous robotic systems are often programmed using agents. Several works we found BIB014 BIB013 BIB012 BIB006 ] make use of the AJPF BIB007 program model checker. The properties being checked by AJPF are described in temporal logic, but the system is a BDI agent program written in GWENDOLEN. The AJPF translates agent programs into a formally defined internal representation to enable model checking. The work in  describes the verification of safety properties using the Averest framework. Robotic systems are described using the Quartz language and the safety properties are specified in μ-calculus. Quartz 5 is a synchronous language that allows the developer to describe, for example, parallel execution and nondeterministic choice. Several papers use the Behaviour Interaction Priority (BIP) framework BIB001 , which uses familiar FSMs to specify a system but provides the D-Finder tool BIB008 to check for deadlocks and other safety properties. Some work shows how BIP can be used to specify and verify robotic software  BIB002 BIB003 . In addition, RV-BIP BIB009 is a tool that produces a runtime monitor as an "additional component in a BIP system" that can check an LTS-based specification at runtime. Finally, the work in BIB010 provides a synthesis technique to generate robotic software from BIP models. Another synthesis technique is presented in BIB011 and BIB005 , which tackle robotic teams' communication strategies. The properties that the robotic team must exhibit (i.e., the tasks) are specified using a (formally defined) regular expression language. These specifications are used to synthesize robot controllers, as FSA. relax is a requirements language for dynamic self-adaptive systems that enables developers to indicate requirements that may be relaxed at runtime BIB004 . The syntax of relax is structured natural language and Boolean expressions (including standard temporal operators). Its semantics is defined in terms of temporal fuzzy logic.