Creating safe robots with Imandra

Kostya Kanishev
Jul 9, 2018 · 3 min read

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).

Image for post
Image for post

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).

Image for post
Image for post
Visualisation of one the example robots you’ll find on our demo site.

Check our Imandra-ROS project GitHub repository and the collection of Imandra Jupyter notebooks in it:

  1. 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.
  2. Simple_ROS_Verify.ipynb notebook uses Imandra to formally verify various statements about the simple model we’ve created.
  3. 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!

Reasoning as a Service @ www.imandra.ai

Medium is an open platform where 170 million readers come to find insightful and dynamic thinking. Here, expert and undiscovered voices alike dive into the heart of any topic and bring new ideas to the surface. Learn more

Follow the writers, publications, and topics that matter to you, and you’ll see them on your homepage and in your inbox. Explore

If you have a story to tell, knowledge to share, or a perspective to offer — welcome home. It’s easy and free to post your thinking on any topic. Write on Medium

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store