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

Grobosch, Sebastian; Engell, Sebastian; Kowalewski, Stefan

doi:38761

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

Grobosch, Sebastian^RWTH*

2019

VerantwortlichkeitsangabeSebastian Patrick Grobosch

ImpressumDüren : Shaker 2019

Umfang1 Online-Ressource (ix, 162 Seiten) : Illustrationen, Diagramme

ISBN978-3-8440-6984-6

ReiheAachener Informatik-Berichte ; 2019-03

Dissertation, RWTH Aachen University, 2018

Auch veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Kowalewski, Stefan (Thesis advisor)^RWTH* ; Engell, Sebastian (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2018-11-30

Online
DOI: 10.18154/RWTH-2019-09536
URL: https://publications.rwth-aachen.de/record/768999/files/768999.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
eingebettete Systeme (frei) ; Informatik (frei) ; KMU (frei) ; Software Entwicklung (frei) ; embedded systems (frei) ; formal verification (frei) ; formale Methoden (frei) ; formale Verifikation (frei) ; small and medium sized enterprises (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Die Anzahl der Steuergeräte in Fahrzeugen der Oberklasse ist in den letzten 15 Jahren stetig gestiegen und liegt aktuell bei etwa 100 Stück. Dabei entsteht der Großteil aller Innovationen im Fahrzeug durch Elektronik und Software. Dies macht Software einerseits zu einem der wichtigsten Innovationstreiber für Unternehmen in der Automobilindustrie, andererseits birgt sie ein hohes Risikopotential: Programmfehler. Durch internationale Normen und strengere Anforderungen an die Software-Qualität wird versucht, diesem Risiko entgegenzuwirken. Um alle Wünsche der Endkunden individuell erfüllen zu können, wächst allerdings die Komplexität der Systeme durch die steigende Variantenvielfalt. Das Testen von solchen Software-Systemen kann dabei nur das Vorhandensein von Fehlern zeigen, jedoch nicht deren Abwesenheit. Eine Garantie, dass ein System die gestellten Anforderungen erfüllt, kann durch formale Methodengegeben werden. Die in dieser Arbeit vorgestellten Ansätze tragen dazu bei, die Software-Entwicklung in kleinen und mittleren Unternehmen durch Methoden der formalen Verifikation zu verbessern und zu unterstützen. Dabei werden die Vorteile von kleinen gegenüber großen Unternehmen genutzt und ausgebaut. Dazu zählen die ausgeprägte Nähe zum Kunden sowie ein hohes Maß an Flexibilität und Wirtschaftlichkeit. Die Systemkomplexität der meisten Projekte sowie die Prozessstrukturen können positiv zur Akzeptanz für die Einführung von formalen Methoden in den jeweiligen Entwicklungsprozess beitragen. Der erste Ansatz befasst sich mit der Analyse von Zeitanforderungen für eingebettete Systeme basierend auf der formalen Methode des Model-Checkings. Dabei wird für ein bestehendes Variantensystem für Steuergeräte ein Task-System mittels Uppaal modelliert und eine Einplanbarkeitsanalyse auf Basis von Zeitautomaten vorgestellt. Zur Verwaltung der Varianten wurde ein Framework basierend auf pure::variants entworfen und eine bestehende Software-Plattform evolutionär in eine Produktlinie umgewandelt. Damit können sich Unternehmen stärker auf die individuellen Kundenwünsche fokussieren und vorhandene Komponenten effizient und mit hoher Qualität wiederverwenden. Der zweite Ansatz zur Verbesserung der Software-Qualität befasst sich mit der Verifikation von Programmcode eingebetteter Systeme durch den Model-Checker Arcade. Hierbei wurde speziell das Formulieren von formalen Anforderungen und die Anwendbarkeit im industriellen Umfeld untersucht. Mittels dieses Ansatzes konnten sowohl Fehler im Programmcode lokalisiert als auch das Einhalten von Anforderungen gezeigt werden. Der Einsatz von Binär-Code-Verifikation kann den Testaufwand reduzieren, aber nichtersetzen. Der Vorteil für Unternehmen ist allerdings, dass diese Methode das Ausbleiben von Fehlern beweisen kann, was durch herkömmliches Testen nicht möglich ist. Insgesamt wurde ein Ansatz zur Integration formaler Methoden in den Entwicklungsprozesseines kleinen und mittleren Unternehmens vorgestellt, erfolgreich mit entsprechender Werkzeugunterstützung umgesetzt und evaluiert. Mit Hilfe der gezeigten Methoden ist es möglich, den Testaufwand zu reduzieren und die Qualität von automobilen Steuerungssystemen schon frühzeitig in den wichtigen Phasen der Entwicklung zu steigern.

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.

OpenAccess:
PDF
(additional files)