The following technical report is available from http://aib.informatik.rwth-aachen.de:

Formale Methoden für die Entwicklung von eingebetteter Software in kleinen und mittleren Unternehmen Sebastian Patrick Grobosch AIB 2019-03

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 Methoden gegeben 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 nicht ersetzen. 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 Entwicklungsprozess eines 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.