eFMU Front End for Astrée

• The eFMU front end allows for the automatic generation of an Astrée project from an eFMU
• Astrée is a static code analyzer that finds runtime errors and rule violations in safety-critical software written or generated in C
• Astrée is sound - that is, if no errors are signaled, the absence of errors has been proved
• Astrée offers powerful annotation mechanisms for supplying external knowledge and fine-tuning the analysis precision for individual loops or data structures
• The integrated RuleChecker can be configured to check for compliance with MISRA, CWE, ISO/IEC, and SEI CERT C coding rules

Input(s):

• ProductionCode eFMU

Main feature(s):

• The eFMU front end reads an eFMU with C production code, sets up an Astrée project and starts Astrée
• Astrée automatically checks for runtime errors and violations of coding rules in C applications

Output(s):

• List of runtime errors and rule violations, or statement that no such problems exist

• The eFMU front end requires Python 3
• Astrée requirements: -- Windows: 64-bit Windows 7 SP1 or newer -- Linux: 64-bit CentOS/RHEL 7 or compatible -- 4 GB of RAM (16 GB recommended) -- 4 GB of disk space

Developers using the eFMI workflow

AbsInt offers commercial licenses, including training, support, and maintenance