Copyrights to these papers may be held by the publishers. The download 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.

Tze-Meng Low and Franz Franchetti (Proc. IEEE International Symposium on High Assurance Systems Engineering (HASE), 2017)
High Assurance Code Generation for Cyber-Physical Systems
Preprint (188 KB)
Published paper (link to publisher)
Bibtex

High Assurance SPIRAL (HA-SPIRAL) is a tool that synthesizes a faithful and high performance implementation from the mathematical specification of a given controller or monitor. At the heart of HA-SPIRAL is a mathematical identity rewrite engine based on a computer algebra system. The rewrite engine refines the mathematical expression provided by a control engineer, through mathematical identities, into an equivalent mathematical expression that can be implemented in code. In this paper, we discuss the use of HA-SPIRAL in generating provably correct and high-performance implementations for different controllers and monitors for autonomous land and air vehicles.

Keywords:
Coding/Decoding, High assurance, Cyber-physical systems