Sebastian GroboschFormale Methoden für die Entwicklung von eingebetteter Software in kleinen und mittleren Unternehmen | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
ISBN: | 978-3-8440-6984-6 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Series: | Mathematik, Informatik | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Keywords: | formale Methoden; eingebette Systeme; kleine und mittlere Unternehmen; Softwareentwicklung | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Type of publication: | Thesis | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Language: | German | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Pages: | 182 pages | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Figures: | 60 figures | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Weight: | 238 g | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Format: | 21 x 14,8 cm | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Binding: | Paperback | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Price: | 48,80 € / 61,10 SFr | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Published: | November 2019 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Buy: | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Download: | Available PDF-Files for this title: You need the Adobe Reader, to open the files. Here you get help and information, for the download. These files are not printable.
User settings for registered users You can change your address here or download your paid documents again.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Recommendation: | You want to recommend this title? | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Review copy: | Here you can order a review copy. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Link: | You want to link this page? Click here. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Abstract: | 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. Das Testen von komplexen Software-Systemen kann 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. 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. Der zweite Ansatz zur Verbesserung der Software-Qualität befasst sich mit der Verifikation von Programmcode eingebetteter Systeme durch den Model-Checker Arcade. 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. |