aiT automatically computes tight upper bounds for the worst-case execution time of tasks in real-time systems. It directly analyzes binary executables and takes cache and pipeline behavior into account. No testing or measuring is necessary, the analysis results hold for all inputs and execution scenarios. Special kits simplify the qualification for DO-178C, ISO 26262, and other safety standards.
StackAnalyzer automatically determines the worst-case stack usage of the tasks in embedded applications. It directly analyzes binary executables and considers all possible execution scenarios. Tight integration with TargetLink and SCADE is available, as well as qualification kits for standards such as ISO 26262, DO-178B, and IEC 61508.
Astrée automatically proves the absence of runtime errors and invalid concurrent behavior in C applications. It is sound for floating-point computations, very fast, and exceptionally precise. The analyzer also checks for MISRA coding rules and supports qualification for ISO 26262, DO-178C level A, and other safety standards. Jenkins and Eclipse plugins are available.
CompCert is a formally verified optimizing C compiler for safety-critical and mission-critical software. Unlike any other production compiler, it is mathematically proven to be exempt from miscompilation issues. Such confidence in the correctness of the compilation process is unprecedented and helps meet the highest levels of software assurance.
For over a decade, Airbus France has been using our tools in the development of safety-critical avionics software for several airplane types, including the flight control software of the A380, the world’s largest passenger aircraft.
Honda has been using our tools in developing the FADEC software of a turbofan engine.
The Technical University of Munich is using our tools in the development, testing and optimization of flight control and navigation algorithms.
Daimler has been using our tools in many automotive software projects, including the powertrain control system of the new Actros truck.
NASA used our timing-analysis tool for demonstrating the absence of timing-related software defects in the 2010 Toyota investigation.
OHB uses our tools in the development of onboard software essential for mission success of the SmallGEO platform for geostationary communication satellites and the GALILEO FOC+++ platform for satellite navigation.
ESA used our runtime-error analyzer to prove the absence of runtime errors in the automatic docking software of the Jules Verne Automated Transfer Vehicle, enabling it to transport payloads to the International Space Station.
AREVA employs our runtime error analysis and stack analysis tools to verify their safety-critical TELEPERM XS platform that is used for engineering, testing, operating and troubleshooting nuclear reactors.
MTU uses our tools for verified compilation and static program analysis to ensure the correctness of control software for emergency power generators in power plants.
As a leading provider of embedded wireless communication and positioning solutions, u‑blox is using our tools to avoid stack overflow at compile time and to increase the reliability and quality of their controlling software.
Siemens used our expertise to drastically reduce the size of their mobile-phone applications, allowing 25% more functionality to be packed into the flash memory of millions of mobile phones worldwide.