The design of embedded real-time systems requires specific toolchains to guarantee time constraints and safe behavior. These tools and their artifacts need to be managed in a coherent way all along the design process and need to address timing constraints and execution semantic in a holistic way during the system’s modeling, verification, and implementation phases. However, modeling languages used by these tools do not always share a common semantic. This can introduce a dangerous gap between what designers want to express, what is verified and the behavior of the final executable code. In order to address this problem, we propose a new toolchain, called Hippo, that integrates tools for design, verification and execution built around a common formalism. Our approach is based on an extension of the Fiacre specification language with runtime features, such as asynchronous function calls and synchronization with events. We formally define the behavior of these additions and describe a compiler to generate both an executable code and a verifiable model from the same high-level specification. The execution of the resulting code is supported by a dedicated execution engine that guarantees real-time behavior and that reduces the semantic gap between high-level models and executable code. We illustrate our approach with a non-trivial use case: the autonomous navigation of a Segway RMP440 robotic platform. We describe how we derive a Hippo model from an initial specification of the system based on the robotics programming framework . We also show how to use the Hippo runtime to control this robot, and how to use formal verification in order to check critical properties on this system.

Throughout the last few decades, researchers and practitioners are showing more and more interest in using formal methods in order to predict and prevent software failures in robotic and autonomous systems. However, the applicability of formal methods to such systems is limited due to several factors. For instance, robotic specifications are often non-formal which makes their formalization hard and error prone, and their translation into formal models ad-hoc and non automatic. Furthermore, the complexity and size of robotic applications lead most often to scalability issues with exhaustive techniques such as model checking. In this paper, we investigate the use of runtime verification as an alternative to model checking for the rigorous verification of large robotic systems. To do so, we first develop a sound and automatic translation from the robotic framework GenoM3 to the real-time version of the BIP formal language. Then, we apply the translation to a real-world case study the formal models of which do not scale with model checking, and use the BIP Engine to execute the generated BIP model, verify properties online, and adequately react to their possible violation. The experiments are carried out on a real Robotnik robot and show the efficiency of our approach in verifying timed properties, that is when the amount of time separating events is important.

The ability to navigate in diverse and previously unknown environments is a critical service of autonomous robots. The validation of the navigation software typically involves test campaigns in the field, which are costly and potentially risky for the robot itself or its environment. An alternative approach is to perform simulation-based testing, by immersing the software in virtual worlds. A question is then whether the bugs revealed in real worlds can also be found in simulation. The paper reports on an exploratory study of bugs in an academic software for outdoor robots navigation. The detailed analysis of the triggers and effects of these bugs shows that most of them can be revealed in low-fidelity simulation. It also provides insights into interesting navigation scenarios to test as well as into how to address the test oracle problem.

This paper reports on FAPE (Flexible Acting and Planning Environment), a framework integrating acting and planning on the basis of the ANML modeling language. ANML is a recent proposal motivated by combining the expressiveness of the timeline representation with decomposition methods of Hierarchical Task Networks (HTN). Our current focus is not efficient temporal planning per se, but the tight integration of acting and planning. This integration is addressed by: (i) extending HTN methods with the refinement of planned actions with skills, expressed in PRS, to map actions into low-level commands, (ii) interleaving the planning process with acting, the former performs plan repair and replanning, while the latter implements the skill-based refinements, and (iii) executing commands with a dispatching mechanism that synchronizes observed time points of action effects and events with planned time. FAPE has been integrated to a PR2 robot and experimented in a home-like environment. The paper presents how planning is performed and integrated with acting and describes briefly the robotics experiments.

The topic of reusable software in robotics is now largely addressed. Components based architectures, where components are independent units that can be reused accross applications, have become more popular. As a consequence, a long list of middlewares and integration tools is available in the community, often in the form of open-source projects. However, these projects are generally self contained with little reuse between them. This paper presents a software engineering approach that intends to grant middleware independance to robotic software components so that a clear separation of concerns is achieved between highly reusable algorithmic parts and integration frameworks. Such a decoupling let middle-wares be used interchangeably, while fully benefitting from their specific, individual features. This work has been integrated into a new version of the open-source GenoM component generator tool: GenoM3

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 Geno

Autonomous robots offer alluring perspectives in numerous application domains: space rovers, satellites, medical assistants, tour guides, etc. However, a severe lack of trust in their dependability greatly reduces their possible usage. In particular, autonomous systems make extensive use of decisional mechanisms that are able to take complex and adaptative decisions, but are very hard to validate. This paper proposes a fault tolerance approach for decisional planning components, which are almost mandatory in complex autonomous systems. The proposed mechanisms focus on development faults in planning models and heuristics, through the use of diversification. The paper presents an implementation of these mechanisms on an existing autonomous robot architecture, and evaluates their impact on performance and reliability through the use of fault injection.

This paper reports on the design and implementation of a real-time executive for a mobile rover that uses a model-based, declarative approach. The control system is based on the intelligent distributed execution architecture (IDEA), an approach to planning and execution that provides a unified representational and computational framework for an autonomous agent. The basic hypothesis of IDEA is that a large control system can be structured as a collection of interacting agents, each with the same fundamental structure. We show that planning and real-time response are compatible if the executive minimizes the size of the planning problem. We detail the implementation of this approach on an 'exploration rover (Gromit, an RWI ATRV Junior at NASA Ames) presenting different IDEA controllers of the same domain and comparing them with more classical approaches. We demonstrate that the approach is scalable to complex coordination of functional modules needed for autonomous navigation and exploration.

This paper presents a new approach to integrate real-time execution control in autonomous systems and how such an approach integrates in their software architecture. The use of decisional autonomy is becoming more widely accepted as a solution to the increasing need to deploy complex systems (robots, satellites, etc.) able to perform nontrivial tasks in various environments. We present an overview of the organization of such systems. Then we explain why the increasing complexity of functional components as well as the presence of autonomy components becomes an obstacle to system safety and dependability. To address this issue, we propose the integration of an execution control component in the software architecture. This component is synthesized from a model of the acceptable and dangerous state using model-checking techniques. The execution controller has a generic representation of system behavior and, according to some specified system constraints, acts as a "safety bag" allowing acceptable states and avoiding forbidden ones. The controller uses an OBDD like data structure which offers a bounded execution time, and which can be formally validated offline to check temporal properties. Real experimentations have been made on our autonomous mobile robots, and have confirmed it can catch in real-time design errors from the decisional components which would have lead to disastrous consequences.

This paper presents some recent developments of the LAAS architecture for autonomous mobile robots. In particular, we specify the role of the execution control level of this architecture. This level has a fault protection role with respect to the commands issued by the decisional level, which are transmitted to the real system (through the functional level). We introduce a new approach and a new tool inspired from the model checking domain. We present a new language to specify the model of acceptable and required states of the system (valid contexts for requests to functional module and resources usage). This language is compiled in an ordered binary decision diagram like structure which is then used online to check the specified constraints in real-time. Such model checking approach could be extended to check off line more complex temporal properties of the system.

Autonomous robots are complex machines embedding: software modules implementing basic functions such as servo loops to follow a path, or to compute stereo correlation of a pair of images; software to take into account the interactions between the robot components; programs which deal with the supervision and the planning of the mission. These components are integrated within an architecture which defines an organization and a methodology for robot operation.

Procedural reasoning systems (PRS) have inspired some works in execution control and supervision, in particular in robotics applications. However, one of the main drawbacks of the PRS is the lack of planning capabilities, even though some PRS execution mechanisms and knowledge representations are related to planning. We propose some extensions to PRS, to integrate both execution and planning in the robotics domain. In particular, we propose two planning mechanisms: plan synthesis to complement existing operational procedures by building new plans from operators; and anticipation planning, which anticipates the plans and procedures execution, to advise the execution for the best option to take when facing choices, and to forecast problems that may arise due to unforeseen situations. These new extensions rely on a common language to represent plans, planning operators and operational procedures. In particular, the description we propose makes transitions between planning activities and execution seamless. This work is used in two complex real-world problems: planning and control for our autonomous mobile robots (e.g. for delivery tasks), and for the management of the transition phases of a blast furnace.

The authors previously (1998) argued that the LAAS architecture is one of the most suitable for mobile robot control. This statement may seem over-optimistic, not to say pretentious and unverifiable. After all, can we compare architectures? can we set up benchmarks? or can we measure how good an architecture is compared to another? An architecture defines organization principles, integration methods and supporting tools. Comparing those tools, methods and principles may sometime end up in sterile controversies. However, we think there are means to measure the overall quality (or interest) of an architecture. Development time is for example one relevant criterion. Basically, using a specific architecture, how long does it take to integrate a complete demonstration, including nontrivial decisional capabilities, from the low level functional modules up to the supervisory level? This may seem a rather weak measure of architecture quality; however, it encompasses properties such as genericity and adaptability, ease of design and programming, extensibility and robustness. In this paper we describe our recent experience in integrating a complete demonstration from scratch in 40 days using the LAAS architecture.

Presents our project to develop a personal robot called Diligent. We first discuss the main issues involved in personal robotics. Then we analyze some of the key features implied by what we call "human-friendly navigation". Finally, we present the current state of Diligent. Diligent is already able to navigate safely and repeatedly in a relatively large environment. It is also capable of some preliminary human-robot interactions through very simple and intuitive commands.

We present and discuss the use of a generic scheme for multi-robot cooperation called the "plan-merging paradigm" for managing a large fleet of autonomous mobile robots. Each robot, autonomously and incrementally builds and executes its own plans taking into account the multi-robot context obtained by collecting the current plans and goals of the other robots. We describe the overall system architecture and discuss the properties of our cooperative scheme. We show how the plan-merging paradigm (PMP) can be used in a hierarchical manner and how it "fills the gap" between centralized planning and distributed execution. We finally illustrate this scheme through an implemented system which allows a fleet of autonomous mobile robots to perform load transfer tasks in a route network environment. The central activity is limited to task allocation and important gains are obtained in system flexibility and robustness to execution contingencies. Simulations (using up to 30 robots) as well as experiments with real robots (3) are presented and discussed.

Our approach in proposing the plan-merging paradigm as a cooperation scheme was to allow an efficient distribution of the decisions for a better reactivity to contingencies for multi-robot applications with loosely coupled tasks. The paradigm proved to be quite efficient because it exploits the fact that most conflicts can be solved locally and because it allows a finer overlapping between plan refinement, plan coordination and execution. We develop in this paper the mechanisms which allow one to extend this paradigm in order to obtain a scheme which distributes as much as possible the decision processes for planning and coordination while maintaining two key features: the coherence of the global system and the ability to detect the situations where it is not applicable; and a localized management of the planning and coordination processes with, in particularly intricate situations, a progressive transition to more global schemes which may "degrade" to a unique and centralized planning activity.

We discuss Procedural Reasoning System (PRS) as a high-level control and supervision language adapted to autonomous robots to represent and execute procedures, scripts and plans in dynamic environments. We discuss the main reasons why PRS is well suited for this type of application: (1) The semantics of its plan (procedure) representation, which is important for plan execution and goal refinement; (2) Its ability to construct and act on partial (rather than complete) plans; (3) Its ability to pursue goal-directed tasks while at the same time being responsive to changing patterns of events in bounded time; (4) Its facilities for managing multiple tasks in real-time; (5) Its default mechanisms for handling stringent real-time demands of its environment; and (6) Its meta-level (or reflective) reasoning capabilities. C-PRS has been used to implement an embedded control and supervision system for autonomous mobile robots in two different experimentations that we briefly present. We conclude with some suggestions to further develop C-PRS and with a short review of related work.

This paper presents an approach we have recently developed for multi-robot cooperation. It is based on a paradigm where robots incrementally merge their plans into a set of already coordinated plans. This is done through exchange of information about their current state and their future actions. This leads to a generic framework which can be applied to a variety of tasks and applications. The paradigm, called plan-merging paradigm, is presented and illustrated through its application to planning, execution and control of a large fleet of a autonomous mobile robots for load transport tasks in a structured environment.

This paper presents an implemented system which allows one to run a fleet of autonomous mobile robots in a route network with a very limited centralized activity. The robots are provided with all the necessary ingredients for planning and executing navigation missions in a multi-robot context. Multi-robot cooperation is based on a generic paradigm called plan-merging paradigm, where robots incrementally merge their plans into a set of already coordinated plans. The robot architecture is derived from the generic architecture developed at LAAS. A 3D graphic environment system allows one to display a complete system composed of a dozen (or more) robots, each running on an independent workstation. An example is presented together with numerical results on the system behavior.