The verification process has two stages:
To start a Module Verification, developers can type
to automatically configure and run Astrée and RuleChecker on their
module. The automatic configuration considers all relevant information
from the build process, like C file names, include paths, and macro
definitions. Ranges of interface variables for input and output are also
derived automatically from the interface specification of the module.
After running the automatically configured analysis, developers can use the graphical user interface to investigate and comment on all possible run-time errors and MISRA-C rule violations reported by Astrée and RuleChecker.
The development-process integration then automatically stores the full analysis configuration, results, and comments in a central repository.
Stored analysis configurations and results can be retrieved from the repository in order to
For all three scenarios, Astrée and RuleChecker are configured automatically by the process integration based on information from the build system, interface specification, and module verification results. Moreover, Astrée and RuleChecker provide the same user interface for all use cases.
The results of an Integration Verification can be commented on in the graphical user interface and stored in the central repository in the same way as after a Module Verification.
The successful introduction of Astrée and RuleChecker allowed Bosch/AS to replace their existing legacy tools, resulting in significant savings thanks to faster analysis speed, improved accuracy, and optimized licensing and support costs.