VeriDrone
Foundational Verification of Cyber-Physical Systems
Verification of Sampled-Data Systems using Coq (Dissertation)
Daniel Ricketts
Abstract: Due to their safety-critical nature, cyber-physical systems (CPS) demand the most rigorous verification techniques. However, the complexity of the domain puts many cyber-physical systems outside the scope of automated verification tools. Formal deductive proofs hold the potential to verify virtually any property of any system, but proofs for practical cyber-physical systems often require an impractical amount of manual effort. This proof burden can be mitigated by capturing common reasoning patterns in powerful higher-order proof rules. Existing work has focused on proof rules applicable to arbitrary hybrid systems (a formal model for CPS), but many systems actually fall into more constrained classes. One such class of systems are called sampled-data systems, in which a discrete controller runs periodically. In this dissertation, we complement general hybrid system proof rules with a series of rules that leverage the particular structure of sampled-data systems. We demonstrate the applicability of these rules on the double integrator, an important model in robotic and vehicle systems. All work is formalized in the Coq proof assistant, whose expressive logic is crucial to maintaining soundness while applying domain-specific proof rules for sampled-data systems. Finally, we experimentally evaluate our results by implementing verified controllers on a quadcopter and conducting flight tests.
Modular Deductive Verification of Sampled-Data Systems (EMSOFT 2016)
Daniel Ricketts, Gregory Malecha, Sorin Lerner (UCSD)
Abstract: Unsafe behavior of cyber-physical systems can have disastrous consequences, motivating the need for formal verification of these kinds of systems. Deductive verification in a proof assistant such as Coq is a promising technique for this verification because it (1) justifies all verification from first principles, (2) is not limited to classes of systems for which full automation is possible, and (3) provides a platform for proving powerful, higher-order modularity theorems that are crucial for scaling verification to complex systems. In this paper, we demonstrate the practicality, utility, and scalability of this approach by developing in Coq sound and powerful rules for modular construction and verification of sampled-data cyber-physical systems. We evaluate these rules by using them to verify a number of non-trivial controllers enforcing safety properties of a quadcopter, e.g. a geo-fence. We show that our controllers are realistic by running them on a real, flying quadcopter.
Towards Foundational Verification of Cyber-physical Systems (SoSCYPS 2016)
Gregory Malecha, Daniel Ricketts, Mario M. Alvarez, Sorin Lerner (UCSD)
Abstract: The safety-critical aspects of cyber-physical systems motivate the need for rigorous analysis of these systems. In the literature this work is often done using idealized models of systems where the analysis can be carried out using high-level reasoning techniques such as Lyapunov functions and model checking. In this paper we present VeriDrone, a foundational framework for reasoning about cyber-physical systems at all levels from high-level models to C code that implements the system. VeriDrone is a library within the Coq proof assistant enabling us to build on its foundational implementation, its interactive development environments, and its wealth of libraries capturing interesting theories ranging from real numbers and differential equations to verified compilers and floating point numbers. These features make proof assistants in general, and Coq in particular, a powerful platform for unifying foundational results about safety-critical systems and ensuring important properties at all levels of the stack.
Formal Verification of Stability Properties of Cyber-physical Systems (CoqPL 2016)
Matthew Chan, Daniel Ricketts, Sorin Lerner, Gregory Malecha (UCSD)
Abstract: We increasingly rely on computers to interact with the physical world for us. At the large end, software underlies the control systems of commercial aircraft and power plants, and at the small end it controls medical devices and hobbiest UAVs. The failure of any of these systems can have severe consequences which are often measured in the loss of human lives. Formal verification has proven a promising approach to achieving very strong guarantees in more classic areas of computer science. In this work we present an overview of our experiences formalizing stability properties of hybrid systems using the Coq proof assistant.
Towards Verification of Hybrid Systems in a Foundational Proof Assistant (MEMOCODE 2015)
Daniel Ricketts, Gregory Malecha, Mario Alvarez, Vignesh Gowda, Sorin Lerner (UCSD)
Abstract: Unsafe behavior of hybrid systems can have disastrous consequences, motivating the need for formal verification of the software running on these systems. Foundational verification in a proof assistant such as Coq is a promising technique that can provide extremely strong, foundational, guarantees about software systems. In this paper, we show how to apply this technique to hybrid systems. We define a TLA-inspired formalism in Coq for reasoning about hybrid systems and use it to verify two quadcopter modules: the first limits the quadcopter's velocity and the second limits its altitude. We ran both of these modules on an actual quadcopter, and they worked as intended. We also discuss lessons learned from our experience foundationally verifying hybrid systems.