Formale Methoden für die Entwicklung von eingebetteter Software in kleinen und mittleren Unternehmen

The number of control units within upper class vehicles has steadily increased over the last 15 years and is currently around 100 units. The majority of all innovations in the vehicle are generated by electronics and software. This makes software, on the one hand, one of the most important drivers of innovation for companies in the automotive industry. On the other hand, it involves a high risk potential: programming errors. With international standards and stricter requirements for software quality the industry is trying to counteract this risk. However, the complexity of the systems is growing due to the increasing diversity of variants in order to be able to fulfil all the wishes of the end customer individually. The testing of such software systems can only show the presence of errors, but not their absence. A guarantee that a system fulfils the requirements can be provided by formal methods. The approaches presented in this thesis help to improve and support software development in small and medium-sized enterprises by means of formal verification methods. In doing so, the advantages of small over large companies should be utilised and enhanced. This includes the close proximity to the customer as well as a high degree of flexibility and profitability. The system complexity of most projects as well as the process structures can positively contribute to the adoption of formal methods in the respective development process. The first approach deals with the analysis of timing requirements for embedded systems based on the formal method of model checking. In this case, a task system is modelled using Uppaal for an existing variant system for control units, and a schedulability analysis based on timed automata is presented. To manage the variants, a framework based on pure::variants was designed and an existing software platform was transformed into a product line. This allows companies to focus more on individual customer requirements and to reuse existing components efficiently and with high quality. The second approach to improve the quality of software is to verify the program code of embedded systems through the model checker Arcade. Specifically, the formalization of formal requirements and the applicability in the industrial environment were analysed. Errors in the program code could be localized as well as compliance with requirements were shown. The use of binary code verification can reduce the test effort, but will not replace it. The advantage for companies is, however, that this method can prove the absence of errors, which is not possible by conventional testing. Overall, an approach to the integration of formal methods into the development process of a small and medium-sized enterprise was presented, successfully implemented and evaluated with appropriate tool support. With the methods shown, it is possible to reduce the test effort and to increase the quality of automotive control systems at a nearly stage in the important phases of development