In spring 2018, the static analyzers Astrée and RuleChecker were integrated into the development and verification processes at Robert Bosch Automotive Steering (Bosch/AS, formerly ZF Lenksysteme).
The integration
The verification process has two stages:
- Module Verification, that verifies small code units in isolation
- Integration Verification, that then considers a complete application composed of many modules
To start a Module Verification, developers can type make astree
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
- re-run the analysis on a newer version of the module’s code,
- review the analysis results and comments,
- run an Integration Verification over several modules.
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 verdict
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.
Official press release one year later: Static analysis at Bosch