ABSTRACT
The paper considers the problem of model-based deployment of platform-independent control code on a specific platform. The approach is based on automatic generation of platform-specific glue code from an architectural model of the system. We present a tool, ROSGen, that generates the glue code based on a declarative specification of platform interfaces.
Our implementation targets the popular Robot Operating System (ROS) platform. We demonstrate that the code generation process is amenable to formal verification. The code generator is implemented in Coq and relies on the infrastructure provided by the CompCert and VST tool. We prove that the generated code always correctly connects the controller function to sensors and actuators in the robot. We use ROSGen to implement a cruise control system on the LandShark robot.
PROOF ENVIRONMENT
Fig. 1. ROSGen dependency structure.
Figure 1 shows the tools underlying ROSGen, which are briey described below.
Coq. The Coq Proof Assistant2 is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
CompCert. CompCert is a formally verified optimizing compiler for the C programming language that currently targets PowerPC, ARM and 32-bit x86 architectures. The compiler is specified, implemented and proved correct using the Coq proof assistant. It targets embedded systems programming, with stringent reliability requirements. CompCert’s source language, a large subset of C called Clight, is the target language of our code generator; our generator pro- duces abstract syntax values for Clight.
ROS-BASED CONTROL SYSTEM
Fig. 2. ROS-based controller system skeleton.
Figure 2 shows the skeleton of a ROS-based control system. In order to subscribe to a topic in ROS, users need to define a callback function. A callback function for a topic is a message handler that is invoked to process the new messages when they arrive. Subscribe is a function from the ROS API that registers subscription information: a topic name, the message type, the internal buffer size and the callback function for those messages.
Fig. 3. LandShark robot.
In this section we illustrate a typical ROS-based control system using the LandShark robot. The LandShark is an electric unmanned ground vehicle, shown in Figure 3, manufactured by Black-I Robotics.4 Our case study develops a constant-speed cruise control algorithm that is resilient to attacks on vehicle sensors.
Fig. 4. LandShark control system architecture.
Figure 4 shows the architecture of the LandShark control system, which consists of sensor/actuation/controller nodes and the connections between them through topic-based pub/sub communication. The ROS nodes landshark gps and landshark base are associated with sensors that read GPS and wheel encoder values respectively and publish them. The ROS node landshark wheel velocity subscribes to the series of wheel encoder values and publishes the velocity of the vehicle calculated from them.
CODE GENERATION
Fig. 5. Verified code generation toolchain.
Our tool chain for verified code generation appears in Figure 5. The ROSLab tool supports the design of system architectures, allowing the creation of a diagram block using a graphical user interface. The diagram block in ROSLab can then be exported in our architectural description language as a ROS node model. With the ROS node model, ROSGen produces an abstract syntax tree for a subset of C called Clight, by instantiating a Clight AST template.
Fig. 6. Top-level template.
Code generation proceeds by instantiating templates that are Clight AST fragments. We use a top-level template, representing the whole pro- gram, and a set of local templates. The top-level template is shown in Figure 6. The program contains a list of global definitions and the name for the main function. A global definition can be either a variable definition or a function definition.
CODE PROOF
Fig. 8. Data delivery correctness property for ROS-based control system.
As shown in Figure 8, the specifications of the functions capture the DDC property of the generated AST instance. The callback functions are responsible for transferring sensor messages to global message variables; the input glue function is responsible for transferring global message variable to the input parameter of controller function; and the output glue function is responsible for transferring output of controller function to the parameters of publish function.
Fig. 9. DDC specification of input glue functifon.
As shown in Figure 9, the input glue function has the precondition that there are three global message variables with values and controller input Controller U with an unknown value. The post condition indicates that Controller U contains the right value from corresponding fields defined in the ROS node model and that the values of those three global variables are unchanged. By satisfying this post condition, we can guarantee that the input to the controller function is consistent to the architecture ROS node model.
CODE GENERATOR PROOF
Fig. 11. Relation consistency of the input glue function.
The first property can be proven by showing that the lists of expressions are consistent with the ROS node model interface relation, as stated by the lemma in Figure 11. In this lemma, lg_expr is the list of expressions for global_expr, while lc_expr is the list of expressions for con_trolexpr. The quantified variable lir is the list of interface relations from Table 1. To prove the consistency, we verify that the fields of these expression lists are identical to the fields in the interface relation.
Fig. 12. Type checking for input glue function.
For the valid assignment property, we only need to check that the lists of types for the left and right sides of the assignment are consistent. The type checking function for the input glue function is shown in Figure 12. Since users may specify an inconsistent ROS node model, mapping a ROS message field with one type to controller input with a different type, the generated assignment can be invalid. The type checking function is applied before generating the input glue function.
RELATED WORK
There has been much work on automatic generation of platform-specific glue code based on the architectural model of the system and the underlying platform specification. In code generation for a variety of platforms is performed using AADL models to represent hardware and software architectures and their properties relevant for code generation. None of these papers targeted the ROS platform. More importantly, they do not consider verification of the generated code nor the code generator itself.
There is also a similarity between the intent of our approach and verification of model transformations in domain-specific languages. Most of that work, how- ever, is done in the context of behavioral models, with the goal of ensuring that syntactic constraints are preserved by the transformation. By contrast, we start with an architectural model, where behavior is implicit, and generate executable code.
CONCLUSIONS
We propose a verified framework ROSGen for generating glue code for ROS- based control systems. We start with a model of a ROS node capturing external connections of the node and parameters needed to execute the node. The code generator, implemented in Coq, uses this model to instantiate Clight templates and use the VST toolset to reason about the code.
We then use CompCert utilities to generate C source code from Clight AST. We discuss how to generalize the proof of data delivery correctness for the generated code to a proof of data delivery correctness for the code generator itself. We apply the approach to the cruise control system for the LandShark robotic vehicle.
Our plans for future work include extending the proof approach to directly reason over quantified Clight templates, allowing for a more natural proof of the code generator correctness. Furthermore, we plan to extend the framework to cover the step function, to be able to reason about control-related properties of the code, in addition to the data delivery properties.
Source: University of Pennsylvania
Authors: Wenrui Meng | Junkil Park | Oleg Sokolsky | Stephanie Weirich | Insup Lee