Creating safe robots with Imandra
From self-driving cars to medical surgeons, robots have become ubiquitous. Ensuring they operate safely and correctly is evermore important. The most popular middleware for robotics is the open-sourced Robot OS. We have begun work on developing an Imandra interface to Robot OS, opening up the world of robotics to the latest advancements in automated reasoning. In this post, we showcase our early results, discuss our roadmap and our submission for a talk at the upcoming ROSCon 2018 (Madrid, Spain).
Robot Operating System (ROS) is a robotics middleware framework, consisting of a package manager, a collection of standard libraries and simulators, and a message-passing middleware system. ROS adopts a distributed architecture for robotic computing enabling independent nodes to communicate via messages across the ROS computation graph.
While having many practical advantages, such distributed systems are inherently much more complex and difficult to reason about. To ensure that the software controlling such a distributed system is correct we need to turn to formal verification — mathematically reasoning about the correctness of computer programs.
At Aesthetic Integration, we are developing methods and tools for formally reasoning about distributed message-passing systems such as ROS. Imandra by Aesthetic Integration is both a reasoning engine and a programming language which you can use to analyse and verify properties of the programs written in Imandra Modelling Language (IML, a purely functional subset of OCaml). Imandra is able to reason about your code and, being valid OCaml, the same code can be compiled and executed.
To further improve the developer experience, Imandra provides its own Jupyter kernel that allows one to interactively develop, document and share Imandra models via computational notebook interfaces. If you want to give Imandra notebook a try, visit https://try.imandra.ai/ to explore our collection of introductory notebooks and run your own Imandra kernel instance in the cloud. We’re working on a version of Imandra that our users will be able to download and use locally – stay tuned!
ROSCon is the annual conference for ROS developers and will take place this September in Madrid, Spain. We proposed a talk that will demonstrate how one can use Imandra to formally verify the behaviour of ROS nodes. We’ll present our open-source IML/OCaml interface to ROS and demonstrate several examples of simple executable robot controller nodes (the source code is available at http://try.imandra.ai).
Check our Imandra-ROS project GitHub repository and the collection of Imandra Jupyter notebooks in it:
- Simple_ROS_Node_Model.ipynb notebook explains how to create a simple ROS node in Imandra and then compile and run it as a part of the ROS system.
- Simple_ROS_Verify.ipynb notebook uses Imandra to formally verify various statements about the simple model we’ve created.
- ROS_Verify.ipynb notebook loads a more complex ROS node model and illustrates how one can use Imandra to prove some of the model properties and investigate the counterexamples that Imandra produces when failing to prove some of them.
Hope to see you at ROSCon!
