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)
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)
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.
Strange behavior of quadcopter at boundaries
(Jul 17, 2015)