# Imandra interface to Robot OS: Part II

At AI, we’ve been working on an IML (Imandra Modelling Language) interface to ROS, allowing one to develop ROS nodes and use Imandra to verify their properties. This post is the second of the 2-part sequence (check out the Part I here) where we demonstrate how to create and verify a simple ROS node model in Imandra. We’ll illustrate how Imandra may reason about our ROS node by formally verifying some of its properties and describing its behaviour with mathematically precise statements.
(There is an
Imandra notebook version of the two posts, that you can try live in the cloud.)

Formal verification is the process of reasoning mathematically about the correctness of computer programs. We can use the Imandra reasoning engine to formally verify some properties of the ROS node model we’ve created.

## Verifying outgoing `Twist` message at `Clock` ticks

Our model is designed in such a way that it updates its state parameters upon `LaserScan` messages and sends out `Twist` control messages in response to `Clock` messages. Let’s verify a simple theorem that on every incoming `Clock` message, there is an outgoing `Twist` message. We can formally write this statement down as:

This means that for every state `s`, if the state contains an incoming `Clock` message, then the system will respond by sending an `outgoing` `Twist `message (i.e., in the next `state` obtained as `one_step(s)`). We can almost literally encode this formal expression as an Imandra `theorem`:

When we ask Imandra to reason about this, it comes back with Proved, meaning that it has constructed a mathematical proof that the statement holds true. Here’s a snippet of its evidence (for the complete proof and code, see this Notebook):

## Verifying that we never drive backwards

As another example, let us check that, no matter what, the node will never send out a message with negative linear velocity. That is, we will never “drive backwards.”

Passing that conjecture to Imandra, we’ll get a response that our conjecture was “Refuted” and Imandra has created a counterexample `CX` module for us. This module contains concrete values for the parameters that illustrate a concrete violation of the statement’s condition. Let’s examine the value of `CX.state`:

The counterexample `state` produced by Imandra has the `incoming` message set to `None` and the `outgoing` message set to a `Twist` message with negative `linear.x`. Our `one_step` function keeps the state unchanged if the incoming message is empty.

We can either consider this behavior as a bug and change our `one_step` implementation; or we can consider this a normal behavior and amend our theorem, adding the non-empty incoming message as an extra premise of the theorem:

Passing that to Imandra, we see that it is able to formally prove this claim. We’ve proven that the model never creates negative linear speed in response to any incoming message — alternatively we can set `state.outgoing = None` as a premise, proving that an empty `outgoing` message is never filled with a `Twist` with negative velocity.

# Inductive proofs. Stopping near objects.

As a final formal verification goal, we want to be able to prove that the robot stops and starts turning if one of the values in the scanner `ranges` is lower than 0.2 meters. In general, reasoning about variable-sized lists (i.e., arbitrary length sequences) requires inductive proofs — and these might require proving some lemmas. So, we will first try to prove a simpler version of the theorem — if all the ranges in the incoming laser scan message are less than 0.2 meters, then we definitely transition to the `Turning` state. We’ll try to encode our theorem using `List.for_all` standard function:

Passing that to Imandra, we see that we have failed to prove the statement and Imandra has created a counterexample `CX` module for us. Examining the counterexample `state` we notice that the incoming `laserScan_ranges` list is empty.

Adding the extra requirement that the list is not `[]`, we successfully verify the statement:

Imandra successfully proves the `stopping_if_for_all` theorem, but our ultimate goal is to prove the theorem when any of the values in `laserScan_ranges` are less than the safety cutoff.

If we simply try to replace the `List.for_all` with `List.exists`, Imandra will fail to either prove or disprove the theorem, but will give us hints (“Checkpoints”) suggesting lemmas we should prove. Moreover, we can use Imandra’s bounded model checking tools (via `verify`) to verify that there exist no counterexamples to this conjecture up to a given depth (by default, up to a recursion unrolling bound of `100`). Imandra performs this bounded verification in just a few seconds. This gives us strong evidence that our conjecture is indeed true.

Armed with that evidence, we next use Imandra to prove this goal for all possible scenarios by breaking this final theorem into several smaller steps, making a rough “sketch” of the inductive proof we want and asking Imandra to fill in the gaps.

As a first step, we extract the anonymous threshold function and prove a lemma that if the `get_min_range` function returns a value satisfying the threshold, then the conclusion about the `one_step` function holds:

Next, we prove a “bridge” lemma that connects two statements about the `get_min_range` and the `List.exists` functions in their relation to the `under_threshold` predicate. This proof requires induction — to tell Imandra to use induction one should add the `[@@induct]` attribute to the theorem declaration:

Finally, we `[@@apply]` the two lemmas above to prove our final theorem with the `List.exists` condition:

# Conclusion

We’ve created a model of a Robot OS node together with a collection of formally verified theorems about it. Imandra helped us to iteratively create and prove the theorems by refuting our false conjectures and giving us explicit counterexamples for these statements. The collection of these proven theorems precisely specify the properties of our node, explicitly mentioning all the edge cases of its behaviour. Simultaneously, the code of the model can be compiled and executed as part of the ROS system.

We believe that such a mathematical formalization of robotic systems will result in more reliable and safe software that controls our robots. We want to encourage wider adoption of the formal verification techniques in the robotics community by developing tools and methods for formal verification of distributed systems like ROS.

The Part I of this series goes through the creation and execution of the model code. There is an Imandra notebook version of the two posts, that you can try live in the cloud. To learn more about our Imandra-ROS project, please visit our GitHub. To stay in touch with our updates, please sign up on our website.

--

--