Keywords

1 Introduction

Wheeled robots are popular because of the simplicity and versatility of their components. Nowadays, autonomous wheeled robots are being used for complex tasks, including space exploration, mission-critical military applications, and precision agriculture. The integration of a vast amount of sensors and their interaction with the environment, make these robots highly concurrent. This scenario poses a significant challenge for guaranteeing correct behavior such as safe navigation, precise goal tracking, and fault tolerance [2]. Moreover, because of the high value of some of the components and the costs associated to malfunction (e.g., money investment, human lives, or crop production), autonomous robots are expected to be highly reliable [13].

The robotics community has developed near-real simulation environments to test control architectures in operation conditions that can help in design-testing a robot development before its deployment. Nevertheless, due to the intrinsic limitations of simulation-based testing, these environments are far from answering the important question of, up to a high degree of confidence, how reliable control architectures really are. The inherent non-deterministic nature of robot autonomy, and the divide between the mathematical properties and the operational semantics of the language used to program the robot, can make this situation more dramatic. For example, an extensive test-guided validation in the design phase of a robot development could suggest absence of deadlocks in a control architecture. However, deadlocks may be present in the resulting implementation because of semantic issues with synchronization structures in the programming language.

Today’s formal methods are scaling up to meet the challenges in the development of mission-critical software and hardware. The notion of software/hardware verification via automatic reachability analysis or model checking has evolved to become an accepted technology in development processes. Moreover, new symbolic techniques based, e.g., on the satisfiability modulo theories (SMT) approach are being readied for industrial use as a solution to the state-explosion problem, commonly faced in the algorithmic verification of concurrent systems. Nowadays, formal methods are being used in the development, e.g., of unmanned aircraft systems [15] and have had big impact in the design of policies for unmanned aircraft systems [25]. A key benefit of the formal methods approach is that it provides techniques, tools, and insights highly valuable in a mission-critical development.

This paper presents a hybrid control architecture, based on the Plan Execution Interchange Language [6] (\(\text {PLEXIL}\)), for autonomy of wheeled robots running the Robot Operating System [8] (\(\text {ROS}\)). \(\text {PLEXIL}\) is a synchronous reactive language created by NASA for mission-critical robotic systems. \(\text {ROS}\) is one of the most popular frameworks for robotics middle-ware development. The proposed hybrid architecture is given in a deliberative/reactive/driver layered setting. \(\text {PLEXIL}\) is used in the reactive layer to implement behavior in a mission plan with a hierarchical composition of nodes, where the ones at the top represent high-level behavior and the ones at the bottom basic actions (e.g., primitive robot commands and variable assignment). On the other hand, \(\text {ROS}\) (and its drivers) is used to represent components specific to wheeled robots as a hardware abstraction at the level of the robot’s sensors. The deliberative layer, where mission plans are generated according to some given goals, is not directly addressed in this paper. The technical contribution of this paper can now be better explained. The integration between \(\text {PLEXIL}\) and \(\text {ROS}\) is a bi-directional software adapter between the reactive and driver layers. This adapter enables: (i) the execution of \(\text {PLEXIL}\) low-level commands in a wheeled robot running \(\text {ROS}\), and (ii) the interaction of \(\text {PLEXIL}\) with the external environment via events triggered by sensors under the control of \(\text {ROS}\) in the driver layer. This approach is showcased in a path tracking scenario using the Husky robot platform via a Gazebo simulation.

The integration of \(\text {PLEXIL}\) and \(\text {ROS}\) presented in this paper has the additional benefit of making available to \(\text {ROS}\)-enabled robots all the formal analysis and verification tools already developed for \(\text {PLEXIL}\). These tools include a rewriting logic semantics in Maude [5], an interactive environment for automatic reachability analysis and LTL model checking [22], and automatic symbolic reachability analysis based on rewriting modulo SMT [23]. This integration opens the door of formal verification to a wide class of \(\text {ROS}\) modules, thus making autonomous planning more reliable. Furthermore, new plans can now be developed following a more rigorous formal methods-oriented approach.

The rest of the paper is organized as follows. Section 2 reviews some related work. Sections 3 and 4 present, respectively, a high-level description of \(\text {PLEXIL}\) and \(\text {ROS}\). Section 5 proposes the layered architecture based on the \(\text {PLEXIL}\)-\(\text {ROS}\) integration and Sect. 6 exhibits a proof of concept. Section 7 concludes the paper.

2 Related Work

There is a vast amount of research in the field of control architecture for autonomous robots. Control architectures can be classified in several categories: by the type of interaction between control modules (e.g., hierarchical or centralized architectures), by the type of functionality assigned to each module (e.g., general or specific purpose), and by the way modules interact with the external environment (e.g., event-based or procedural behavior). The latter category, which is closest to the proposal in this paper, can be further classified as deliberative, reactive, or hybrid. In a deliberative control architecture, a plan is generated based on a goal and a static model of the environment targeted after successful operation. In a reactive control architecture, control commands are generated during operation based on interaction with the environment. In a hybrid control architecture, a deliberative agent statically generates plans that will be executed by reacting to the external environment during operation. Fairly complete surveys of works in each category and subcategory are [13, 17, 27].

There are significant efforts to have reliable and modular hybrid control architectures for autonomy in robotic systems. On the one hand, the main focus is on using languages with mathematically proven properties, e.g., \(\text {PLEXIL}\) as the intermediate layer for plan representation and execution. On the other hand, the main focus is on defining control structures on top of \(\text {ROS}\)-enabled systems. Muñoz et al. [16] propose a control architecture for the Ptinto robot, a hexapod robot for exploration in difficult terrains. They use \(\text {PLEXIL}\) as the intermediate plan specification language and reactive layer for SGPlan (a deliberative planner that automatically partitions large planing problems into subproblems with specific goals). However, in their work, the hardware abstraction layer is proprietary and therefore the architecture is tied to the specific target robot. Jenson et al. [10], propose a control architecture for AMIGO and other \(\text {ROS}\)-enabled robots to perform tasks in human environments. Their system uses a hierarchical ordered planner, a special type of deliberative system in which a predefined set of actions is hierarchically arranged once a goal is set for the autonomous robot. Benjamin et al. [1] propose ROSoClingo, a control architecture with a reactive layer for \(\text {ROS}\)-enabled robots. Their approach uses answer set programming (ASP), a declarative programming paradigm intended to solve NP-hard combinatorial search problems. The proposed architecture encodes adaptive behaviors directly in a declarative knowledge formalism, which requires the addition of reactive capabilities not necessarily available from the target robot.

It is fair to say that the main difference between the above-mentioned works and the proposal in this paper, is that the latter aims at combining the best elements of both worlds: a robust, mathematically verifiable high-level language such as \(\text {PLEXIL}\) for the reactive layer, and \(\text {ROS}\), the actual de-facto standard for robotic middle-ware. This unique combination brings an important advantage to future projects in robotics. Namely, the possibility of having verified – and eventually certified – control architecture software for autonomous robots that use conventional and affordable hardware.

3 The Plan Execution Interchange Language

The Plan Execution Interchange Language [6] (\(\text {PLEXIL}\)) is a synchronous reactive language developed by NASA to support autonomous spacecraft operations. It has been used on applications such as robotic rovers, a prototype of a Mars drill, and to demonstrate automation capabilities for potential future use on the International Space Station. Programs in \(\text {PLEXIL}\), called plans, specify actions to be executed by an autonomous system as part of normal spacecraft operations or as reactions to changes in the environment. The computer system on board the spacecraft that executes plans is called the Universal Executive [26].

3.1 PLEXIL in a Nutshell

A \(\text {PLEXIL}\) plan consists of a set of nodes representing a hierarchical decomposition of tasks. A leaf node in the tree represents a primitive task such as variable assignment or a command execution, whereas an intermediate node defines the control structure of its descendants such as sequential or concurrent execution. Each node is equipped with a set of conditions that trigger its execution, e.g., a start condition and an end condition. At any time, each node offers information about its execution state: inactive, waiting, executing, iterationended, failing, finishing, or finished. There is also information about the termination status of a task: success, skipped, or failure.

When events are reported by interaction with the external environment (e.g., by sensors or timers), the nodes triggered by such events are executed concurrently, updating e.g., local variables, until quiescence. The internal execution of each node, in turn, can trigger the execution of other nodes. Although more than one event can become enabled simultaneously, all parallel operations in \(\text {PLEXIL}\) are synchronized and will not arbitrarily interleave. This is because \(\text {PLEXIL}\) semantics is designed under the synchronous hypothesis [18]. One important feature of \(\text {PLEXIL}\) semantics is that it guarantees determinism (in the absence of external events), which is a convenient property for autonomous programming because it helps in having a clean mathematical semantics.

As an example, consider the simple \(\text {PLEXIL}\) plan in Fig. 1. It consists of a tree with three nodes: the root node SamplePlan, and the leaf nodes ActionOne and ActionTwo. In this plan, there are two integer variables, namely, x and y, which are accessible from any node in the plan. The run-to-completion semantics of the leaf nodes depends on the value of the variable sensorOne, which is under control of the external environment. For instance, if the value of sensorOne becomes 201, then both leaf nodes will execute in parallel. In an asynchronous setting, such an execution would result in an unpredictable outcome because of the race condition in the assignment of x and y. However, thanks to its synchronous semantics, \(\text {PLEXIL}\) guarantees a consistent variable swap in this case so that x is assigned the value 20 and y is assigned the value 10, without any race condition.

Fig. 1.
figure 1

A very simple \(\text {PLEXIL}\) plan.

3.2 Rewriting Logic-Based Automatic Analysis

\(\text {PLEXIL}\) has been designed with verification and validation in mind, and has motivated the development of an important amount of research and tools in the rewriting logic community. Rewriting logic [14] is a semantic framework that unifies a wide range of models of concurrency. Specifications in rewriting logic are called rewrite theories and can be executed in the rewriting logic implementation Maude [4]. By being executable, they benefit from a set of formal analysis tools available to Maude, such as state-space exploration and automata-based LTL model checking. A rewrite theory is a tuple \(\mathcal {R}= (\varSigma , E \uplus B, R)\) with: (i) \((\varSigma , E \uplus B)\) an order-sorted equational theory with signature \(\varSigma \), E a set of equations over the set \(T_\varSigma \) of \(\varSigma \)-terms, and B a set of structural axioms – disjoint from the set of equations E – over \(T_\varSigma \) for which there exists a finitary matching algorithm (e.g., associativity, commutativity, and identity, or combinations of them); and (ii) R a finite set of rewrite rules over \(T_\varSigma \). Intuitively, \(\mathcal {R}\) specifies a concurrent system whose states are elements of the set \(T_{\varSigma /E\uplus B}\) of \(\varSigma \)-terms modulo \(E \uplus B\) and whose concurrent transitions are axiomatized by the rewrite rules R. In particular, for \(t,t' \in T_\varSigma \) representing states of the concurrent system described by \(\mathcal {R}\), a transition from t to \(t'\) is captured by a formula of the form \([t]_{E\uplus B} \rightarrow _\mathcal {R}[t']_{E\uplus B}\); the symbol \(\rightarrow _\mathcal {R}\) denotes the binary rewrite relation induced by R over \(T_{\varSigma /E\uplus B}\).

The ground rewriting logic semantics of \(\text {PLEXIL}\) [5] is a rewrite theory \(\mathcal {R}_\text {PLEXIL}\) with topsort \(\mathfrak {s}\), meaning that concurrent transitions in the system are mathematically captured by \(\rightarrow _{\mathcal {R}_\text {PLEXIL}}\) and are over the set \(T_{\varSigma ,\mathfrak {s}}\) of \(\varSigma \)-terms of sort \(\mathfrak {s}\). The symbolic rewriting logic semantics of \(\text {PLEXIL}\) [21, 23], based on the rewriting modulo SMT technique, is a rewrite theory \(\mathcal {S}_\text {PLEXIL}\) with topsort \(\mathfrak {s}\times \varGamma \), meaning that symbolic concurrent transitions in the system are mathematically captured by \(\rightarrow _{\mathcal {S}_\text {PLEXIL}}\) and are over state pairs of the form \(\left( t \,; \varphi \right) \) with \(t\in T_\varSigma (X)_\mathfrak {s}\) and \(\varphi (X)\) a quantifier-free first-order logic formula under the control of the SMT solver. Intuitively, a symbolic state \(\left( t \,; \varphi \right) \) in \(\mathcal {S}_\text {PLEXIL}\) can represent infinitely many concrete states, namely, those states \(t\sigma \) for each ground substitution \(\sigma \) satisfying \(\varphi \). The constraint \(\varphi \) in a symbolic state is used to model the behavior of variables under control of the external environment. Techniques and tools for reachability analysis and LTL model checking with \(\rightarrow _{\mathcal {R}_\text {PLEXIL}}\) and \(\rightarrow _{\mathcal {S}_\text {PLEXIL}}\) have been developed. They have been used for detecting the violation of safety properties such as invariants, race conditions, and deadlock freedom. For details, the reader is referred to [22, 24].

4 The Robot Operating System

The creation and development of robots involves the interaction and collaboration of several areas of knowledge such as mechanics, electronics, and computer science. For example, once a robotic device has been mechanically designed and its electronic components able to read data from the environment, software artifacts may be developed to pursue autonomy. In general, a large-span robotics project can require a vast amount of collaborative effort – both in time and money. Thus, it would be highly convenient to reuse as many artifacts as possible across similar projects.

An open source initiative promoted by Willow Garage has emerged and, as a result, the Open Source Robotic Foundation (OSRF) has been established recently. The Robot Operating System (\(\text {ROS}\)) has been created by the OSRF with the goal of increasing the reusability of the software components specifically developed for robots. The adoption of \(\text {ROS}\) can also dramatically decrease the time and money needed to deploy robot applications. During the past few years, \(\text {ROS}\) has gradually become the de-facto standard in robot development. For example, the paper [19] introducing \(\text {ROS}\) has been cited 3350+ times since 2009. \(\text {ROS}\) has not only gained a distinguished position in the research community, but it has also become an important player in the robot manufacturing industry: the \(\text {ROS}\) Industrial Consortium has the support of 42 of the most prestigious robot manufacturers in the world.

The Robot Operating System is defined in [8] as follows:

\(\text {ROS}\) is a meta-operating system for your robot. It provides the services you would expect from an operating system, including hardware abstraction, low-level device control, implementation of commonly-used functionality, message-passing between processes, and package management. It also provides tools and libraries for obtaining, building, writing, and running code across multiple computers.

\(\text {ROS}\) has been designed to be modular at a fine-grained scale, where the basic unit is a node representing a process. For example, one node can control a laser range-finder, or the wheel motors, or perform localization. A robot application in \(\text {ROS}\) can be specified as a computation graph representing the peer-to-peer network resulting from node interaction: an edge in this graph denotes message-passing communication between two processes. Figure 2 depicts a graph corresponding to a \(\text {ROS}\) program.

Fig. 2.
figure 2

An example of a \(\text {ROS}\) program. It is a graph where a node is a process providing or obtaining data from other processes. Related processes are linked by edges and denote interaction based on message passing.

Tools are provided by \(\text {ROS}\) to analyze and visualize data, simulate robots and environments, and to store large amounts of data generated by sensors and processes. For instance, RViz [9] and Gazebo [7] are useful tools to visualize and analyze the data captured by sensors and kinematics. RViz has been designed to visually interact with almost all processes running in a \(\text {ROS}\) graph. Gazebo, on the other hand, is an open source 3D dynamic simulator [11], which will be included by the OSFR in modern distributions of \(\text {ROS}\).

Figure 3 depicts the interaction between the Gazebo simulation environment and a Husky robot deployed in an environment with obstacles. On the left, a computer simulation of the environment can be seen. On the right, a RViz application is shown with the information retrieved by several sensors. For example, data captured from the camera and laser mounted on the Husky has been interpreted and drawn by RViz.

Fig. 3.
figure 3

Example of interaction between the Gazebo simulation environment and a Husky robot deployed in an environment with obstacles.

One key effort in \(\text {ROS}\) has been the standardization of message-passing and the abstraction of the format they use. Messages are important in \(\text {ROS}\) because they are at the heart of interaction infrastructure. Each message in \(\text {ROS}\) is a data structure comprising different types of fields such as integers, floating point values, Booleans, and arrays of primitive types. For example, the Twist message format is part of the geometry package in \(\text {ROS}\), and is used to communicate linear and angular velocities of a body:

figure a

The message standardization in \(\text {ROS}\) makes it possible to create a clean hardware abstraction layer (HAL) between hardware and software. In particular, it makes it possible to define a common communication channel between software components that control the behavior of the robot and the hardware components actually enforcing such a behavior. In this sense, \(\text {ROS}\) reduces the effort of tailoring software components to each particular kind of robot. For example, in \(\text {ROS}\), any robot can be commanded to move by using the Twist message by indicating the linear and angular velocities. \(\text {ROS}\) assumes that each robot will execute this command accordingly to its own “anatomy”. In the case of wheeled robots, only linear velocity has an important meaning since the angular velocity in the axis of movement is perpendicular to the floor. In the case of aerial vehicles, they can be commanded to change position by using three linear and three angular velocities, without any kinematic restriction.

5 Layered Architecture for the Integration

This section presents the main contribution of this paper. The key idea is to use \(\text {PLEXIL}\) as reactive layer and thus, by taking advantage of all automatic formal analysis techniques and tools available to it, enable the development of autonomous control modules for \(\text {ROS}\) with high degrees of reliability.

The proposed architecture is depicted in Fig. 4. It is based on the hybrid deliberative/reactive paradigm (see Sect. 2) and has the following elements:

  • The top layer (or deliberative layer): a software component that uses a global “environment model” (e.g., it contains terrain features and obstacles) and on a set of goals or problem description. It ultimately generates a mission plan composed of subtasks required to accomplish the goals in the given world model.

  • The deliberative/reactive binding layer: a software component responsible for providing compatibility between the format of the mission plan generated by the planner in the deliberative layer and the language used to describe the hierarchy of action nodes in the reactive layer.

  • The reactive layer: a hierarchical composition of nodes in which nodes at the top represent high-level behavior in the mission plan and the ones at the bottom represent basic actions in the plan (e.g., primitive robot commands and variable assignment).

  • The driver layer: a software component using \(\text {ROS}\) and the \(\text {ROS}\) drivers required for the specific robot components. This layer represents the hardware abstraction for the robot at the level of sensor actions and their access.

Fig. 4.
figure 4

Proposed \(\text {ROS}\) and \(\text {PLEXIL}\) layered architecture.

In particular, the control architecture resides in the reactive layer. On the one hand, this layer handles information from the environment such as changes on Yaw or position coordinates, which are updated based on data received via the driver layer from \(\text {ROS}\) drivers. On the other hand, the hierarchical composition of nodes in this layer has, at the top level, goal-oriented nodes such as driving straight for a distance or following a sequence of points. Such nodes will decompose in lower-level action nodes that, for instance, can perform tracking strategies such as follow-the-carrot or pure-pursuit [12] by calculating the required speed and steering settings.

As a proof of concept, a general purpose \(\text {PLEXIL}\)-\(\text {ROS}\) adapter has been developed by the authors, following the ideas proposed as future work in [3]. Conceptually, this adapter transforms \(\text {ROS}\) events triggered by the environment into variables that \(\text {PLEXIL}\) plans can handle, and \(\text {PLEXIL}\) commands into requests to \(\text {ROS}\) driver nodes. Figure 5 depicts how the \(\text {PLEXIL}\)-\(\text {ROS}\) adapter integrates \(\text {PLEXIL}\) plans and \(\text {ROS}\) nodes, transforming the data that flows from the layers when necessary:

  1. 1.

    The \(\text {PLEXIL}\) Universal Executive executes the plan defined for the reactive layer of the architecture using a \(\text {PLEXIL}\) adapter.

  2. 2.

    The adapter defines the low-level operations and environment variables for such a plan.

  3. 3.

    The adapter uses an interface that is subscribed to relevant events in \(\text {ROS}\).

  4. 4.

    The adapter transforms the generated events by updating environment variables and handles command invocation by publishing \(\text {ROS}\) events.

  5. 5.

    The message-oriented middle-ware of \(\text {ROS}\) (ROSCORE) enables the indirect communication with a real or simulated robot.

Fig. 5.
figure 5

Proposed \(\text {PLEXIL}\)-\(\text {ROS}\) integration architecture.

As a technical detail, it is important to note that in order to ensure that the \(\text {PLEXIL}\) plan in the reactive layer is able to check that the environment information has been initialized – preventing the initialization of the plan with inconsistent data –, a special variable called ‘Ready’ is assigned true when \(\text {ROS}\) reports the status of the robot for the first time. The current implementation of the adapter, for testing purposes, is based on the Husky platform [20].

6 Proof of Concept

This section presents a proof of concept of the implementation of the \(\text {PLEXIL}\)-\(\text {ROS}\) adapter proposed in Sect. 5. The Husky robot platform – via a Gazebo simulation – and a basic path tracking scenario were chosen for the experiment. The goal of the experiment is to demonstrate how a \(\text {PLEXIL}\) plan in the reactive layer can command a \(\text {ROS}\)-enabled robot whose drivers are in the hardware-abstraction layer. Note that for the purpose of this paper, the plan has been developed manually and without the help of a deliberative layer software.

The experiment is the following: make a Husky follow a fixed-size square-shaped path specified by a \(\text {PLEXIL}\) plan. Figure 6 depicts the logical description of the plan as a tree of tasks and Listing 1.1 presents the code of the plan. Intuitively, the \(\text {PLEXIL}\) plan consists of:

  • Two high-level nodes: move forward for a given distance and turn a given amount of degrees.

  • The plan performs four consecutive iterations of the sequence: move N meters, stop, and turn 90 degrees.

  • The Move node is defined as a sequence of two nodes: OdometryUpdate and MoveUntilDistanceReached. The first one performs a lookup of the current position and the second one performs a LinearVelocityRequest until the repeat condition is not met (i.e., until the distance from the starting point to the current position is less than the expected distance).

  • Angular velocity is continuously requested by Stop.

  • Node Turn re-calculates the angular displacement every time a new Yaw is reported. Once the angular displacement is approximately close to the expected one, CompleteTurnCheck makes StaticTurn reach the final (i.e., FINISHED) state in the plan.

Fig. 6.
figure 6

\(\text {PLEXIL}\) plan tree for the proof of concept.

figure b

Finally, Fig. 7 shows a superposition of screenshots of the simulation executed in Gazebo.

Fig. 7.
figure 7

Gazebo simulation.

7 Concluding Remarks

Designing and developing control software for an autonomous robot is a challenging and complex task, specially considering that – with cyber-physical systems – the costs of failure or unexpected behaviors can be dramatic. Unfortunately, formal verification methods, a powerful set of techniques and tools aimed at ensuring software correctness and reliability are not easily accessible to most robot developers. Although \(\text {ROS}\) has simplified the development of robotic solutions with its low level control layer commanding a robot to perform desired movements, moving the actuators (e.g., servo-motors), and process data provided by sensors, the problem of identifying control flaws is far from solved. Common flaws include deadlocks, violation of conformance to temporal, spatial, or timed constraints, which are key to mission-critical applications.

This paper has presented a software architecture and implementation for integrating \(\text {PLEXIL}\) and \(\text {ROS}\). The main idea is to use \(\text {PLEXIL}\), a synchronous reactive language created by NASA for mission critical robotic systems, in the reactive layer in a hybrid architecture to command \(\text {ROS}\)-enabled robots. \(\text {PLEXIL}\) has been proved to be mathematically reliable and robust by the scientific community. Given the fact that during the past 10 years \(\text {ROS}\) has become a de-facto standard in robotics, both in research and in industry, the \(\text {PLEXIL}\)-\(\text {ROS}\) integration can have positive impact in the development of mission-critical plans for autonomy in rovers. For example, it offers automatic verification techniques and tools already available for \(\text {PLEXIL}\) to \(\text {ROS}\) programmers. The proposed architecture has been validated and illustrated with an example consisting of an autonomous plan written in \(\text {PLEXIL}\) for a wheeled \(\text {ROS}\)-enabled robot.

Future work will integrate \(\text {PLEXIL}\)-compatible modules in the deliberative layer, which will be tested with specific tasks. They can include strategic areas in Colombia where reliable automation is needed. These include, for instance, precision agriculture. On the other hand, it will be ideal to deploy an official \(\text {PLEXIL}\)-\(\text {ROS}\) package to make the integration of components and the validation environments above-mentioned fully available to the \(\text {ROS}\) programming community. The feedback from the \(\text {ROS}\) community will be a valuable input for future stages of this project. Finally, specific-purpose verification techniques and tools need to be developed for the \(\text {PLEXIL}\)-\(\text {ROS}\) integration depending on the area of use.