Confident Algorithms with Formal Proof Techniques

Sensor fusion software is unique with its combination of firmware-like layers, responsible for reading and validating sensor data, and higher-level algorithmic software, responsible for producing synthesized, actionable data. Because of the criticality of these systems, they require extensive testing and verification to increase confidence that the computed data can be trusted. From a software development point of view, the traditional approach is to rely on the C or C++ programming language, and to offset its inherent safety vulnerabilities by using expensive tooling and human-based processes. In this presentation we will present an alternative approach, through the usage of a different programming language which was designed for safety critical systems and gives developers tools to write safe and secure firmware, as-well-as, robust high-level algorithmic code with the same ecosystem of language and tooling. Topics covered:

• Overview of Ada and SPARK language features for firmware development
• Overview of Ada and SPARK language features for algorithm and high-level software development
• Overview of formal proof and how it differs from traditional static analysis techniques
• Integration with existing C code bases
• Performances considerations
• ISO 26262 considerations and benefits
• Resources for Ada and SPARK in the software community