The bigger picture of verifying autonomous robots

Posted on by Yoav Hollander

Summary: This post talks about the “bigger picture” of autonomous robot verification (beyond basic CDV stuff). It mainly discusses the challenges, not the solutions.

I am in the process of creating a minimal CDV-based verification framework for autonomous robots. This framework will simply do the usual CDV stuff (constraint-based generation, checking, coverage etc.) with minimal extra modeling.

So I am starting to think of what’s next, i.e. what is the “bigger picture” of verifying an autonomous robot (and what kind of modeling this implies). Here are some initial thoughts.

The autonomous robotics field (including, say, autonomous cars and UAVS) is advancing fairly rapidly (see e.g. here). The example I’ll use is an autonomous assistive robot, i.e. a robot which will help a disabled / elderly user in daily life.

For instance, it will help the user climb up the stairs, fix furniture (together), perform home medical procedures, go to a concert (while travelling via a bus) and so on. In general, the user is in charge, and tells the robot what to do (via speech recognition, visual gestures etc.). However, the robot is also autonomous, and can take control during some moments.


Here are two scenarios demonstrating aspects of this mixed-initiative behavior:

  1. The user says “take me to the Grand concert hall via a bus”. The robot gathers information, helps the user go downstairs, helps the user cross the street and climbs into the bus with him. However, if while crossing the street it notices a truck lumbering down on them, it should unceremoniously push the user across the street very quickly, much like a human guardian would.
  2. The user says “take me to the Grand concert hall via a bus”. The robot checks,finds that previous concerts have exerted a big stress on the user’s heart, and suggests avoiding concerts for that reason. However, the user decides to go anyway, and they proceed to the concert – in general (and unlike the special case in the previous example) the user makes the final decision.

I think such assistive robots may actually be deployed in 3 to 10 years (with perhaps growing degrees of intelligence). They certainly don’t need “general AI”, but they are still fairly intelligent – let’s call them ARAI, for Autonomous Robot AI. They’ll need a fair amount of verification. I expect verification (and its automation) to receive quite a bit of attention, because of regulatory requirements, and because one would need to fully re-verify each new release of the HW and SW.

Below I’ll discuss how the challenges of ARAI verification, and a bit about how they can be verified (with an emphasis on dynamic verification).

ARAI verification challenges

Here are some of the big ARAI verification challenges. Note that many of these (especially the first few below) are actually spec’ing challenges (which then manifest themselves also as verification challenges):

  • Modeling and checking decisions between two good (or two bad) possible outcomes
    • E.g. should it save the user or 20 schoolchildren? And whose definition of “better” should be used?
  • Modeling and checking those mixed-initiative situations
    • Like the two examples above
  • Modeling and checking behavior in the face of uncertainty
    • The job of the DUT is to optimize things statistically, but a particular decision may end up with a bad outcome due to chance – this is not necessarily an error on the part of the DUT
    • Also, we need to take into account limited computation time (“bounded rationality”) for the AI: It may not be able to always find the best answer – just a pretty good answer.
  • Modeling all these objects
    • people, vehicles, city situations, failures, …
    • This includes modeling uncertainty/non-determinism, including modeling “logical uncertainty” (i.e. uncertainty about the actual mechanisms to be used)
  • Generating all those interesting usage scenarios and their variants
    • We should certainly test the help_user_go_to_some_venue generic scenario, the help_user_fix_furniture scenario and so on, each with its myriad permutations – the space is really infinite
  • Considering completely-new / unexpected events?
    • Especially when “just stop and do nothing” is not an option, e.g. during high-speed traffic
  • Avoiding spec bugs
    • Specs bugs are more dangerous than implementation bugs – see here
  • Building a verification framework which will work in different execution modes
    • Obviously, most verification will be done with the simulated version, but some should run using Hardware-In-the-Loop and a small subset even with User-In-the-Loop
  • Doing this verification in a modular, incremental, repeatable way
    • I.e. removing incidental complexity from the verification job
So how will ARAI verification be done?

How will these systems realistically be verified, using techniques available in (say) the next 5 years?

This is not completely clear – the field is still fairly immature. There is some work on formal verification of some aspects of autonomous robots (e.g. here), and some initial work on dynamic, coverage-driven verification (e.g. here).

My current intuition is that ARAI verification is best done with dynamic verification / CDV as the main vehicle, though formal techniques can help. I have summed up some of my ideas at the end of this post.

Leave a Reply