| SPARCS: Synthesis of Platform-aware Attack-Resilient Control Systems |
Verified generation of glue code
A resilient control algorithm must be correctly implemented in software in order to actually deliver resilience in a system implementation. For this, we are relying on code generation from domain-specific models. In this phase of the project, we assume that the control algorithm is developed in a commonly used modeling language, such as Simulink, and rely on existing code generation tools to obtain code. However, these code generators produce platform-independent functions that cannot be executed directly. We need to add platform-specific glue code in order to deploy the control function of a specific platform. We have developed ROSGen, a tool to automatically generate glue code for conrol code to be deployed on the Robot Operating System (ROS) platform, widely used in the robotic community. ROSGen is implemented using the Coq proof assistant and relies on the infrastructure provided by the CompCert, a verified C compiler. This allows us to formally prove properties of the generated code using the Verified Software Toolchain environment, as well as correctness of the code generator itself.ROSGen is integrated with ROSLab, a tool for developing robotic applications based on ROS. ROSGen is currently being used to build a high-assurance control system for the DARPA HACMS program.
Download
The current Coq implementation of ROSGen and files related to the LandShark case study can be found here.The technical report includes the VST specifications and more details about the formal proof.