User story: Bosch Automotive Steering

Bosch logo

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:

  1. Module Verification, that verifies small code units in isolation
  2. 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

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.