Automotive software underlies high quality requirements and thus is being developed with great effort. Nevertheless, in particular cases, errors occur late within the development process or - in the worst case- during use, not having been recognized during the numerous quality assurance procedures. The enterprises engaged in the development have great interest in methods which can improve this situation.

A possible approach for an early error detection is the method of formal verification. This method has been a research topic since decades and meanwhile, promising tools are available, yet lacking establishment within the automotive software domain.

Thus, the topic of this diploma thesis is the research of possibilities being offered by formal verification for error prevention in automotive software development. The starting point will be real error data for low-level software in electronic control units which are being made available by the industry partner Siemens-VDO. On this basis and with the possibility of asking developers for further information, the question of whether the respective errors would have been found during systematic use of formal verification methods (above all model checking), should be answered. Along with an analysis considering the effort and possible alternatives, you should evaluate which methodical improvements can be achieved through formal verification.

The diploma thesis will be carried out together with Siemens-VDO in Regensburg. It will require stopovers in Regensburg as well as in Aachen.

• Dr. rer. nat. Andreas Polzer

• Dr.rer.nat. Bastian Schlich