Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> GENERAL SOFTWARE ENGINEERING TECHNIQUES FOR ROBOTIC SYSTEMS <s> Presents the software framework SMARTSOFT to implement sensorimotor systems. SMARTSOFT not only contains software components to support a modularized implementation but also structural rules and templates. These ensure that the implementation of modules is conforming with an overall multilayer system architecture. Since the provided structures allow the exact specification of the external behavior of modules in terms of interfaces and dependencies, the interaction with a symbolic task execution layer is explicitly supported. SMARTSOFT significantly eases the implementation and integration of new modules into a complex sensorimotor system which for example provides the opportunity even to compare and reuse different modules on a mobile platform. SMARTSOFT has already proven its usefulness within the collaborative research center (SFB 527) "Integration of Symbolic and Subsymbolic Information Processing in Adaptive Sensorimotor Systems". <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> GENERAL SOFTWARE ENGINEERING TECHNIQUES FOR ROBOTIC SYSTEMS <s> We present in this paper a methodology for computing the maximum velocity profile over a trajectory planned for a mobile robot. Environment and robot dynamics as well as the constraints of the robot sensors determine the profile. The planned profile is indicative of maximum speeds that can be possessed by the robot along its path without colliding with any of the mobile objects that could intercept its future trajectory. The mobile objects could be arbitrary in number and the only information available is their maximum possible velocity. The velocity profile also enables to deform planned trajectories for better trajectory time. The methodology has been adopted for holonomic and non-holonomic motion planners. An extension of the approach to an online real-time scheme that modifies and adapts the path as well as velocities to changes in the environment such that both safety and execution time are not compromised is also presented for the holonomic case. Simulation and experimental results illustrate the efficacy of this methodology. <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> GENERAL SOFTWARE ENGINEERING TECHNIQUES FOR ROBOTIC SYSTEMS <s> This paper proposes the RT-Middleware for robot system integration. "RT" means "Robot Technology" which is applied not only to industrial field but also to nonindustrial field such as human daily life support systems. We have studied modularization of RT elements and have developed software platform RT-Middleware which promotes application of RT in various field. Robotic system development methodology and our RT-Middleware concepts is discussed. The RT-Component which is a basic madular unit of RT-Middleware based system integration is derived from this discussion. A methodology of system development with RT-Components, and a framework to make component are shown. <s> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> GENERAL SOFTWARE ENGINEERING TECHNIQUES FOR ROBOTIC SYSTEMS <s> A component is a reusable and replaceable software module accessed through its interface. Component-based development is expected to shorten the development period, reduce maintenance costs, and improve program reusability and the interoperability of components. This paper proposes a new robot software component platform in order to support the entire process of robot software development. It consists of specifications of a component model, component authoring tool, component composer, and component execution engine. To show its feasibility, this paper presents the analysis results of the component’s communication overhead, a comparison with other robotic software platforms, and applications in commercial robots. <s> BIB004 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> GENERAL SOFTWARE ENGINEERING TECHNIQUES FOR ROBOTIC SYSTEMS <s> In recent years increased research activity in robotics has led to advancements in both hardware and software technologies. More complex hardware required increasingly sophisticated software infrastructures to operate it, and led to the development of several different robotics software frameworks. The driving forces behind the development of such frameworks is to cope with the heterogeneous and distributed nature of robotics software applications and to exploit more advanced software technologies in the robotics domain. So far, though, there has been not much effort to foster cooperation among these frameworks, neither on conceptual nor on implementation levels. Our research aims to analyse existing robotics software frameworks in order to identify possible levels of interoperability among them. The problem is tackled by determining a set of software concepts, in our case centering around component-based software development, which are used to determine a set of common architectural elements in an analysis of existing robotics software frameworks. The result is that these common elements can be used as interoperability points among software frameworks. Exploiting such interoperability gives developers new architectural design choices and fosters reuse of functionality already developed, albeit in another framework. It is also highly relevant for the development of new robotics software frameworks, as it opens smoother migration paths for developers to switch from one framework to another. <s> BIB005 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> GENERAL SOFTWARE ENGINEERING TECHNIQUES FOR ROBOTIC SYSTEMS <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> BIB006 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> GENERAL SOFTWARE ENGINEERING TECHNIQUES FOR ROBOTIC SYSTEMS <s> Software is an essential part of robotic systems. As robots and autonomous systems are more and more deployed in human environments, we need to use elaborate validation and verification techniques in order to gain a higher level of trust in our systems. This motivates our determination to apply formal verification methods to robotics software. In this paper, we describe our results obtained using model-checking on the functional layer of an autonomous robot. We implement an automatic translation from GenoM, a robotics model-based software engineering framework, to the formal specification language Fiacre. This translation takes into account the semantics of the robotics middleware. TINA, our model-checking toolbox, can be used on the synthesized models to prove real-time properties of the functional modules implementation on the robot. We illustrate our approach using a realistic autonomous navigation example. <s> BIB007 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> GENERAL SOFTWARE ENGINEERING TECHNIQUES FOR ROBOTIC SYSTEMS <s> Robotic technologies are continuously transforming the domestic and the industrial environments. Recently the Robotic Operating System (ROS), has been widely adopted both by industry and academia, becoming one of the most popular middleware frameworks for developing robot applications. Guaranteeing the correct behaviour of robotic systems is, however, challenging due to their potential for parameterization and heterogeneity. Although different approaches exist, focusing on concrete domain spaces for specific scenarios, no general approach to reason about ROS systems has yet arisen. This paper proposes an approach to model and verify ROS systems using real time properties, focusing on one of the main features of ROS, the communication between nodes. It takes low-level parameters into account, such as queue sizes and timeouts, and uses timed automata as the modelling language. The robot Kobuki is used as a complex case study, over which properties are automatically verified using the UPPAAL model checker, enabling the identification of problematic parameter combinations. <s> BIB008 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> GENERAL SOFTWARE ENGINEERING TECHNIQUES FOR ROBOTIC SYSTEMS <s> Work in swarm robotics typically focuses on the bottom-up design of local rules for individual robots that create emergent swarm behaviors. In this paper, we take a top-down approach and consider the following problem: how can we specify a desired collective behavior and automatically synthesize decentralized controllers that can be distributed over robots to achieve the collective objective in a provably correct way? We propose a formal specification language for the high-level description of swarm behaviors on both swarm and individual levels. We present algorithms for automated synthesis of decentralized controllers and synchronization skeletons that describe how groups of robots must coordinate to satisfy the specification. We demonstrate our algorithms on a case study. <s> BIB009
The complex task of engineering a reliable robotic system is often addressed using a variety of software engineering techniques. Though the focus of this survey is formal approaches to specifying and verifying robotic systems, this section introduces some of the less formal approaches, particularly where they are potentially useful inputs to, or could be integrated with, a formal technique. We intend this section to provide the reader with a more rounded and complete view of robotic system engineering, beginning with the commonly used middleware architectures. Middleware Architectures: Architectures for developing robotic systems generally adopt the paradigm of communicating components/nodes. Among the most popular in the literature are ROS  , OPRoS BIB004 , OpenRTM BIB003 , Orocos BIB001 , and G en oM  . Each of these supports engineering a robotic system in a slightly different way, but most share a common set of componentbased, modular concepts BIB005 to facilitate reuse of modules between different frameworks. Supporting the integration of middleware frameworks,  presents a robotic software manager with a high-level API that bridges the gaps between ROS, OPRoS, and OpenRTM. It is often assumed that a middleware is sound, and this is key to trusting the robotic system BIB007 . However, given the heterogeneity of the systems that can be produced using such architectures and their parameterizable nature, guaranteeing correct robot behavior is challenging BIB008 . Thus, we have identified the following categories of non-and semiformal methods. Testing and Simulation: Both testing and simulation are useful when developing robotic systems, particularly simulation, which enables the examination of the system's behavior in statistically unlikely situations. However, they are time-consuming and examine part of the program's state space, so they cannot be used to reason reliably about properties of the whole program. Moreover, field tests are potentially dangerous to life and the robot hardware. Examples include the following uses of field tests BIB007 BIB008 BIB006 BIB009 and/or simulations BIB002 BIB006 .