
DARPA HACMS: 







High Assurance Spiral: Scalable and Performance Portable DomainSpecific Control System Synthesis (FA87501220291) 



Franz Franchetti (PI), José M. F. Moura (CoPI), Manuela Veloso (CoPI), Andre Platzer (CoPI), Soummya Kar (CoPI), David Padua (CoPI), Jeremy Johnson (CoPI), Mike Franusich (CoPI)
Systems Scientists: Tze Meng Low
PostDocs: Stefan Mitsch, Khalil Ghorbal, JeanBaptiste 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, JanDavid Quesel, Seokje Seo, Kevin Owens, Nicolas Huynh Thien, Christos Angelopoulos




Overview
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 resourceefficient, platformadapted, 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 floatingpoint calculations and provides highly optimized synthesized code. It is possible to estimate the available headroom to enable assurance/performance tradeoffs under realtime 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 cosynthesizing 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 realtime simulator. 



Approach
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., modelbased monitors or PID) that compute actuation inputs, detect sensor failures and attacks, and switch to safemode 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 abovementioned dynamics, sensing, and control questions. The key insight is that for a properly chosen subclass 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 cosynthesis. 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 codelevel 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 prettyprinted 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 higherlevel 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 BlackI 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 CoPI 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.




Publications
Journal Publications
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.
Conference Papers
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 CyberPhysical System Models
RV 2014.
F. Franchetti, A. Sandryhaila, J. R. Johnson
High Assurance SPIRAL
Proceedings of SPIE 2014.
Stefan Mitsch, JanDavid Quesel, André Platzer
From Safety to Guilty and from Liveness to Niceness
Formal Methods for Robotics and Automation 2014.
Khalil Ghorbal and Andre Platzer
Characterizing Algebraic Invariants by Differential Radical Invariants?
TACAS 2014.
Vadim Zaliva and Franz Franchetti
Barometric and GPS Altitude Sensor Fusion
ICASSP 2014.
Juan Pablo Mendoza, Manuela Veloso, Reid Simmons
Early Detection of Anomalous Clusters for Task Execution Monitoring
ICRA 2014.
Stefan Mitsch, JanDavid Quesel, André Platzer
Refactoring, Refinement, and Reasoning: A Logical Characterization for Hybrid Systems
FM 2014.
Stefan Mitsch, Grant Olney Passmore, Andre Platzer
A Vision of Collaborative VerificationDriven Engineering of Hybrid Systems
DoForm @ AISB 2013.
Juan Pablo Mendoza, Manuela Veloso, Reid Simmons
Motion Interference Detection in Mobile Robots
IROS 2012.
Juan Pablo Mendoza, Manuela Veloso, Reid Simmons
Mobile Robot Fault Detection based on Redundant Information Statistics
IROS 2012.

