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.