Looking for feedback on formally verified quadcopter software

[Daniel Ricketts]

For the past year or so, I've been working on the VeriDrone research project at UC San Diego, in which we formally verify quadcopter safety software. Our goal is to build a software module to load on an off the shelf quadcopter in order to enforce safety constraints on the vehicle, like preventing it from flying too high, over an airport, etc. I know that some existing quadcopters have similar software, but our novel contribution is that it's formally verified, giving you extremely strong guarantees that the software does what it should. Here's a short video giving a brief introduction to the project: Short introduction to the VeriDrone project.

I'm posting this here because I'm hoping to get some feedback from pilots on the merits of such a system. Would pilots like this? Would people use it? Would it make anyone feel safer?

 

[User Name]

I'm torn on things like this. On the one hand, I think they could be invaluable for novice pilots and/or the totally oblivious person who just buys a multirotor on a whim and promptly looses it.

On the other hand, I fear something like this becoming mandatory on all quads, because the restrictions can be overwhelmingly negative. I recently discovered a small private airport outside my town, and calculated that a 5 mile radius covers 100% of a local nature preserve where I've done the majority of my flying, filming it's many landscapes and features. I did some research and ran a few numbers and found that a 5 mile radius around every airport in the US covers roughly 40% of the entire land mass of the country. I fear it's very easy to see geofencing as a good idea, not realizing the devastating effect it could have on the industry.

Regarding the height restrictions, even that can be less than cut and dry. One of the main features in the local nature preserve is a vertical ridge line that can be up to 250 feet high in places. There's a perfect launching spot at the base, and while the FAA's restrictions call for a 400 AGL limit, what happens when you start your flight from a significantly lower elevation than you intend to fly over? If I want to drop down from 400 feet over the ridge line, that could put me at 650 feet above my launch site - but still within the FAA's rules of 400 feet AGL. Would your system be smart and/or flexible enough to account for this?

I, as most, purchased this expensive camera platform specifically for filming. I certainly don't want to endanger anyone with it and I always fly it as responsibly as possible, but I fear systems like this will utterly cripple my ability to film anything worthwhile. Sport/scale RC model fields, school yards and the occasional patch of indescript forest make for lousy filming subjects, and totally negates the value of the vehicle.

As an optional system, I'm all for it, but I would really oppose it's forced, blanket implementation. I get that we need to ensure the safety of general aviation, but these things have opened up access to the sky to a far greater number than general aviation ever did or will. There has to be a cooperative solution - the sky shouldn't be reserved only for those who can drop several 10's of thousands of dollars on training and an airplane.

 

[Maddog]

OMG- you're trying to curb reckless, stupid behavior with software now! Society will always be filled with stupid irresponsible people- you can't legislate them out of existence (gun control) and you can't exterminate them (the Nazi's).

So you are figuring out a way to profit off the impending Federal rules governing drone use by supplying "formally verified" nany software.

What does "formally verified" mean? Who verified it and why should we believe or trust said "verifiers"?

No, I don't like it. No I wouldn't use it- if it becomes mandated by the gov't, somebody will figure out a way to disable it.

No, it wouldn't make me feel safer but I think a lot of liberal, gov't loving leftists would. You know, the same people who believe the TSA makes air travel safer despite the fact they failed to detect simulated weapons & bombs 95% of the time.

This smells like a left-wing "feel good" project that makes people feel safer but accomplishes nothing. Kinda like believing "expanded background checks" for gun purchases will stop mass shootings.

 

[Daniel Ricketts]

I'm torn on things like this. On the one hand, I think they could be invaluable for novice pilots and/or the totally oblivious person who just buys a multirotor on a whim and promptly looses it.

On the other hand, I fear something like this becoming mandatory on all quads, because the restrictions can be overwhelmingly negative.

I share your concerns. When I first started learning to fly a quadcopter, I would have wanted some sort of geo-fencing system. It would have made me feel a bit more comfortable to have such a safety net. However, I definitely believe that for expert pilots such as yourself, this safety net could be extremely restrictive without providing much of a benefit.

Perhaps one solution is to have a dynamic geofence that adjusts to the presence of other aircraft. For example, a plane is taking off from some runway, so the geofence prevents small UAVs from flying in near the flight path of that airplane. Of course, this would require communication between air vehicles, and current technology (our system included) comes nowhere near supporting it. Nevertheless, it could be a solution at some point in the future.

However, at the moment, I too would prefer our system to be used optionally by novices hoping to safely learn how to fly. Perhaps drone companies could have something like this pre-loaded on their products, with a mechanism for disabling it.

Regarding the height restrictions, even that can be less than cut and dry. One of the main features in the local nature preserve is a vertical ridge line that can be up to 250 feet high in places. There's a perfect launching spot at the base, and while the FAA's restrictions call for a 400 AGL limit, what happens when you start your flight from a significantly lower elevation than you intend to fly over? If I want to drop down from 400 feet over the ridge line, that could put me at 650 feet above my launch site - but still within the FAA's rules of 400 feet AGL. Would your system be smart and/or flexible enough to account for this?

Our system will soon be able to enforce arbitrary 3-dimensional safe regions, so it would be able to account for this scenario. Of course, you would need data on where these ridges are. We don't attempt to solve that problem.

 

[Daniel Ricketts]

OMG- you're trying to curb reckless, stupid behavior with software now! Society will always be filled with stupid irresponsible people- you can't legislate them out of existence (gun control) and you can't exterminate them (the Nazi's).

So you are figuring out a way to profit off the impending Federal rules governing drone use by supplying "formally verified" nany software.

What does "formally verified" mean? Who verified it and why should we believe or trust said "verifiers"?

No, I don't like it. No I wouldn't use it- if it becomes mandated by the gov't, somebody will figure out a way to disable it.

No, it wouldn't make me feel safer but I think a lot of liberal, gov't loving leftists would. You know, the same people who believe the TSA makes air travel safer despite the fact they failed to detect simulated weapons & bombs 95% of the time.

This smells like a left-wing "feel good" project that makes people feel safer but accomplishes nothing. Kinda like believing "expanded background checks" for gun purchases will stop mass shootings.

I must have given the impression that we're trying to mandate use of our system. I apologize for that. We're not trying to force anyone to use this technology, we're not trying to profit off it, and this has nothing to do with our political positions. We're simply performing academic research into tools and techniques for formally verifying quadcopter software. What kind of safety guarantees can we provide for quadcopters (and more generally cyber-physical systems)?

What does "formally verified" mean? Who verified it and why should we believe or trust said "verifiers"?

That's a great question. Formal verification means different things to different people. In our case, it means foundational verification in a tool called a proof assistant. This tool allows you to express properties about your code/system as precise mathematical theorems, and then prove that these theorems are true. Studies have shown that software built using proof assistants is extremely reliable - foundational verification often provides much stronger guarantees than those provided by traditional techniques such as testing.

In our case, we prove that a model of our system (which includes a model of the physical dynamics of the quadcopter and a specification of our software) guarantees the desired geofence. So what do you have to trust? There are essentially two things:

1. Does the theorem we prove actually capture the property we want?
2. Is the proof actually correct?

To address the second point, the proofs are mechanically checked by a computer program. You might point out that this program could be buggy, but it's generally accepted that if this program says your proof is true, it's almost certainly true. You can't really get a stronger guarantee than that.

The first point is very important though. Most significantly, you have to trust that our model of the physical dynamics of the quadcopter is sufficiently accurate to capture the real world. You're definitely right to be a bit skeptical. One of the things we're working on is building more accurate, realistic models, but ultimately there will be a gap between the model and the real world. For this reason, we always experimentally evaluate everything we do to make sure it corresponds to something in the real world.

 

[PdxSteve]

A "proof assistant". What you are describing sounds a bit like TDD?

 

[Daniel Ricketts]

A "proof assistant". What you are describing sounds a bit like TDD?

It's different from TDD and any other testing methodology. Suppose you're going to write some code to sort a list. If you're going to use testing, you would write a bunch of input-output pairs where the output is the sorted version of the input. You construct these tests so that they hopefully cover all the relevant cases that a sorting function should handle. However, there are an infinite number of possible inputs, so you can never be sure you've covered everything.

If you use a proof assistant, you write a single property expressing what it means for a list to be sorted. Then you write a single theorem stating that for all possible inputs, your code produces the sorted list as output. Then you write a mechanically checkable proof that this theorem holds, thus guaranteeing that for all possible inputs, your code is correct, not just for some finite set of test cases.

Of course, you have to trust that the single property expressing what it means for a list to be sorted is correct. However, I believe it to be significantly easier to trust this property than to trust that you've written a comprehensive set of tests.

 

[Maddog]

Currently, DJI has geofencing software built into their drones.
Are you saying something is wrong with their software?

I guess I don't understand if you are trying to fix an existing problem with existing software?

If not, it just sounds as if you have a solution in search of a problem.

 

[Daniel Ricketts]

Currently, DJI has geofencing software built into their drones.
Are you saying something is wrong with their software?

I guess I don't understand if you are trying to fix an existing problem with existing software?

If not, it just sounds as if you have a solution in search of a problem.

In general, we're trying to increase confidence that cyber-physical systems software works properly. In particular, we're currently trying to build a geofence using techniques that give you extremely strong guarantees that the software does in fact enforce the geofence.

I don't know if there are problems with DJI's existing geofencing software. However, I do know that virtually all realistic software has bugs and that foundational verification has been shown to provide extremely strong guarantees that your software works properly.

 

[Daniel Ricketts]

Currently, DJI has geofencing software built into their drones.
Are you saying something is wrong with their software?

As it turns out, DJI has had problems with their geofence software. Here's a video demonstrating a bug:

To view this content we will need your consent to set third party cookies.
For more detailed information, see our cookies page.

Accept third party cookies

. Essentially, the vehicle seems to get stuck at the boundaries with no way to get back inside. The pilot has no control to move the vehicle back inside the geo fence, and the geo fence software does not move the vehicle back inside. These are the kinds of bugs we're trying to eliminate.

 

[Maddog]

As it turns out, DJI has had problems with their geofence software. Here's a video demonstrating a bug:

To view this content we will need your consent to set third party cookies.
For more detailed information, see our cookies page.

Accept third party cookies

. Essentially, the vehicle seems to get stuck at the boundaries with no way to get back inside. The pilot has no control to move the vehicle back inside the geo fence, and the geo fence software does not move the vehicle back inside. These are the kinds of bugs we're trying to eliminate.

Wow- that's bad! Good luck with your work.

 

[mgrennan]

I think you have a good idea of people concerns. My 40 year old RC field is inside the 5 mile limit (Yes we have a letter of under standing with the airport) but all the "air maps" I've see would restrict you from flying there.

When you talk fencing, I agree with others that you are trying to make a dollar off the fears the public OK It might still be nice if my "Fly Away" doesn't fly over the AirForce base. But then, what about flying under 50 feet in my back yard one mile from the airport? Absolute rules just SUCK.

When you start talking about the quality of the code. Integer over runs and buffer over flows, this is great. I'm sure everyone at DYI Drones (3DR) would like to have a good code review, my self included. As a pilot I would feel safer with someone looking over the shoulders of the developers.

As a big believer in Open Source and doing electronics and software as a hobby as much as RC Flying, I also believe in the freedom to tinker. Freedom to Tinker — Research and expert commentary on digital technologies in public life I never want to see something like the DMCA used on RC flight code to keep me out. (Like most warranties, that's a rule I would be breaking.)

So market your work carefully.