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.
Twist message at
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
Twist message (i.e., in the next
state obtained as
one_step(s)). We can almost literally encode this formal expression as an Imandra
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
state produced by Imandra has the
incoming message set to
None and the
outgoing message set to a
Twist message with negative
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.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:
[@@apply] the two lemmas above to prove our final theorem with the
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.