AbsInt
AbsInt provides advanced development tools for embedded systems, and tools for validation, verification and certification of safety-critical software.
Absint tools are based on a generic and generative framework which allows an extremely quick, sound and flexible response to customer needs.
Astrée
Astrée is a static code analyzer that proves the absence of runtime errors and invalid concurrent behavior in safety-critical software written or generated in C/C++.
Astrée primarily targets embedded applications as found in aeronautics, earth transportation, medical instrumentation, nuclear energy, and space flight. Nevertheless, it can just as well be used to analyze any structured C/C++ programs, handwritten or generated, with complex memory usages, dynamic memory allocation, and recursion.
StackAnalyzer
StackAnalyzer automatically determines the worst-case stack usage of the tasks in your application. It lets you find any stack overflows, or formally prove the absence thereof.
Features
- Detailed and precise information on user-stack usage and system-stack usage by application tasks.
- Freely selectable entry points for the analysis. You can easily focus on any code parts of particular interest to you.
- Control-flow reconstruction directly from binary code. Potential flaws in the debug information will not confuse StackAnalyzer.
- Fully integrated, feature-rich graphical and textual viewers for control flow, analysis results, source code, assembly code, and configuration files.
- Customizable XML reports for documentation and certification.
- Optional ValueAnalyzer add-on for static analysis of register and memory cells, memory accesses and function calls.
- Seamless integration with other analysis tools from AbsInt (e.g. aiT for worst-case execution time analysis).
- Batch mode for easy integration with other tools, or into automated build processes.
CompCert
CompCert is a formally verified optimizing C compiler. Its intended use is compiling safety-critical and mission-critical software written in C and meeting high levels of assurance. It accepts most of the ISO C 99 language, with some exceptions and a few extensions. It produces machine code for ARM, PowerPC, x86, and RISC-V architectures.
What sets CompCert apart?
CompCert is the only production compiler that is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues. The code it produces is proved to behave exactly as specified by the semantics of the source C program.
This level of confidence in the correctness of the compilation process is unprecedented and contributes to meeting the highest levels of software assurance.
The formal proof covers all transformations from the abstract syntax tree to the generated assembly code. To preprocess and produce object and executable files, an external C preprocessor, assemblers, linkers, and C libraries have to be used. However, these unverified stages are well-understood and robust from an implementation perspective. This was demonstrated on a development version of CompCert in a 2011 study by Regehr, Yang et al.:
aiT Worst-Case Execution Time Analyzer
Timing Guarantees for Real-Time Systems
aiT WCET Analyzer computes systems. These bounds are tight bounds safe, for the worst-case execution time of tasks in safety-critical i.e. they are valid for any input scenario and each task execution.
aiT is based on statically analyzing a task’s intrinsic cache and pipeline behavior development of complex hard real-time systems on state-of-the-art hardware.
Features
- Visualization of the analysis results providing detailed information about key timing aspects, e.g. the worst-case path given program point.
- Various statistics, or the machine state interactive, at any tables graphs charts that let you quickly other areas of interest.
- Analysis report files for identify bottlenecks documentation and certification purposes, as well as for integration with numerous software development tools.
- Qualification Support Kits are available providing support for automatic tool qualification up the highest criticality levels (DO-178B, DO-178C, ISO26262, IEC 61508, EN 50128).
- Interprocedural analysis enables cache and pipeline behavior to be precisely predicted.
- The analyzer can be run in batch mode seamless continuous verification.
- Flexible annotation mechanism, enabling
- Developers can provide programmer-specific knowledge to aiT to further improve the analysis precision.
- aiT can be coupled with model-based code generators and system-level scheduling tools via an open XMLbased interface to provide timing information in the development phase.
- Graphical comparison of different analysis runs.
- Developers can quickly understand the effect of program modifications on worst-case timing.
Supported Processors
PowerPC 5xx / e200 (55xx, 56xx) / / e300 (603e, 82xx, 83xx) / 750/ 755 / 5777M / 5777C 7448 / 7447A, i386DX, AM486Motorola 68020, ARM Cortex M0 / Cortex-M1 / Cortex-M3 / Cortex-R4F / Cortex-R5F, Infineon XMC4500 (ARM Cortex-M4), TI TMS320C3x, TMS320F28, C16x/ST10, XC2365A-104F80L, HC11, Star12/ HCS12/ HCS12X, TriCore 1197 / 1767 / 1782 / 1784 / 1796 / 1797, AURIX TC 2xx, AURIX TC3xx, NEC/Renesas V850, LEON2, LEON3, ERC32.
TimeWeaver
Hybrid Worst-Case Execution Time Analysis
TimeWeaver combines static path analysis with real-time instruction-level tracing to provide worst-case execution time estimates. The computed time bounds provide valuable feedback for assessing system safety and for optimizing worst-case performance.
Features
The analysis results reported by TimeWeaver include:
- global end-to-end time, based on the maximum observed trace segment times combined to an overall bound
- end-to-end bounds for specific functions, depending on trace points
- coverage of the control-flow graph by the input traces
- maximum possible and maximum observed iteration counts for loops
- time variance of each code segment over all traces
- TimeWeaver offers the same powerful user interface you are used to from working with other AbsInt tools, with fully integrated graphical and textual viewers for control flow, analysis results, source code, assembly code, and configuration files. You can:
- interactively explore analysis results
- save and restore analysis scenarios
- export customizable reports for documentation and certification purposes
- start all analyses from the same GUI and handle all the tools with the same look and feel
Supported architectures and trace formats
- All PowerPC boards able to emit Nexus program trace messages (IEEE-ISTO 5001, class 2 or higher), for example:
- PowerPC QorIQ P204x/P30xx/P40xx/P50xx (e500mc core)
- PowerPC QorIQ T series (e5500/e6500 core)
- PowerPC Qorivva line MPC55xx/MPC56xx/MPC57xx (e200 core)
- ARM using cycle-accurate ETM traces, for example:
- Cortex-A53
- Cortex-R5F
ARM ULINK Pro traces are supported since release 21.10
- TriCore:
- AUDO family (e.g. TC1796)
- AURIX (e.g. TC275), including support for interactive MCDS tracing via Infineon DAS
- AURIX 2nd GEN (e.g. TC397)
- Tight integration with PowerTrace from Lauterbach for all CPU architectures