Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Self-Adaptive and Reconfigurable Systems <s> Fault tolerance and safety verification of control systems are essential for the success of autonomous robotic systems. A control architecture called mission data system (MDS), developed at the Jet Propulsion Laboratory, takes a goal-based control approach. In this paper, a method for converting goal network control programs into linear hybrid systems is developed. The linear hybrid system can then be verified for safety in the presence of failures using existing symbolic model checkers. An example task is simulated in MDS and successfully verified using HyTech, a symbolic model checking software for linear hybrid systems. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Self-Adaptive and Reconfigurable Systems <s> In this paper, we propose a novel policy for steering multiple vehicles between assigned start and goal configurations, ensuring collision avoidance. The policy rests on the assumption that all agents are cooperating by implementing the same traffic rules. However, the policy is completely decentralized, as each agent decides its own motion by applying those rules only on the locally available information, and scalable, in the sense that the amount of information processed by each agent and the computational complexity of the algorithms do not increase with the number of agents in the scenario. The proposed policy applies to systems in which new vehicles may enter the scene and start interacting with existing ones at any time, while others may leave. Under mild conditions on the initial configurations, the policy is shown to be safe, i.e., it guarantees collision avoidance throughout the system evolution. In the paper, conditions are discussed on the desired configurations of agents, under which the ultimate convergence of all vehicles to their goals can also be guaranteed. To show that such conditions are actually necessary and sufficient, which turns out to be a challenging liveness-verification problem for a complex hybrid automaton, we employ a probabilistic verification method. The paper finally presents and discusses simulations for systems of several tens of vehicles, and reports on some experimental implementation showing the practicality of the approach. <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Self-Adaptive and Reconfigurable Systems <s> This paper summarizes our survey on the development of reconfigurable machines (RMs). The goals of this survey were to (i) clarify the needs and drivers to develop the RMs, (ii) define the academic and practical issues involved in the development of RMs, (iii) learn the state of the art of the RD while RMs are essential components to implement an RMS. RMs should be designed to meet a variety of task requirements via its reconfigurability. It has been found that few existing RMs can achieve this objective. The survey has concluded that the obstacles of the development of RMs include (i) the difficulties to identify and generalize design requirements since an RM is application-oriented and the design requirements have to be defined from an actual application; and in fact, some requirements are very difficult to be quantified; (ii) the lacking of efficient automated robot programming tools despite that the robots are essential components for most of the RMs; (iii) the lack of effective technologies that can be used to support system reconfigurations; (iv) no international organization that serves for standardizing the modular components for manufacturing and assembly processes; (v) the lack of the effort in implementing a heterogeneous system consisting of different types of RMs. The survey has suggested some future research works to overcome these obstacles. <s> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Self-Adaptive and Reconfigurable Systems <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> BIB004 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Self-Adaptive and Reconfigurable Systems <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> Self-Adaptive and Reconfigurable Systems <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> BIB006 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Self-Adaptive and Reconfigurable Systems <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> BIB007 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Self-Adaptive and Reconfigurable Systems <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> BIB008 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Self-Adaptive and Reconfigurable Systems <s> A self-adaptive software system modifies its behavior at runtime in response to changes within the system or in its execution environment. The ful- fillment of the system requirements needs to be guaranteed even in the presence of adverse conditions and adaptations. Thus, a key challenge for self-adaptive software systems is assurance. Traditionally, confidence in the correctness of a system is gained through a variety of activities and processes performed at de- velopment time, such as design analysis and testing. In the presence of self- adaptation, however, some of the assurance tasks may need to be performed at runtime. This need calls for the development of techniques that enable contin- uous assurance throughout the software life cycle. Fundamental to the develop- ment of runtime assurance techniques is research into the use of models at runtime <s> BIB009 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Self-Adaptive and Reconfigurable Systems <s> The book provides a comprehensive introduction to the key techniques and technologies that help to achieve autonomous space systems for cost-effective, high performing planetary robotic missions. Main topics covered include robotic vision, surface navigation, manipulation, mission operations and autonomy, being explained in both theoretical principles and practical use cases. The book recognizes the importance of system design hence discusses practices and tools that help take mission concepts to baseline design solutions, making it a practical piece of scientific reference suited to a variety of practitioners in planetary robotics. <s> BIB010 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Self-Adaptive and Reconfigurable Systems <s> The widespread adoption of autonomous systems depends on providing guarantees of safety and functional correctness, at both design time and runtime. Information about the extent to which functional requirements can be met in combination with non-functional requirements (NFRs) -- i.e. requirements that can be partially complied with -- , under dynamic and uncertain environments, provides opportunities to enhance the safety and functional correctness of systems at design time. We present a technique to formally define system attributes that can change or be changed to deal with dynamic and uncertain environments (denominated weakened specifications) as a partially ordered lattice, and to automatically explore the system under different specifications, using probabilistic model checking, to find the likelihood of satisfying a requirement. The resulting probabilities form boundaries of "optimal specifications", analogous to Pareto frontiers in multi-objective optimization, informing the designer about the system's capabilities, such as resilience or robustness, when changing its attributes to deal with dynamic and uncertain environments. We illustrate the proposed technique through a domestic robotic assistant example. <s> BIB011 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Self-Adaptive and Reconfigurable Systems <s> The use of Petri Nets in the design of Reconfigurable Manufacturing Systems is an attractive field. Petri Nets allow modelling RMSs in an abstract way and to make specification, refinement, verification and validation of these systems. Moreover, the use of Stochastic Petri Nets allows the designer to catch more indispensable aspects (time and stochastic events) of RMSs, thus the designer can make performance evaluation. In order to study explicitly the reconfigurability, in Petri nets, several works proposed the extension of PN called reconfigurable Petri nets. However, these extensions do not deal yet with stochastic Petri nets. The objective of this paper is to present an extension of Stochastic Petri nets to deal with reconfigurability in manufacturing. <s> BIB012
Ensuring fault tolerance of robotic systems that operate in hazardous environments, potentially isolated from human interaction, is crucial. These systems must be able to diagnose and to reconfigure themselves to adapt to changes in their requirements or operating environment. Reconfiguration can help maintain quality of service or meet functional objectives BIB004 . This is particularly relevant for robotic systems that are deployed in hostile environments, such as in space or the deep ocean BIB010 BIB005 . Rational autonomy, where a system can explain its reasoning, is crucial for safe reconfiguration. Therefore, modeling the motivations and decisions of the system is an important line of current work. Ideally, this should be done in a way that enables formal verification of the autonomous decisions BIB006 . This is discussed in more detail in Section 4.1. A self-adaptive system continually alters its behavior in an environmentally driven feedback loop. The findings of a literature survey indicated that while there are no standard tools for the formal modeling and verification of self-adaptive systems, 40% of the studies they surveyed used formal modeling or validation tools, and 30% of those tools were model checkers  . Architecturebased self-adaptive systems are a specific class of self-adaptive system where the system reasons about a model of itself and the environment and adapts according to some adaptation goals. In this case, the feedback loop consists of Monitor, Analyze, Plan, and Execute components and runtime models that provide Knowledge (MAPE-K) BIB008 . A series of MAPE-K templates has been formally verified using Timed Automata (TA) and Timed Computation Tree Logic (TCTL) to aid in development. Related to the notion of adaptation is the concept of a reconfigurable system, which senses the environment and makes a decision about how best to reconfigure itself to suit changes in its requirements or the physical environment. Reconfiguration is essential for ensuring the fault tolerance of a safety-critical robotic system BIB005 . The reconfigurable systems literature focuses on two research questions: (1) how to specify and analyze a reconfigurable system BIB011 and (2) how to compare different configurations of the system BIB011 BIB004 . Therefore, it seems crucial that formal techniques applied to reconfigurable systems are able to tackle these questions. The development of reconfigurable machines is an area where a substantial amount of research has been carried out with respect to the hardware for such machines, but developing software that can autonomously reconfigure the system is a challenge for the entire community BIB003 . The development of such systems places a heavy emphasis on designing these systems to be modular, thus making reconfiguration a more approachable endeavor. Reconfigurability can be achieved by developing a flexible control system that can reconfigure itself when a fault is detected BIB001 . Specifying this can be challenging, however. The work in BIB007 presents a collection of TA models for different modes of operation and a module that enables them to be swapped during their execution on a Virtual Machine (VM). Executing the TA models ensures that the model's verified behavior is the program's runtime behavior. Recent work includes a methodology for verifying reconfigurable timed net condition/event systems  and stochastic Petri Nets to verify reconfigurable manufacturing systems BIB012 . One avenue of research suggests providing (both semiformal and formal) models to be used at runtime BIB009 . This agenda considers approaches such as automatic test case generation and formal model checking. This relies on the fact that many variables that are unknown during the design of a system can be quantified at runtime, which helps to control the problems of state space explosion. This has the benefit of providing online assurance of an adaptive system while it is adapting, which can improve the trust in results regarding safety. Decentralized systems can bring their own set of challenges for adaptation and reconfigurability. Iftikhar and Weyns  use a traffic monitoring system as their case study, where a collection of cameras monitor the traffic on a stretch of road. When a traffic jam is detected, the cameras collaborate in a master-slave architecture to report information about the traffic. This self-adaptation is managed without a central control unit to avoid the communications bottleneck this would cause. They model this system using TA and describe invariants and correctness properties using TCTL. Related work utilized a Monte Carlo approach to probabilistically verify a system of cooperating agents (autonomous vehicles) that implement a policy-based collision avoidance algorithm BIB002 .