Autonomous Vehicle Controller

Verification of the Boyer-Green-Moore car controller — proving that a vehicle under arbitrary wind conditions always remains in a safe state.

Overview

This case study formalizes and verifies a classic problem from the Boyer-Green-Moore tradition: a vehicle controller that must maintain a safe position despite unpredictable wind disturbances. The controller uses a simple feedback law based on the sign of the vehicle's position and velocity, and the proof establishes that the system always remains within a bounded safe region.

This is a foundational example of invariant-based safety verification for cyber-physical systems.

The Model

State Space

type state = {
  w : int;  (* current wind speed *)
  y : int;  (* y-position of the vehicle *)
  v : int;  (* accumulated velocity *)
}

Controller

The controller computes a thrust adjustment based on the sign of the current and previous positions:

let controller sgn_y sgn_old_y =
  (-3 * sgn_y) + (2 * sgn_old_y)
 
let sgn x =
  if x < 0 then -1
  else if x = 0 then 0
  else 1

State Transition

At each step, wind changes by at most ±1, position updates based on velocity and wind, and velocity updates based on the controller's output:

let next_state dw s =
  { w = s.w + dw;
    y = s.y + s.v + s.w + dw;
    v = s.v +
        controller
          (sgn (s.y + s.v + s.w + dw))
          (sgn s.y) }
 
let arbitrary_delta_ws = List.for_all (fun x -> x = -1 || x = 0 || x = 1)
 
let rec final_state s dws =
  match dws with
  | [] -> s
  | dw :: dws' ->
    let s' = next_state dw s in
    final_state s' dws'
[@@adm dws]

Safe State Invariant

The good_state predicate enumerates all 13 safe (position, velocity+wind) pairs:

let good_state s =
  match s.y, s.w + s.v with
  | -3, 1 -> true  | -2, 1 -> true  | -2, 2 -> true
  | -1, 2 -> true  | -1, 3 -> true  | 0, -1 -> true
  | 0, 0  -> true  | 0, 1  -> true  | 1, -2 -> true
  | 1, -3 -> true  | 2, -1 -> true  | 2, -2 -> true
  | 3, -1 -> true  | _ -> false

Understanding the Invariant

The 13 safe states form a bounded region in the (y, w+v) plane where the controller can always recover. Each state represents a position and combined velocity:

• States near y=0 have small velocities -- the vehicle is centered and stable. For example, (0, 0) is the equilibrium, while (0, -1) and (0, 1) represent gentle drifting that the controller can easily correct.
• States at |y|=3 (maximum displacement) always have velocity pointing back toward center. At y=3, the combined velocity w+v is -1, meaning the vehicle is already returning. At y=-3, the combined velocity is +1. The controller has just enough authority at these extremes.
• Intermediate states show the controller building momentum to return. At y=-2, velocities of +1 and +2 are safe because they carry the vehicle back toward center. At y=2, velocities of -1 and -2 serve the same purpose.
• The asymmetry in the state counts (e.g., two safe velocities at y=-2 but also two at y=2) reflects the symmetric nature of the controller's feedback law, which uses sgn of position and previous position.

The key insight: this invariant was not designed by hand. It was discovered by forward-chaining from the initial states (0, 0) with all possible wind sequences, then verified to be inductive by ImandraX. The 13 states are precisely the reachable set -- no more, no fewer.

Verification

Step 1: Single-Step Safety

First, prove that one step from a good state with bounded wind always produces another good state:

theorem safety_1 s dw =
  good_state s && (dw = -1 || dw = 0 || dw = 1)
  ==> good_state (next_state dw s)
[@@rw]

ImandraX proves this by case-splitting over all 13 good states and all 3 wind values (39 cases total).

Step 2: Multi-Step Safety

By induction over arbitrary sequences of wind disturbances:

lemma all_good s dws =
  good_state s && arbitrary_delta_ws dws
  ==> good_state (final_state s dws)
[@@by induction ~id:[%id final_state] () @>>| auto]
[@@disable next_state, good_state]

This proves that for any finite sequence of bounded wind disturbances, starting from a good state, the vehicle remains in a good state forever.

The @@disable annotations prevent ImandraX from expanding the step function and invariant during induction — they've already been proved correct in safety_1, so the inductive step only needs to invoke that rewrite rule.

Results

The proof establishes a perpetual safety guarantee:

• The vehicle's position y always remains in [-3, 3]
• The combined velocity and wind w + v is always bounded
• The controller always has enough authority to counteract any bounded wind sequence

This is achieved despite the controller having no knowledge of future wind — it reacts purely to the current and previous position signs.

References

• Source: car.iml
• Boyer, R.S. and Moore, J S. — original car controller problem