ROS Resources: Documentation | Support | Discussion Forum | Service Status | Q&A

Formal verification of ROS nodes using Imandra reasoning engine

Hello! We at Aesthetic Integration are developing tools and techniques for formal verification of distributed systems. For our ROS-related project, we are working on OCaml client for ROS and we are creating tools and wrappers that allow one to formally reason about ROS node models. With our Imandra reasoning engine you can formally verify statements about models written in OCaml, and the same model can be compiled and executed as a ROS node.

Check our medium post: where we are describing our approach to the creation of a simple model of a ROS node.

1 Like