AbsInt Angewandte Informatik, GmbH, Germany

Profile

AbsInt is an SME focused on the development of program analysis tools for the verification, validation, and certification of safety-critical software. AbsInt’s product range includes tools for timing analysis, stack usage analysis, and runtime-error detection. The tools are based on an abstract interpretation approach. The timing and stack analyzers operate on executables for various processor architectures including modern micro-controllers with caches and complex pipelines. The timing analyzer aiT determines worst-case execution times by static program analysis on binary code, intended to be used for the verification of timing properties in the certification process. The TimingProfiler tool is intended to be used in early stages of system development to provide quick feedback about the timing behaviour. It is ideally suited for constantly monitoring timing behaviour during software development and in model-based development environments. The Astrée tool finds runtime errors in single-threaded and multi-threaded C programs or proves their absence. It has been licensed from École Normale Supérieure and is being extended and marketed by AbsInt. Likewise, the formally verified optimizing C compiler CompCert has been licensed from INRIA.

 

AbsInt collaborates with academic institutions to industrialise their academic prototype tools, with other tool vendors to allow users to easily exchange information between tools with complementary features, and with vendors of development tools to integrate the analysis tools into their development environments. AbsInt has business relationships with Suppliers and OEMs in the avionic and automotive domains who use AbsInt analyzers to verify that their software satisfies the necessary safety constraints. AbsInt’s customers include large companies with safety-critical applications such as Daimler, Siemens, Infineon, EADS, and Airbus.

Relevant expertise

Development of

·       TimingProfiler – Tool for constantly monitoring timing behaviour during software development and in model-based development environments; useful for identifying application parts that cause unsatisfactory execution times;

Astrée – Static program analyzer that finds run-time errors in safety-critical embedded applications, or proves their absence.

Main tasks

AbsInt will help in assessing the safety and security of the systems in the use cases “Air-Traffic Management” and “Space Multicore Architectures” with its TimingProfiler and Astrée tools. In particular, AbsInt will cooperate with SYSGO in the static analysis of SYSGO’s PikeOS kernel with AbsInt’s Astrée tool to find violations of certain safety and security principles, or proving the absence of such violations by means of automatically found program properties. Such formally proven properties can be used as arguments for safety and security in the certification process.