VeriDrone
Foundational Verification of Cyber-Physical Systems
|
Funded by NSF grant 1544757 |
Errors in cyber-physical systems can lead to disastrous consequences. Classic examples date back to the Therac-25 radiation incidents in 1987 and the Ariane 5 rocket crash in 1996. More recently, Toyota's unintended acceleration bug was caused by software errors, and certain cars were found vulnerable to attacks that can take over key parts of the control software, allowing attackers to even disable the brakes remotely. Pacemakers have also been found vulnerable to attacks that can cause deadly consequences for the patient.
To reduce the chances of such errors happening, this project investigates the application of a technique called Foundational Verification to cyber-physical systems. In Foundational Verification, the system being developed is proved correct, in full formal detail, using a Proof Assistant. Because proofs in Foundational Verification are carried out in such complete detail, this project will pave the way to reaching previously unattainable levels of safety for cyber-physical systems. To make sure that the techniques in this project are practical, they will be evaluated within the context of a real flying quadcopter. Although the initial work focuses on quadcopters, the concepts, ideas, and research contributions have the potential for transformative impact on other kinds of systems, including power-grid software, cars, avionics and medical devices (from pacemakers and insulin pumps to defibrillators and radiation machines).
Here is a video of our quadcopter flying (if you cannot see the video below, here is a link). Also note that there is audio!
This video shows the first test flight for our verified altitude monitor, which enforces an upper bound on altitude. This monitor could for example be used to enforce the FAA regulation stating that recreational quadcopters stay below 400 feet. Our altitude monitor is placed between the pre-existing software controller that runs on the quadcopter and the four motors of the quadcopter. In particular, our monitor takes as input the four motor values produced by the pre-existing controller, and it produces four new motor values. If our monitor predicts that no violation of the altitude bound will occur (in essence because there is still enough time to act to avoid any violations), our monitor will pass the four motor values unchanged. However, if our monitor predicts that an intervention is needed to avoid an altitude bound violation, it produces a new set of motor values to slow the quadcopter's upward climb.
What you see in the video above is that pilot Sorin is pushing the upward throttle on the handleld remote controller, which makes the quadcopter climb steadily upward. It's important to realize that all through the video, Sorin is pushing the throttle upwards on the quadcopter handheld controller. The quadcopter climbs until it reaches close to the altitude limit (10 meters), at which point our monitor engages. Because our monitor engages, the quadcopter stops going upward, even though Sorin has the throttle all the way up on the handheld controller. Then at the end of the video, Sorin disables the monitor (with a switch on the handheld controller), and the quadcopter shoots up past the altitude bound. You can hear Gregory proclaim victory!
You can hear in the video (and we observed in practice) that there was a slight violation of the bound, which is due to noise in sensors and actuators. This is a definitely a challenge we want to address in future work: how to reason formally and foundationally about this kind of noise.