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.