VeriDrone

Foundational Verification of Cyber-Physical Systems

Blog
Overview
Papers
Code
Videos
People

Newest Posts

  • The Real Induction (Feb 17, 2016)

    We do a lot of proofs as part of this project, many of them using induction. In computer science, we’re usually taught that induction can prove facts about natural numbers, lists, trees, and other discrete structures. But in VeriDrone, we deal with the physical world, which means we work with real numbers. Can we use induction to prove facts about the real numbers? It turns out we can, though the induction rule is more subtle than you might expect.

  • Embedding Imperative Programs in LTL (Nov 28, 2015)

    In this post I’ll describe how we embed certain classes of imperative programs into LTL, the logic we use to model quadcopter behavior. Doing so is key to being able to reason about how concrete quadcopter-controller implementations will behave in the context of the copter’s physical dynamics.

  • Short introduction to the VeriDrone project (Oct 22, 2015)

    Here is a brief introduction to the motivation, goals, and current progress of the VeriDrone project. This was a short presentation given to industry experts at a recent research review.

  • Model meets reality: practical monitor verification (Oct 20, 2015)

    Back in July, we built a software module to “guarantee” that a quadcopter never leaves a rectangular box. We spent months proving this guarantee as a mathematical theorem. We were pretty proud of ourselves, until we actually bothered to run our code. As it turns out, when it comes to cyber-physical systems, there’s more to it then just proving theorems.

  • Talk at MEMOCODE 2015 (Sep 25, 2015)

    We just got back from MEMOCODE 2015. The conference was a bit outside our normal community, which made it a great experience. We had an opportunity to speak with and hear talks from some cyber-physical systems experts like Georgios Fainekos, Klaus Schneider, and Pavithra Prabhakar and to see an interesting keynote presentation from Rajeev Alur.

  • Aggressive Flying to Test Height Monitor (Sep 17, 2015)

    Here is a video where we are testing our Coq verified altitude limiter with some aggressive flying close to the height boundary. First, I try flying up to the altitude boundary while flying aggressively to the right. Then, with throttle pushed all the way up, I try various motions in other directions, including so-called yaw (essentially pivoting). As you can see, the altitude limiter keeps engaging (since the throttle is all the way up), and it keeps the quadcopter within the appropriate bounds, while allowing control in other dimensions.

  • Fun anecdote about the controller (Sep 8, 2015)

    We’re catching up with our video archive, and I found this fun video that illustrates the kinds of non-research fun we’ve been having! A frustrating problem that took us a long time to fix, and caused us to cry out “D’oh”!

  • Quadcopter stuck outside boundaries (Aug 7, 2015)

    In an earlier post, I mentioned that the first test of our rectangular bounding monitor had a few interesting problems, and I described one of them. In this post, I’ll describe another interesting problem that occurred during the test, and the cause that we later discovered.

  • Improper quadcopter orientation (Jul 30, 2015)

    As I mentioned in this post, the first test of our rectangular bounding monitor had a few interesting problems. In order to discover the cause of the problems, we needed to run more tests. However, running new tests seemed to uncover a new problem: the monitor had no idea where it was.

  • Air-traffic control for drones (Jul 25, 2015)

    It looks like Google and a bunch of other companies are investigating an air-traffic control system for drones. It would be pretty exciting to see “thousands of drones…routinely ply the skies above cities.” It also opens up an interesting long-term direction for our project: distributed-systems aspects of UAV safety.

  • Paper accepted to MEMOCODE 2015! (Jul 24, 2015)

    We had a paper accepted to MEMOCODE 2015. The paper describes preliminary work implementing and formally verifying in Coq an upper bound altitude monitor and and upper bound vertical velocity monitor for a quadcopter. Check it out here.

  • Strange behavior of quadcopter at boundaries (Jul 17, 2015)

    We recently performed the first test of our new rectangular bounding monitor. This runtime monitor is designed to prevent the quadcopter from violating any of the following bounds: