Franz Franchetti

home  |  short cv  |  projects  |  publications  |  professional activity  |  courses  |  students  |  rockin’ 

  DARPA HACMS:
   
 
hacms
   
 

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
   

Overview

hacms1High 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

hacms2High 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. Byhacms3designing 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.

HELIX: Formally Verified Spiral

We have a public GitHub repository for the Spiral HELIX project. HELIX is a formally verified language and rewriting engine for generating high-performance implementations for a variety of numerical algorithms. Based on the existing Spiral system, HELIX adds the rigor of formal verification of its correctness using the Coq proof assistant. Related information can be found in the publications listed on the GitHub-HELIX repository site.

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 Veloso (http://www.cs.cmu.edu/~coral/projects/cobot/).

                 hacms4                  hacms5
 

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.

hacms6
 

Publications

Journal Publications

Stefan Mitsch and André Platzer
ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models
Formal Methods in System Design, 49(1), pp. 33-74. 2016. Special issue for selected papers from RV’14.

Stefan Mitsch, Grant Olney Passmore and André Platzer
Collaborative Verification-Driven Engineering of Hybrid Systems 
 8(1), pp. 71-97, 2014. Special issue on Enabling Domain Experts to use Formalized Reasoning.

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

Tze Meng Low and 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.

Andrew Sogokon, Khalil Ghorbal, Paul B. Jackson and André Platzer 
A Method for Invariant Generation for Polynomial Continuous Systems
In Verification, Model Checking, and Abstract Interpretation, Barbara Jobstmann and K. Rustan M. Leino, Eds.
Proceedings of the17th International Conference, VMCAI 2016, St. Petersburg, Florida, USA, January 17-19, 2016,
Vol. 9583 of LNCS, pp. 268-288. Springer, 2016.

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.

Khalil Ghorbal, Andrew Sogokon, and André Platzer 
A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets. 
In Verification, Model Checking, and Abstract Interpretation, Deepak D'Souza, Akash Lal, and Kim Guldstrand Larsen, Eds.
Proceedings of 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015, vol. 8931 of LNCS, pp. 431-448. Springer, 2015.

Stefan Mitsch, André Platzer
ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models
RV 2014.

F. Franchetti, A. Sandryhaila, J. R. Johnson
High Assurance SPIRAL
Proceedings of SPIE 2014.

Stefan Mitsch, Jan-David 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, Jan-David Quesel, André Platzer
Refactoring, Refinement, and Reasoning: A Logical Characterization for Hybrid Systems
FM 2014.

Stefan Mitsch and André Platzer 
ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models 
In Runtime Verification, Borzoo Bonakdarpour and Scott A. Smolka, Eds. 
Proceedings of 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014.
Vol. 8734 of LNCS, pp. 199-214. Springer, 2014.

Stefan Mitsch, Jan-David Quesel and André Platzer 
Refactoring, Refinement, and Reasoning: A Logical Characterization for Hybrid Systems 
In Proceedings of 19th International Symposium on Formal Methods, Cliff B. Jones, Pekka Pihlajasaari and Jun Sun, Eds.
FM, Singapore, vol. 8442 of LNCS, pp. 481-496. Springer, 2014.

Khalil Ghorbal and André Platzer 
Characterizing Algebraic Invariants by Differential Radical Invariants. 
In Tools and Algorithms for the Construction and Analysis of Systems, Erika Ábrahám and Klaus Havelund, Eds. 
Proceedings of TACAS 2014, vol. 8413 of LNCS, pp. 279-294. Springer, 2014.

Khalil Ghorbal, Andrew Sogokon, and André Platzer. 
Invariance of conjunctions of polynomial equalities for algebraic differential equations 
In Proceeding of 21st International Static Analysis Symposium, Markus Müller-Olm and Helmut Seidl, Eds.  
Vol. 8723 of LNCS, pp. 151-167. Springer, 2014.

Stefan Mitsch, Grant Olney Passmore, Andre Platzer
A Vision of Collaborative Verification-Driven Engineering of Hybrid Systems
Do-Form @ 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.

 

home  |  short cv  |  projects  |  publications  |  professional activity  |  courses  |  students  |  rockin’