High Assurance SPIRAL: Scalable and Performance Portable Domain-Specific Control System Synthesis

(FA87501220291 — DARPA HACMS)

Franz Franchetti (PI), José; M. F. Moura (Co-PI), Manuela Veloso (Co-PI), Andre Platzer (Co-PI), Soummya Kar (Co-PI), David Padua (Co-PI), Jeremy Johnson (Co-PI), Mike Franusich (Co-PI)

Post-Docs: Stefan Mitsch, Khalil Ghorbal, Jean-Baptiste Jeannin, Pooyan Fazli
PhD Students: Vadim Zaliva, Richard Veras, Yuan Chen, Liangyan Gui, Juan Pablo Mendoza, Lingchuan (LC) Meng, Amarin Phaosawasdi
Engineers: Brian Duff, Jason Larkin
Alumni: Aliaksei Sandryhaila, Jan-David Quesel, Seokje Seo, Kevin Owens, Nicolas Huynh Thien, Christos Angelopoulos

Overview

hacms1

High Assurance SPIRAL aims to solve the last mile problem for the synthesis of high assurance implementations of controllers for vehicular systems that are executed in todays and future embedded and high performance embedded system processors. High Assurance SPIRAL is a scalable methodology to translate a high level specification of a high assurance controller into a highly resource-efficient, platform-adapted, verified control software implementation for a given platform in a language like C or C++. High Assurance SPIRAL proves that the implementation is equivalent to the specification written in the control engineer's domain language. Our approach scales to problems involving floating-point calculations and provides highly optimized synthesized code. It is possible to estimate the available headroom to enable assurance/performance trade-offs under real-time constraints, and enables the synthesis of multiple implementation variants to make attacks harder. At the core of High Assurance SPIRAL is the Hybrid Control Operator Language (HCOL) that leverages advanced mathematical constructs expressing the controller specification to provide high quality translation capabilities. Combined with a verified/certified compiler, High Assurance SPIRAL provides a comprehensive complete solution to the efficient synthesis of verifiable high assurance controllers. We demonstrate High Assurance SPIRAL’s capability by co-synthesizing proofs and implementations for attack detection and sensor spoofing algorithms and deploy the code as ROS nodes on the Landshark unmanned ground vehicle and on a “Synthetic Car” in a real-time simulator.

Approach

hacms2

High Assurance SPIRAL synthesizes high assurance controller software implementations in two components: 1) Virtual high assurance sensors that fuse multiple multimodality sensors (environmental or vehicle state,) prior data (e.g., a digital map of the terrain or a motor's torque/current response curve), dynamical vehicle models, and statistically learned uncertainties into one fused virtual sensor with an associated accuracy/confidence value or an inconsistency exception. 2) High assurance monitors and controllers (e.g., model-based monitors or PID) that compute actuation inputs, detect sensor failures and attacks, and switch to safe-mode if an exception is detected. High Assurance Spiral outputs a verified library of implementations for the virtual high assurance sensors and high assurance controllers for the hybrid physical system, including verification, design space exploration and generation of multiple implementation variants. The system relies on a secure/verified environment, from the microkernel level (e.g., CertiKOS, http://flint.cs.yale.edu/certikos/) to the full OS, providing the necessary communication services to sensors and actuators and the hypervisor, and a verified/trusted compiler (e.g., CompCert, http://compcert.inria.fr/).


hacms3Hybrid Control Operator Language (HCOL). Functions, operators, matrices and linear algebra ideas play a crucial role as representational elements of the above-mentioned dynamics, sensing, and control questions. The key insight is that for a properly chosen sub-class of problems in this space a domain specific language (DSL) can be constructed that fits into the theoretical constraints of the original autotuning and program generation Spiral system (http://www.spiral.net). SPIRAL's code generation engine is based on matrix algebra and mathematical identities, encoded as rewriting rules that drive a backtracking search to satisfy the constraints given by the specification and target hardware. With careful HCOL design, these advantages and the power of Spiral can be made available for control code/proof co-synthesis. We are formalizing statistical and continuous control and signal processing algorithms as operators, and operator identities. These operators are subsequently explained (expanded) through mathematical identities interpreted as rewriting rules.

The formal framework extends all the way down to a basic operator calculus that can be interpreted as a functional programming language. Then code-level optimizing rewriting rules perform low level optimizations necessary for high performance code. The transformations are proven correct in the Isabelle proof assistant (http://www.cl.cam.ac.uk/research/hvg/Isabelle/). The final code is pretty-printed as highly efficient C code and compiled either with a certified compiler (CompCert, http://compcert.inria.fr/) or a vendor compiler.

HCOL formulas are derived from higher-level formal systems. For instance, we derive conditions that a safe robot must fulfil using the KeYmaera system (http://symbolaris.com/info/KeYmaera.html), and then convert these conditions into HCOL using Sphinx (http://symbolaris.com/info/KeYmaera.html#Sphinx).

Algorithm library. Part of the High Assurance SPIRAL effort is to develop a library of control algorithms and sensor fusion algorithms expressed in HCOL. We are formalizing algorithms based on set calculus, statistics, machine learning, audio processing, and image processing. These algorithms are chosen to detect attacks while being simple enough to be targets for formal verification and code synthesis.

Target Platforms

Our major targets are the LandShark robot by Black-I Robotics (http://www.blackirobotics.com/) and a simulated car modeled after an American Build Car. Recently we expanded the target list to include air vehicles such as small quadcopters (Arducopter) and Boeing’s Unmanned Little Bird (ULB, http://www.boeing.com/boeing/rotorcraft/military/ulb/). We also target the CoBot Robots developed by Co-PI Veleoso (http://www.cs.cmu.edu/~coral/projects/cobot/).

hacms4 hacms5

Design and Simulation Tools

hacms6

Publications

Journal Publications
  1. Stefan Mitsch, André Platzer
    ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models
    Formal Methods in System Design, 49(1), pp. 33-74, Springer 2016. Special issue for selected papers from RV2014.
  2. Stefan Mitsch, Grant Olney Passmore, André Platzer
    Collaborative Verification-Driven Engineering of Hybrid Systems
    Mathematics in Computer Science, 8(1), pp. 71-97, Springer 2014. Special issue on Enabling Domain Experts to use Formalized Reasoning.
  3. Stefan Mitsch, Khalil Ghorbal, André Platzer
    On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles
    Robotics: Science and Systems IX, 2013.
  4. André Platzer
    Analog and Hybrid Computation: Dynamical Systems and Programming Languages
    Bulletin of the EATCS, 2014. Invited paper in The Logic in Computer Science Column by Yuri Gurevich.
Conference Papers
  1. Tze Meng Low, Franz Franchetti
    High Assurance Code Generation for Cyber-Physical Systems
    Proceedings of the 18th IEEE International Symposium on High Assurance Systems Engineering (HASE 2017), Jan 2017.
  2. Andrew Sogokon, Khalil Ghorbal, Paul B. Jackson, André Platzer
    A Method for Invariant Generation for Polynomial Continuous Systems
    In Verification, Model Checking, and Abstrat Interpretation. Barbara Jobstmann and K. Rustan M. Leino, Eds. Vol 9583 of LNCS, pp. 268-288. Springer, 2016. Proceedings of the 17th Internation Conference, VMCAI 2016.
  3. H. V. Koops, F. Franchetti
    An Ensemble Technique for Estimating Vehicle Speed and Geer Position from Acoustic Data
    Proceedings of the 20th International Conference on Digital Signal Processing (DSP), 2015.
  4. Khalil Ghorbal, Andrew Sogokon, André Platzer
    A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets
    In Verification, Model Checking, and Abstrat Interpretation. Deepak D'Souza, Akash Lai, and Kim G. Larsen, Eds. Vol. 8931 of LNCS, pp. 431-448, Springer, 2015. Proceedings of 16th International Conference, VMCAI 2015.
  5. F. Franchetti, A. Sandryhaila, J. R. Johnson
    High Assurance SPIRAL
    Proceedings of SPIE, 2014.
  6. Stefan Mitsch, Jan-David Quesel, André Platzer
    From Safety to Guilty and from Liveness to Niceness
    Formal Methods for Robotics and Automation, 2014.
  7. Vadim Zaliva, Franz Franchetti
    Barometric and GPS Altitude Sensor Fusion
    Proceedings of the International Conference on Acoustics, Speech, and Signal Processing (ICASSP), 2014.
  8. Juan Pablo Mendoza, Manuela Veloso, Reid Simmons
    Early Detection of Anomalous Clusters for Task Execution Monitoring
    IEEE International Conference on Robotics and Automation (ICRA), 2014.
  9. Stefan Mitsch, Jan-David Quesel, André Platzer
    Refactoring, Refinement, and Reasoning: A Logical Characterization for Hybrid Systems
    In Proceedings of the 19th International Symposium on Formal Methods, Cliff B. Jones, Pekka Pihlajasaari, and Jun Sun, Eds. Vol. 8442 of LNCS, pp. 481-496, Springer, 2014.
  10. Stefan Mitsch, André Platzer
    ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models
    In Runtime Verification, Borzoo Bonakdarpour and Scott A. Smolka, Eds. Vol 8734 of LNCS, pp. 199-214, Springer 2014. Proceedings of RV 2014.
  11. Khalil Ghorbal, André Platzer
    Characterizing Algebraic Invariants by Differential Radical Invariants
    In Tools and Algorithms for the Construction and Analysis of Systems, Erika Abrahám and Klaus Havelund, Eds. Vol. 8413 of LNCS, pp. 279-294. Springer, 2014. Proceedings of TACAS 2014.
  12. Khalil Ghorbal, Andrew Sogokon, André Platzer
    Invariance of Conjunctions of Polynomial Equalities for Algebraic Differential Equations
    In Proceedings of 21st International Static Analysis Symposium, Markus Müller-Olm and Helmut Seidl, Eds. Vol. 8723 of LNCS, pp. 151-167, Springer, 2014.
  13. Stefan Mitsch, Grant Olney Passmore, André Platzer
    A Vision of Collaborative Verification-Driven Engineering of Hybrid Systems
    Do-Form @ AISB 2013.
  14. Juan Pablo Mendoza, Manuela Veloso, Reid Simmons
    Motion Interference Detection in Mobile Robots
    IEEE International Conference on Intelligent Robots and Systems (IROS), 2012.
  15. Juan Pablo Mendoza, Manuela Veloso, Reid Simmons
    Mobile Robot Fault Detection Based on Redundant Information Statistics
    IEEE International Conference on Intelligent Robots and Systems (IROS), 2012.

Copyrights to many of the above papers are held by the publishers. The attached PDF files are preprints. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder. Some links to papers above connect to IEEE Xplore with permission from IEEE, and viewers must follow all of IEEE's copyright policies.