Conference proceeding
High Assurance SPIRAL
SIGNAL PROCESSING, SENSOR/INFORMATION FUSION, AND TARGET RECOGNITION XXIII, v 9091
01 Jan 2014
Featured in Collection : UN Sustainable Development Goals @ Drexel
Abstract
In this paper we introduce High Assurance SPIRAL to solve the last mile problem for the synthesis of high assurance implementations of controllers for vehicular systems that are executed in today's 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 SPIRALs 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.
Metrics
Details
- Title
- High Assurance SPIRAL
- Creators
- Franz Franchetti - Carnegie Mellon UniversityAliaksei Sandryhaila - Carnegie Mellon UniversityJeremy R. Johnson - Drexel University
- Publication Details
- SIGNAL PROCESSING, SENSOR/INFORMATION FUSION, AND TARGET RECOGNITION XXIII, v 9091
- Series
- Proceedings of SPIE
- Publisher
- Spie-Int Soc Optical Engineering
- Number of pages
- 7
- Grant note
- FA8750-12-2291 / DARPA; United States Department of Defense; Defense Advanced Research Projects Agency (DARPA)
- Resource Type
- Conference proceeding
- Language
- English
- Academic Unit
- Computer Science
- Web of Science ID
- WOS:000343864000054
- Scopus ID
- 2-s2.0-84906282092
- Other Identifier
- 991019168279704721
UN Sustainable Development Goals (SDGs)
This publication has contributed to the advancement of the following goals:
InCites Highlights
Data related to this publication, from InCites Benchmarking & Analytics tool:
- Collaboration types
- Domestic collaboration
- Web of Science research areas
- Engineering, Electrical & Electronic
- Optics