Demonstrating SPARK with a Mars Rover (Part 2): The Safety Property What you’ll learn: - How Ada contracts make programs provable. - How contracts can be used to make code safer. - How contracts make code more maintainable. This is part two of a four-part series highlighting the Ada SPARK programming language that’s designed to facilitate the creation of safety- and security-critical systems. It implements the software for the Ada Mars Rover demo platform. In this part, we take a slower look at the safety aspects of the system. The code employs Ada contracts that allow the application to be provably correct at compile time via static analysis. Demonstrating SPARK with a Mars Rover: 4-Part Series - Cyber-Physical Systems - The Safety Property - Improving the System - Formalizing Safety One of the goals for this Mars Rover Demo project was to demonstrate how SPARK can address safety and reliability issues. You can download the sources for the Mars Rover Demo project. function Cannot_Crash return Boolean is (if Rover_HAL.Get_Sonar_Distance < Safety_Distance and then Rover_HAL.Get_Turn = Rover_HAL.Straight then Rover_HAL.Get_Power (Rover_HAL.Left) <= 0 and then Rover_HAL.Get_Power (Rover_HAL.Right) <= 0); The safety distance is set to 20: Safety_Distance : constant Interfaces.Unsigned_32 := 20; This matches the design of the remote-control mode. Proving Controller Safety The monitor is then attached to the controllers, which is done top-down. Contracts are often added to SPARK code bottom-up for proof. However, in this case, it’s easier to think about what’s going on and decide where contracts are needed using a top-down approach, starting with “Rover.Tasks.Demo”. Although not strictly necessary (since the demo loop never terminates), a postcondition can be added in the “rover-tasks.ads” file like this: procedure Demo with Pre => Rover_HAL.Initialized, Post => Rover_HAL.Initialized and then Rover.Cannot_Crash; Such an approach ensures that, if the behavior of “Demo” changes and it’s reused in another context, it will leave the Rover in a safe state. Looking at the body reveals a single loop that executes the autonomous-control mode followed by the remote-control mode, forever. The team added the Loop Invariant like this: loop Rover.Autonomous.Run; Rover.Remote_Controlled.Run; pragma Loop_Invariant (Rover.Cannot_Crash); end loop; Of course, this doesn’t prove yet: First, the team needs to add “Rover.Cannot_Crash” as a postcondition of “Rover.Remote_Controlled.Run”, first. Since this property is intended to be invariant, it’s also made a postcondition of “Rover.Autonomous.Run”. Let’s start with the autonomous-control mode, as it’s actually simpler to prove than the remote-control mode! Autonomous-Control Mode The postcondition to ”rover-autonomous.ads” is added like this: procedure Run with Pre => Rover_HAL.Initialized, Post => Rover_HAL.Initialized and then Rover.Cannot_Crash; A precondition asserts the safety property is unnecessary because the first thing “Run” does is stop everything: -- Stop everything Set_Turn (Straight); Set_Power (Left, 0); Set_Power (Right, 0); Then a Loop Invariant to the body of “Run” is added: while not State.User_Exit loop Go_Forward (State); Find_New_Direction (State); pragma Loop_Invariant (Rover.Cannot_Crash); end loop; Again, this won’t prove without a necessary postcondition to “Find_New_Direction”. Since “Find_New_Direction” is local to the body, it can be added like this: procedure Find_New_Direction (This : in out Auto_State) with Pre => Initialized, Post => Initialized and then Rover.Cannot_Crash SPARK proves that the postcondition is guaranteed by the body of “Find_New_Direction” without any additional proof annotations at proof Level 1. And SPARK proves the loop in “Run” and the postcondition for “Run” at this point. Before moving on, however, it should be considered that, since the safety property is meant to be invariant (never violated), the behavior of `Go_Forward` warrants investigation. `Go_Forward` starts by unconditionally commanding the robot to move forward and then enters a loop looking for obstacles. Given this initial motion, forward movement must not occur unless the safety property holds. We’ll make this a precondition of “Go_Forward”. procedure Go_Forward (This : in out Auto_State) with Pre => Initialized and then Rover.Cannot_Crash, Post => Initialized Why isn't the safety property a postcondition? Let’s look at the loop in “Go_Forward”: loop Check_User_Input (This); exit when This.User_Exit; Next_Mast_Pos (This, -55, 55, Milliseconds (10)); Distance := Sonar_Distance; exit when Distance < 30; Delay_Milliseconds (10); end loop; There are two conditions under which Go_Forward exits this loop: (1) if the user presses a button, and (2) if the distance to an obstacle is less than 30 (which is more conservative than the safety threshold). Unfortunately, neither of these conditions on its own is enough to say that it’s safe. For (1), the Rover could be too close to an obstacle (and still be commanded to move straight forward). For (2), the upper bound on the distance is known, but not the lower bound. We’d have to know that the distance is, e.g., greater than or equal to 20 but less than 30. Vehicle dynamics and the update rate of the sonar may guarantee this, but the information isn't available simply from the code. Thus, if the team tried to prove the safety property as a Loop Invariant and then as a postcondition, they would not succeed. [Footnote: This is part of the reason the team doesn’t use a “Type_Invariant” for the safety property. Since a “Type_Invariant” is asserted at subprogram boundaries, it’s both too restrictive (sometimes the software needs to temporarily break the invariant, as seen here) and not restrictive enough ( the invariant must be asserted in critical “Run” loops). Furthermore, a “Type_Invariant” must be attached to a type (as the name suggests). The invariant is asserted over instances of the type at the boundaries of subprograms. For the Mars Rover, the software doesn’t have such an instance that’s passed around — the state is global (and internal to the “Rover_HAL” package). The team would have had to do significant refactoring to use a “Type_Invariant”.] Arguably, it’s okay that the safety property isn’t established as an invariant or postcondition here. It’s inferred that it’s safe because of the second exit condition, and “Find_New_Direction” doesn’t assume the safety property to do its job. With the contracts on “Go_Forward” and “Find_New_Direction” in place, SPARK proves everything in “Rover.Autonomous”. Note: On the way out, the autonomous-control mode stops everything: -- Stop everything before leaving the autonomous mode Set_Turn (Straight); Set_Power (Left, 0); Set_Power (Right, 0); procedure Run with Pre => Rover_HAL.Initialized and then Rover.Cannot_Crash, Post => Rover_HAL.Initialized and then Rover.Cannot_Crash; The precondition gives some confidence that the Rover isn’t already in trouble (although, as can be seen, it’s not as strong as desired, given how the remote-control mode was originally written!). As above, the safety property in a Loop Invariant is added at the bottom of the loop in the body of “Run”. [...] Delay_Milliseconds (30); pragma Loop_Invariant (Rover.Cannot_Crash); end loop; end Run; And … SPARK can’t prove this — at any proof Level: rover-remote_controlled.adb:144:33: medium: loop invariant might fail in first iteration, cannot prove Rover_HAL.Get_Power (Rover_HAL.Left) <= 0 144 | pragma Loop_Invariant (Rover.Cannot_Crash); | ^~~~~~~~~~~~~~~~~~ in inlined expression function body at rover.ads:27 rover-remote_controlled.adb:144:33: medium: loop invariant might not be preserved by an arbitrary iteration, cannot prove Rover_HAL.Get_Power (Rover_HAL.Left) <= 0 144 | pragma Loop_Invariant (Rover.Cannot_Crash); | ^~~~~~~~~~~~~~~~~~ in inlined expression function body at rover.ads:27 When proof failures like this show up, a good approach is to talk through why you believe the property should hold. Let’s look at the loop again: [...] Dist := Sonar_Distance; if (for some B of Buttons => B) then Last_Interaction_Time := Clock; end if; if Dist < Rover.Safety_Distance then -- Ignore forward commands when close to an obstacle Buttons (Up) := False; end if; Cmd := To_Command (Buttons); Set_Display_Info ("Remote: " & Img (Cmd)); if Cmd /= Last_Cmd then case Cmd is when None => Set_Power (Left, 0); Set_Power (Right, 0); when Forward => Set_Turn (Straight); Set_Power (Left, 100); Set_Power (Right, 100); [...] The distance is read, compared with the safety threshold, and the Up button is released if the Rover is too close to an obstacle. The buttons are then converted into a command, and the turn and motor power are set accordingly. Releasing the Up button should prevent forward motion. This information is contained in the function “To_Command”. But SPARK’s analysis is modular: It only knows about the current subprogram (and its nested subprograms, if any) and expression functions. On inspection of “To_Command”, it’s neither a nested function nor an expression function. And because it has no contract, SPARK has no idea what it’s doing and assumes that the result could be any valid value of the “Remote_Command” type. In essence, critical information is hidden from SPARK! To remedy that, let’s turn this into an inline expression function so that SPARK can see what’s happening: function To_Command (Buttons : Buttons_State) return Remote_Command is (if Buttons (Up) and then Buttons (Left) then Forward_Left elsif Buttons (Up) and then Buttons (Right) then Forward_Right elsif Buttons (Down) and then Buttons (Left) then Back_Left elsif Buttons (Down) and then Buttons (Right) then Back_Right elsif Buttons (Up) then Forward elsif Buttons (Right) then Turn_Right elsif Buttons (Left) then Turn_Left elsif Buttons (Down) then Backward else None) with Annotate => (GNATprove, Inline_for_Proof); At this stage, it might be expected that SPARK has sufficient information to prove the property. However, when the analysis is run again, SPARK still reports that the loop invariant may not hold. The structure of the loop is fairly straightforward: All of the information SPARK needs appears to be there — provided that the new command “Cmd” isn’t equal to the old command “Last_Cmd”. If the two commands are the same, though, the Rover continues to operate based on the turn and motor power levels previously set. In general, SPARK forgets everything that happened in the previous loop iteration when considering the current loop iteration. Only information that’s asserted via Loop Invariants is carried forward into the next iteration. So, SPARK essentially doesn’t know what our getters will return, unless “Cmd /= Last_Cmd”. What should be communicated to SPARK? Looking at the case statement and recalling our safety property, the following should be remembered: -- Carry the information about the relationship between Cmd and the -- turn and power settings around the loop, since when Cmd = Last_Cmd -- these values are retained. pragma Loop_Invariant (if Cmd /= Forward then Get_Turn /= Straight or (Get_Power (Left) <= 0 and Get_Power (Right) <= 0)); The intuition is that because the system doesn’t move forward when the safety threshold is violated, it’s only necessary to make sure that, when the safety threshold is violated, it's not going straight with positive motor values. Turning is acceptable, as is proceeding straight in reverse. With this Loop Invariant, SPARK proves the safety property. Therefore, this Loop Invariant is indeed useful. Unfortunately, it doesn’t prove: SPARK says it may fail in the first iteration (but SPARK does prove that it holds in subsequent iterations, which leads to the belief that it’s probably the right Loop Invariant). Why not? A useful approach to debugging a proof like this is to consider the relationship between the invariant and the structure of the code. Here, as said above, there are two cases of interest: “Cmd = Last_Cmd” and “Cmd /= Last_Cmd”. The Loop Invariant can be split, expressing these two cases as such: pragma Loop_Invariant (if Cmd = Last_Cmd and Cmd /= Forward then Get_Turn /= Straight or (Get_Power (Left) <= 0 and Get_Power (Right) <= 0)); pragma Loop_Invariant (if Cmd /= Last_Cmd and Cmd /= Forward then Get_Turn /= Straight or (Get_Power (Left) <= 0 and Get_Power (Right) <= 0)); Now, SPARK says that the first Loop Invariant, where “Cmd = Last_Cmd”, fails on the first iteration. Therefore, the if statement containing the case statement with the Rover commands can be ignored in our debugging. Let’s talk through how the “Run” procedure works again, with this knowledge in mind, and focus on the first iteration of the loop. The “Run” procedure initializes “Cmd” to “None”. When the loop starts, the buttons on the remote control are polled. Then the value of “Cmd” is copied to “Last_Cmd”, so now “Cmd” and “Last_Cmd” are both “None”. The safety threshold is then checked. If the Rover is too close to an obstacle, the Up button is released. The buttons are then converted to a command, which is assigned to “Cmd”. It’s possible that none of the buttons are pressed, either because the user isn’t pressing a button or because the user was pressing the Up button, but the Rover was too close to an obstacle. So, it’s possible that “Cmd” will (again) be assigned “None”. Thus, it’s possible that “Cmd = Last_Cmd”. And in that case, the Rover will continue doing whatever it was doing before. From the information available in this procedure, there’s no reason to assume that the Rover wasn’t previously driving straight forward. And even though the safety threshold was checked, because “Cmd = Last_Cmd”, it’s not going to change the Rover’s turn or motor powers. Therefore, the safety property could indeed be violated in the first iteration. SPARK is correct. Has a bug been found that could have resulted in the Rover crashing? No, when it comes to the current Rover demo. Recall that, on the way out of autonomous-control mode, everything is stopped, as noted above. This guarantees that when “Cmd = Last_Cmd” in the first iteration, the Rover will (continue to) be stopped, and the safety property isn’t violated. But SPARK doesn’t know this. And the importance of stopping the Rover when handing off to the remote-control mode isn’t documented anywhere. Therefore, if this module were reused in a different context, this unwritten assumption could be violated, leading to the possibility of an accident. And that sounds far-fetched, there are high-profile examples of exactly this happening in safety-critical systems. So, let’s fix it. Fixing the Remote-Control Mode The remote-control mode problem can be fixed in a couple of different ways. A precondition could be introduced that requires the Rover to be stopped — or in some similarly safe state — before the remote-control mode is called. This could be implemented using the available getters, for example: procedure Run with Pre => Rover_HAL.Initialized and then Rover.Cannot_Crash and then Rover_HAL.Get_Power (Rover_HAL.Left) = 0 and then Rover_HAL.Get_Power (Rover_HAL.Right) = 0, Post => Rover_HAL.Initialized and then Rover.Cannot_Crash; With this change, SPARK fully proves “Rover.Remote_Controlled” at Level 1. (To fully discharge the proof for the demo, these constraints would need to be added to the postcondition of “Rover.Autonomous.Run”). It does seem a pity that the Rover has to be stopped to activate the remote-control mode, though. An enhanced version of the demo could allow a user to take control seamlessly by pressing the remote-control button that corresponds to the Rover’s current motion. A new “Rover_Command” that represents the initial, invalid state of “Last_Cmd”, to better handle the first loop iteration, is introduced. The new command is added like this: type Remote_Command is (Invalid, None, Forward, Backward, Turn_Left, Turn_Right, Forward_Left, Forward_Right, Back_Left, Back_Right); The case statement is then updated to account for the new command by removing the case for “None” and adding a “when others” at the bottom: when others => Set_Power (Left, 0); Set_Power (Right, 0); end case; These changes ensure that, in the first iteration, “Cmd /= Last_Cmd”, because “To_Command” can never generate this “Invalid” command. As a result, greater flexibility is enabled in how the remote-control mode can be activated while still preserving the safety property. With this change, SPARK fully proves the demo at Level 1. It’s been demonstrated how to formalize a safety requirement for a simple Mars rover and use it to prove that the controller never issues a command that would cause a collision. They implement the formalism with ghost state and uninterpreted functions that model getters, without altering the executable semantics of the rover HAL. After attaching the model to the code, they uncover an unstated assumption in the remote-control mode that could have permitted a crash if that mode were reused as a component in a new system. In turn, they correct the remote-control mode to ensure safety regardless of how it’s invoked. Finally, they show that SPARK proves the model at Level 1 with minimal reliance on intermediate assertions. >>Check out Part 1 of this series About the Author Tony Aiello Product Manager, AdaCore Tony Aiello is a Product Manager at AdaCore. Currently, he manages SPARK Pro and GNAT Pro for Rust, with a hand in UX and application of AI to AdaCore’s products. Tony has been principal investigator of multiple United States Air Force research projects that focus on the enhancement and application of formal methods to Air Force-relevant applications. Previously, Tony led the SSI and QGen teams, led research directions, and was Head of Product at AdaCore. Before joining AdaCore, Tony was a Principal Scientist at, and briefly President of, Dependable Computing, a small research and development group focused on safety and formal methods. Voice Your Opinion! To join the conversation, and become an exclusive member of Electronic Design, create an account today! Leaders relevant to this article: