Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Process Algebras <s> This paper suggests that input and output are basic primitives of programming and that parallel composition of communicating sequential processes is a fundamental program structuring method. When combined with a development of Dijkstra's guarded command, these concepts are surprisingly versatile. Their use is illustrated by sample solutions of a variety of familiar programming exercises. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Process Algebras <s> The parallel language CSP [9], an earlier version of which was described in [7], has become a major tool for the analysis of structuring methods and proof systems involving parallelism. The significance of CSP is in the elegance by which a few simply stated constructs (e.g., sequential and parallel composition, nondeterministic choice, concealment, and recursion) lead to a language capable of expressing the full complexity of distributed computing. The difficulty in achieving satisfactory semantic models containing these constructs has been in providing an adequate treatment of nondeterminism, deadlock, and divergence. Fortunately, as a result of an evolutionay development in [S], [lo], [15], [l], [14], [2], and [4] we now have several such models. The purpose of this paper is to report the development of the first real-time models of CSP to be compatible with the properties and proof systems of the abovementioned untimed models. Our objective in this development is the construction of a timed CSP model which satisfies the following: (1) Continuous with respect to time. The time domain should consist of all nonnegative real numbers, and there should be no lower bound on the time difference between consecutive observable events from two processes operating asynchronously in parallel. (2) Realistic. A given process should engage in only finitely many events in a bounded period of time. (3) Continuous and distributive with respect to semantic operators. All semantic operators should be continuous, and all the basic operators as defined in [2], except recursion, should distribute over nondeterministic choice. (4) Verijiable design. The model should provide a basis for the definition, specification, and verification of time critical processes with an adequate treatment of nondeterminism, which assists in avoidance of deadlock and divergence. <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Process Algebras <s> We present a new framework optimized for the design, implementation, and testing of control systems for autonomous robots. It is based on a new visual specification language which specifies both control and data flow, and which is suited to be interpreted in real-time. The framework is divided into a comprehensive development and a lightweight run-time environment. The latter is fully integrated with a real-time operating system and permits to reconfigure a control system without compilation at run time. Moreover, communication in distributed systems is supported. An earlier version of the framework has been successfully applied in an autonomous helicopter and an autonomous ground vehicle project. <s> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Process Algebras <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> BIB004 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Process Algebras <s> The effective use of autonomous robot teams in highly-critical missions depends on being able to establish performance guarantees. However, establishing a guarantee for the behavior of an autonomous robot operating in an uncertain environment with obstacles is a challenging problem. This paper addresses the challenges involved in building a software tool for verifying the behavior of a multi-robot waypoint mission that includes uncertain environment geometry as well as uncertainty in robot motion. One contribution of this paper is an approach to the problem of a-priori specification of uncertain environments for robot program verification. A second contribution is a novel method to extend the Bayesian Network formulation to reason about random variables with different subpopulations, introduced to address the challenge of representing the effects of multiple sensory histories when verifying a robot mission. The third contribution is experimental validation results presented to show the effectiveness of this approach on a two-robot, bounding overwatch mission. <s> BIB005 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Process Algebras <s> Programming sophisticated robots such as service robots or humanoids is still a complex endeavor. Although programming robotic applications requires specialist knowledge, a robot software environment should support convenient development while maintaining full flexibility needed when realizing challenging robotics tasks. In addition, several desirable properties should be fulfilled, such as robustness, reusability of existing programs, and skill transfer between robots. In this work, we introduce the ArmarX statechart concept, which is used for describing control and data flow of robot programs. This event-driven statechart approach of ArmarX helps realizing important features such as increased robustness through distributed program execution, convenient programming through graphical user interfaces, and versatility by interweaving dynamic statechart structure with custom user-code. We show that using hierarchical and distributed statecharts increases reusability, allows skill transfer between robots, and hides complexity in robot programming by splitting robot behavior into control flow and functionality. <s> BIB006 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Process Algebras <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> BIB007 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Process Algebras <s> Robot software controllers are often concurrent and time critical, and requires modern engineering approaches for validation and verification. With this motivation, we have developed a tool and techniques for graphical modelling with support for automatic generation of underlying mathematical definitions for model checking. It is possible to check automatically both general properties, like absence of deadlock, and specific application properties. We cater both for timed and untimed modelling and verification. Our approach has been tried in examples used in a variety of robotic applications. <s> BIB008
Process algebraic approaches define the behaviors of a system in terms of events and the interactions of processes. They are well suited to specifying concurrent systems. Process algebras can capture (discrete) time, but they seldom capture probabilistic behavior. Multiagent systems can be described by a combination of the process algebra Finite State Processes (FSPs) and π calculus combined with ADL (π ADL)  . FSP specifies the required safety and liveness properties, which are transformed into Labeled-Transition Systems (LTSs); then the agent program and architecture (writted in π ADL) are checked to see if they satisfy these properties. The Bio-PEPA process algebra has been used to model the microscopic behavior of a robot swarm BIB004 . It enables several different analysis methods using the same specification. They describe a specification of a robot swarm performing a foraging task where a team of three robots is required to collect each object, and the teams vote on taking either a long or short path between the start and pick-up points. They present results about the model using stochastic simulation, statistical model checking, and ordinary differential equations. This collection of results is compared with an existing analysis of the same case study; the comparison shows that the approach of Massink et al. provides similar results but enables a wider range of analysis methods from a single specification. RoboChart provides a formal semantics, based on CSP BIB001 , for a timed state-machine notation BIB007 . This is a similar approach to the (nonformal) state chart notations ArmarX BIB006 and rFSM BIB003 , described in Section 2. RoboChart is supported by an Eclipse-based environment, RoboTool BIB008 , which allows the graphical construction of RoboChart diagrams so that it can be automatically translated into CSP, in the form described above. In CSP, events are instantaneous. RoboChart allows the specification of explicit time budgets and deadlines, which RoboTool translates into Timed CSP BIB002 . The CSP model checker, the Failures-Divergences Refinement checker (FDR)  , can be opened from within RoboTool to enable quick checking of the timed and untimed properties of the RoboChart model. RoboTool automatically generates basic assertions (to check for deadlock, livelock, timelock, and nondeterminism) for FDR. These can be edited, but this requires some skill with CSP and knowledge of the model, which many software engineers do not have. The ability to graphically edit and visualize the state machines is a key aspect of being able to integrate this notation into an existing engineering process. The timed process algebra, CSP+T (which extends CSP with a notion of time), has also been used to capture the real-time aspects of robotic systems. The work in  derives correct and complete CSP+T specifications from a description of a system in the Unified Modeling Language (UML) profile UML-RT-designed for developing real-time systems. This work maps each subsystem in the UML-RT description of the system to a CSP+T process and composes them in parallel. They demonstrate this approach on a two-armed industrial robot. However, this mapping appears to be a manual, informal process. As previously mentioned in Section 5.2, the graphical robot mission design tool MissionLab contains a process algebra, PARS. The work in BIB005 describes a robot's behavior using FSA and its environment using a Gaussian model, but MissionLab automatically translates these into PARS for checking the robot's behavior within the given environment.