Since writ­ing my blog post ​“Let’s Write a Safe­ty Mon­i­tor for a Mars Rover!”, I’ve been giv­ing pre­sen­ta­tions and a webi­nar on SPARK and using my work to help illus­trate what it’s like writ­ing and prov­ing cor­rect­ness prop­er­ties with SPARK. This forced me to look again care­ful­ly at what I was prov­ing — there’s noth­ing like pre­sent­ing some code in front of an audi­ence to focus atten­tion on what you’re doing! I found I was increas­ing­ly unhap­py with this loop, in Autonomous_Mode.Run:

The loop invari­ant does prove, so we know that the Rover isn’t in an unsafe state at that point — but I didn’t like my fail­ure to assert the safe­ty prop­er­ty after Go_Forward (Rover.Cannot_Crash isn’t a post­con­di­tion of Go_Forward, here). I proved that, after find­ing a new direc­tion, the Rover would be in a safe state — but I didn’t prove that after going for­ward the Rover would be in a safe state.

I addressed this in the orig­i­nal blog post by mak­ing an infor­mal argu­ment about the vehi­cle dynam­ics and its impact on the cor­rect­ness of the code:

There are two con­di­tions under which we exit [the Go_Forward] loop: (1) if the user press­es a but­ton; and (2) if the dis­tance to an obsta­cle is less than 30 units (which is more con­ser­v­a­tive than our safe­ty thresh­old). Unfor­tu­nate­ly, nei­ther of these con­di­tions on its own is enough to say that we are safe. For (1), the Rover could be too close to an obsta­cle (and still be com­mand­ed to move straight for­ward). For (2), we know the upper bound on the dis­tance, but not the low­er bound — we’d have to know that the dis­tance is, e.g., greater than or equal to 20 but less than 30. Vehi­cle dynam­ics and the update rate of the sonar may guar­an­tee this, but we don’t have this infor­ma­tion avail­able sim­ply from the code.

Now, this is a valid approach to deal­ing with code that depends on real-world assump­tions that can­not be checked in soft­ware. But it felt unsat­is­fy­ing for this demo, which I want­ed to be more com­plete and more self-contained.

In this post, I’ll update the Rover demo to for­mal­ize the infor­mal argu­ment I made in the pri­or post. The result is a more sat­is­fy­ing autonomous mode that does a bet­ter job of guar­an­tee­ing that the Rover can­not crash. You can find the full Mars Rover demo — includ­ing the enhance­ments I describe here — at the Mars Rover demo’s home on github: https://​github​.com/​a​d​a​C​o​r​e​/​m​a​r​s​-​r​o​v​e​r​-demo.

Prov­ing Go_Forward #

Here’s the com­plete Go_Forward sub­pro­gram from before (with a cou­ple of the mag­ic num­bers replaced by constants):

We’d real­ly like to prove that the Rover is safe dur­ing the loop and when the sub­pro­gram returns. So we should add Rover.Cannot_Crash to the post­con­di­tion and as a loop invari­ant. We’ll put the loop invari­ant after the sec­ond exit state­ment, like this:

SPARK will prove the loop invari­ant: at that point in the loop, we are assured that Dis­tance is greater than 40, which is greater than our safe­ty thresh­old of 20. But SPARK can­not prove the post­con­di­tion: we have exit­ed when we fall below the dis­tance thresh­old of 40 but, as not­ed in the orig­i­nal blog post, we have no way of know­ing that we’re above the safe­ty thresh­old of 20. The Rover could be mov­ing fast enough that the dis­tance to the obsta­cle fell from, e.g., 41 to 19 in one loop iter­a­tion. We have to bring in addi­tion­al information.

Unfor­tu­nate­ly, the addi­tion­al infor­ma­tion we need doesn’t exist any­where in the soft­ware. Instead, this addi­tion­al infor­ma­tion is a phys­i­cal prop­er­ty of the sys­tem: the Rover just isn’t capa­ble of mov­ing fast enough on its own that it could close the dif­fer­ence between the dis­tance and safe­ty thresh­olds in 40 ms. The design of soft­ware depends on this fact, which we need to com­mu­ni­cate to SPARK.

One option is to use an assump­tion. An assump­tion — unlike an asser­tion — will not be proved by SPARK. SPARK will sim­ply use the assump­tion to help prove sub­se­quent checks. We can add the assump­tion like this:

But … this still doesn’t prove! Why not?

There are two exit state­ments in our loop. We’re con­fi­dent we’ve addressed the post­con­di­tion at the sec­ond exit state­ment, because of our new assump­tion. But we’ve not addressed the first exit state­ment. (We can ver­i­fy our think­ing by assert­ing Rover.Cannot_Crash just before the first exit state­ment; SPARK will fail to prove this assertion.)

To do this, we need to strength­en the pre­con­di­tion on Go_Forward. We have said that the Rover must be in a safe state, but Rover.Cannot_Crash is too weak to enable us to prove Rover.Cannot_Crash as our post­con­di­tion at the first exit, the first time around the loop. Why? Because Rover.Cannot_Crash is true if the sonar dis­tance is greater than the safe­ty thresh­old OR we are not mov­ing straight for­ward. So the pre­con­di­tion holds if, e.g., we are mov­ing back­wards and the sonar dis­tance is 5. But then the first thing Go_Forward does is start mov­ing for­ward. So if we took the first exit, we wouldn’t be safe any­more. (More­over, our assump­tion would def­i­nite­ly be invalid in this case!) So we should replace Rover.Cannot_Crash in our pre­con­di­tion with the stronger expres­sion Rover_HAL.Get_Sonar_Distance >= Rover.Safety_Distance¹.

Now SPARK can ful­ly prove Go_Forward, giv­en the assump­tion that we added.

Relax­ing the Assump­tion #

While this works, I don’t like it. As we just saw, assump­tions are a bit dan­ger­ous. Since SPARK can­not check them, it’s far too easy to assume some­thing that just isn’t valid. (It’s also some­times easy to assume some­thing that’s triv­ial­ly false — and this has dis­as­trous impli­ca­tions for the remain­der of the analy­sis, since in log­ic False → False is True.)

First, bald­ly assum­ing Distance >= Rover.Safety_Distance is far too strong. What if we made a mis­take in our def­i­n­i­tion of Sonar_Sampling_Delay and set it to 400 ms? or 4000 ms? Would the Rover still be safe? We have some notion of the Rover’s dynam­ics that led us to believe that our code was cor­rect; we could encode that, instead.

The Rover must have some max­i­mum speed that it can achieve. Let’s define Max_Speed to be 0.5 units per mil­lisec­ond². Then we can com­pute the max­i­mum dis­tance the Rover could trav­el in a giv­en num­ber of mil­lisec­onds and use this in our assump­tion, instead. So if we record the last dis­tance mea­sure­ment tak­en, we could say Distance >= Last_Distance - Sonar_Sampling_Delay * Max_Speed.

Tak­ing types into account, we can rewrite our assump­tion like this:

To do this, we need to cre­ate Last_Distance, which we’ll make Ghost (since we need it only for proof). We also need to set an ini­tial val­ue for Distance, since we’ll be read­ing it (to assign to Last_Distance) pri­or to polling the sonar. We’ll start by ini­tial­iz­ing Distance to Rover.Safety_Distance, because that’s in our precondition.

When we try to repeat the proof, it fails: SPARK can’t prove the post­con­di­tion. If we assert Rover.Cannot_Crash before the sec­ond exit state­ment, we see that this is the path along which SPARK is unable to prove the post­con­di­tion: the asser­tion can­not be proved, but SPARK does prove the post­con­di­tion under the assump­tion that the asser­tion holds. 

Intu­itive­ly, the fail­ure to prove the asser­tion tells us that Last_Distance is the prob­lem: SPARK is told that the dis­tance to the obsta­cle is greater than a func­tion of Last_Distance, but SPARK’s clear­ly not see­ing that this rela­tion­ship is as strong as we need. 

We can con­firm our intu­ition by strength­en­ing the asser­tion to Distance >= Rover.Safety_Distance, which SPARK can­not prove. We can fur­ther con­firm that the prob­lem is Last_Distance by adding an asser­tion about Last_Distance in front of our assumption. 

So we need to know that Last_Distance >= Distance_Threshold for our assump­tion to estab­lish that Distance >= Rover.Safety_Distance; if we assert this, SPARK can­not prove it. We need to make three changes to fix this.

First, because Last_Distance is assigned the val­ue of Distance that was con­strained in the pri­or iter­a­tion of the loop, we have to write the con­straint on Distance in a loop invari­ant. (Remem­ber that, in SPARK, loops rep­re­sent cut points in the analy­sis for any vari­ables assigned dur­ing the loop; only type prop­er­ties and prop­er­ties estab­lished in loop invari­ants are car­ried from one loop iter­a­tion to the next.) So we add Distance >= Distance_Threshold as a new loop invari­ant, next to Rover.Cannot_Crash. This ensures that SPARK will know that Last_Distance >= Safety_Threshold on sub­se­quent loop iterations.

But what about the first iter­a­tion? This leads us to the sec­ond and third changes. We need to strength­en our pre­con­di­tion from Rover_HAL.Get_Sonar_Distance >= Rover.Safety_Distance to Rover.Get_Sonar_Distance >= Distance_Threshold and we need to update the ini­tial­iza­tion of Distance to match. This will ensure that, on the first iter­a­tion, Last_Distance >= Safety_Threshold.

With these changes, when we rerun SPARK, the post­con­di­tion is proved.

We could stop here, but I per­son­al­ly still don’t like hav­ing this assump­tion in our code. It’s not ter­ri­bly obvi­ous that we’ve assumed some­thing that needs to be val­i­dat­ed. And, if we want­ed to lever­age this mod­el of our dynam­ics else­where, we’d have to repeat ourselves.

For­tu­nate­ly, SPARK gives us tools to mod­u­lar­ize these kinds of assumptions.

Mod­u­lar­iz­ing the Assump­tion #

We mod­u­lar­ize the assump­tion in the same way that we might intro­duce a lem­ma or describe the con­tract on a bind­ing to anoth­er lan­guage: we declare a pro­ce­dure whose post­con­di­tion is the assump­tion and mark it Ghost and Import. 

Since SPARK’s analy­sis is mod­u­lar, when we call this pro­ce­dure, SPARK will assume the post­con­di­tion when­ev­er the pre­con­di­tion (which is emp­ty, here) is met. We can now replace the assump­tion in Go_Forward with a ​“call” of this Ghost pro­ce­dure³.

Here’s the final form of Go_Forward that incor­po­rates all of the changes and is ful­ly proved:

Back to Run #

Now that we’ve changed the con­tract for Go_Forward, we need to look again at the loop in Run — because it’s quite clear that it won’t prove in its cur­rent state:

This loop doesn’t meet the pre­con­di­tion on Go_Forward. In the first iter­a­tion, we know only Rover.Cannot_Crash from the pre­con­di­tion on Run — which is weak­er than Rover_HAL.Get_Sonar_Distance >= Distance_Threshold. And in sub­se­quent iter­a­tions, we still know only Rover.Cannot_Crash because that’s all the loop invari­ant establishes.

No mat­ter what else we do, we need to strength­en the post­con­di­tion on Find_New_Direction to Rover_HAL.Get_Sonar_Distance >= Distance_Threshold. And since Find_New_Direction cur­rent­ly has no pre­con­di­tion (oth­er than Initialized), we might as well put it first in the loop:

This way, we could actu­al­ly drop the pre­con­di­tion on Run alto­geth­er, allow­ing the Rover to start arbi­trar­i­ly close to an obsta­cle and still avoid crashing.

Let’s see what it will take to get Find_New_Direction to promise Rover_HAL.Get_Sonar_Distance >= Distance_Threshold.

Improv­ing Find_New_Direction #

Here’s the cur­rent imple­men­ta­tion of Find_New_Direction:

The log­ic here is that we look to the left and the right and mea­sure the dis­tance to obsta­cles in both direc­tions and then reori­ent the vehi­cle based on those mea­sure­ments. If both left and right are too close (clos­er than 50 units), we turn around. Oth­er­wise, we turn towards whichev­er direc­tion has an obsta­cle fur­ther away.

This is intu­itive — but doesn’t guar­an­tee that we’ll end up point­ed in a direc­tion with an obsta­cle more than 40 units — our dis­tance thresh­old and the pre­con­di­tion for Go_Forward — away. For exam­ple, what if we don’t turn far enough to the left or the right? The delay was cho­sen based on Rover dynam­ics — but we have no guar­an­tee (in soft­ware!) that we’ll end up point­ed in a direc­tion with an obsta­cle more than 40 units away. What if motor pow­er drops dur­ing the turn and we don’t turn as far as expect­ed? Worse, what if the Rover finds itself inside of a (small) box with no exits? The cur­rent code would turn around and start mov­ing for­ward with­out con­firm­ing that the way out is clear!

Now, these are cor­ner cas­es that we might argue are impos­si­ble. But safe­ty is about iden­ti­fy­ing cor­ner cas­es and either remov­ing them or argu­ing through risk assess­ment that we’re pre­pared to accept the con­se­quences if the cor­ner case occurs (e.g., the Rover dri­ves into a canyon on Mars and is blocked in by a rock fall).

Before we strength­en the post­con­di­tion to Rover_HAL.Get_Sonar_Distance >= Distance_Threshold and update this sub­pro­gram to meet it, we might pause and ask: ​“how is the cur­rent post­con­di­tion proved?” giv­en the prob­lems we note above. The answer is, again, our safe­ty prop­er­ty is (much) weak­er than the new post­con­di­tion we want to prove. Here, it’s met entire­ly because Find_New_Direction always leaves the Rover in a state in which it is not mov­ing straight for­ward. And that’s enough to sat­is­fy our safe­ty prop­er­ty, so the cur­rent post­con­di­tion proves. But it’s not enough to sat­is­fy the pre­con­di­tion of our now-proved-safe Go_Forward.

For­tu­nate­ly, fix­ing Find_New_Direction isn’t dif­fi­cult. Here’s the updat­ed, ful­ly proved implementation:

We’ve sim­ply wrapped the cur­rent func­tion­al­i­ty in a while loop that con­tin­ues search­ing for a new direc­tion until the dis­tance is greater than or equal to the dis­tance thresh­old of 40 units. We’ve intro­duced a new, local func­tion that mea­sures the dis­tance straight ahead because we need this func­tion­al­i­ty twice — so encap­su­la­tion helps us keep the imple­men­ta­tion DRY (Don’t Repeat Yourself).

Note that we didn’t need to write a sin­gle loop invari­ant or asser­tion. SPARK proves that our new post­con­di­tion holds with only the updat­ed implementation.

Finalizing Run

There’s one more change we need to make to Run. Since Find_New_Direction promis­es This.User_Exit or Rover_HAL.Get_Sonar_Distance >= Distance_Threshold, we need to check for user exit pri­or to mov­ing forward:

And that’s it. We now fully prove the safety property throughout autonomous mode, including while the Rover is driving forward in Go_Forward.

[1] In safety-critical systems, it is common for a safety property (or a safety invariant) that is proved to hold now to be insufficient (too weak) to guarantee that it will hold later, e.g., during the next iteration of a loop. What’s required in this case is a stronger property - often referred to as an inductive invariant - that is strong enough to guarantee that the safety property will hold in a future state. (And, indeed, we typically need to know that the inductive invariant will guarantee that it holds in a future state, so that we can keep running safely.) As we will see in the next section, the inductive invariant that we need here is that the distance to an obstacle is greater than or equal to 40 units - a much stronger property than the 20-unit safety threshold that’s part of our safety property!

[2] It’s actually been measured to be 0.012 units per millisecond - in the final code, we set Max_Speed to 0.015 for a bit of additional margin: we don’t need to squeeze all the performance possible out of the system.

[3] There are at least two implicit assumptions underpinning the correctness of invoking our dynamic model, here: (1) that the sonar measurements overlap the axis of motion (i.e., detect obstacles straight forward) and (2) that the elapsed time since the last measurement is no greater than the sonar sampling delay. We could encode these as preconditions and prove they hold at the point of call - but to do so, we’d have to modify our HAL to report the direction and time of the sonar measurement so we can retrieve these via (models of) getters. For the moment, we’ll leave this enhancement as an exercise for the reader.