High Assurance Spiral: Scalable and Performance Portable Domain-Specific Control System Synthesis (FA87501220291)
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)
Systems Scientists: Tze Meng Low
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
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.
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/).
Hybrid 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. Bydesigning HCOL carefully, 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.
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/).
Design and Simulation Tools
Our research is bundled in the High Assurance Spiral tool chain, an open source toolbox built on the Spiral Engine (http://www.spiralgen.com). The High Assurance Spiral Tool Chain integrates Spiral, KeYmaera, Sphinx, Isabelle, ROS, and deployment on robots.
Stefan Mitsch, Khalil Ghorbal, Andre Platzer On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles
Robotics: Science and Systems IX.
André Platzer Analog and Hybrid Computation: Dynamical Systems and Programming Languages
Bulletin of the EATCS, Invited paper in The Logic in Computer Science Column by Yuri Gurevich.
H. V. Koops, F. Franchetti An Ensemble Technique for Estimating Vehicle Speed and Gear Position from Acoustic Data
Proceedings of the 20th International Conference on Digital Signal Processing (DSP) 2015, accepted.
Stefan Mitsch, André Platzer ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models