VeriDrone project: building quadcopters people can bet their lives on

[Daniel Ricketts]

For the past year or so, I've been working on the VeriDrone project, in which we formally verify quadcopter software. We have an active blog, which I want to share with the community to get some feedback from real practitioners. Here's one blog post giving a brief introduction to the project: http://ucsd-pl.github.io/veridrone/talk/2015/10/22/intro-cns-review.html#read-more. Please let me know what you think.

 

[GJH105775]

For the past year or so, I've been working on the VeriDrone project, in which we formally verify quadcopter software. We have an active blog, which I want to share with the community to get some feedback from real practitioners. Here's one blog post giving a brief introduction to the project: http://ucsd-pl.github.io/veridrone/talk/2015/10/22/intro-cns-review.html#read-more. Please let me know what you think.

That is a really bold, risky business with some liability attached haha. I assume though that you would have a release of liability, but still bold haha.

I'd be pretty interested is seeing how everything goes. I really do like some of the features though, DJI has been incorporating some of these, do you have a way to install it alongside the flight controller, perhaps everything would plug into it and from your device into an existing flight controller? This will allow features of any flight controller, but if something abnormal happened you could process and change user input side if it were user error OR motor output side if it were an error like a fly-away.

 

[Daniel Ricketts]

That is a really bold, risky business with some liability attached haha. I assume though that you would have a release of liability, but still bold haha.

I'd be pretty interested is seeing how everything goes. I really do like some of the features though, DJI has been incorporating some of these, do you have a way to install it alongside the flight controller, perhaps everything would plug into it and from your device into an existing flight controller? This will allow features of any flight controller, but if something abnormal happened you could process and change user input side if it were user error OR motor output side if it were an error like a fly-away.

You can follow us on Twitter (@VeriDrone) if you want to see how things are going.

We do actually run our verified code alongside an off-the-shelf flight controller, namely ardupilot. Our goal is to retain the benefits of a state of the art flight controller while providing strong safety guarantees. We want to do so by running our code (which we call a shim or monitor) as the last thing before signals are sent to motors. This means that if the user or the existing flight controller code attempts to send unsafe signals to the motors, our code can intervene.

At the moment, we almost achieve this. Our code outputs signals to an existing (unverified) attitude controller which outputs signals to motor mixing code (also unverified). However, we plan to eventually verify all of this code, so that the guarantees are as strong as possible.

If you're interested in learning more, you can check out a paper that we published on some preliminary work here: http://ucsd-pl.github.io/veridrone/papers.html. That webpage also contains a talk describing the work in that paper. This paper only describes a software module that prevents the quadcopter from going too high or exceeding a vertical velocity. However, we have currently unpublished results in which we enforce more sophisticated bounds on the quadcopter.

You can also check out our blog here: http://ucsd-pl.github.io/veridrone/index.html. It describes interesting challenges we've encountered in this project. Feel free to comment under the blog posts or email us. We're always looking for feedback.

 

[GJH105775]

You can follow us on Twitter (@VeriDrone) if you want to see how things are going.

We do actually run our verified code alongside an off-the-shelf flight controller, namely ardupilot. Our goal is to retain the benefits of a state of the art flight controller while providing strong safety guarantees. We want to do so by running our code (which we call a shim or monitor) as the last thing before signals are sent to motors. This means that if the user or the existing flight controller code attempts to send unsafe signals to the motors, our code can intervene.

At the moment, we almost achieve this. Our code outputs signals to an existing (unverified) attitude controller which outputs signals to motor mixing code (also unverified). However, we plan to eventually verify all of this code, so that the guarantees are as strong as possible.

If you're interested in learning more, you can check out a paper that we published on some preliminary work here: http://ucsd-pl.github.io/veridrone/papers.html. That webpage also contains a talk describing the work in that paper. This paper only describes a software module that prevents the quadcopter from going too high or exceeding a vertical velocity. However, we have currently unpublished results in which we enforce more sophisticated bounds on the quadcopter.

You can also check out our blog here: http://ucsd-pl.github.io/veridrone/index.html. It describes interesting challenges we've encountered in this project. Feel free to comment under the blog posts or email us. We're always looking for feedback.

Sounds great. Have you considered having it also monitor user input that way it can look for any anomalies that it may not otherwise find? I really think this is a great project, and perhaps more than just professionals would be interested (who wants a $1000 device to crash?).

 

[Daniel Ricketts]

Sounds great. Have you considered having it also monitor user input that way it can look for any anomalies that it may not otherwise find? I really think this is a great project, and perhaps more than just professionals would be interested (who wants a $1000 device to crash?).

At the moment, we don't directly monitor user input. However, in a sense, we indirectly monitor user input since our code checks every signal getting sent to the motors, regardless of whether it originated with a user's action or with some autopilot command. Do you think we could gain something by directly monitoring the user's input? What sort of issues could we detect?

I definitely hope that non-professionals are interested in our work. Actually, I think that novice hobbyist pilots could benefit from this type of work. A beginner pilot might want code running that guarantees some sort of safety net. It would be nice to know that, no matter what stupid things I do as a pilot (and I do a lot of stupid things), the quadcopter won't fly too close to an airport or somewhere else dangerous.

 

[GJH105775]

At the moment, we don't directly monitor user input. However, in a sense, we indirectly monitor user input since our code checks every signal getting sent to the motors, regardless of whether it originated with a user's action or with some autopilot command. Do you think we could gain something by directly monitoring the user's input? What sort of issues could we detect?

I definitely hope that non-professionals are interested in our work. Actually, I think that novice hobbyist pilots could benefit from this type of work. A beginner pilot might want code running that guarantees some sort of safety net. It would be nice to know that, no matter what stupid things I do as a pilot (and I do a lot of stupid things), the quadcopter won't fly too close to an airport or somewhere else dangerous.

I believe that it could detect problems similar to a fly away if the user input was not reasonable to the motor output, though I don't know if any gained latency would be worth it for the scope of your project. If it keeps you from crashing it is a REALLY big benefit, now I understand that it would hot have obstacle avoidance, or buckshot avoidance haha.