Katalog : Details
 | Sebastian GroboschFormale Methoden für die Entwicklung von eingebetteter Software in kleinen und mittleren Unternehmen | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ISBN: | 978-3-8440-6984-6 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Reihe: | Mathematik, Informatik | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Schlagwörter: | formale Methoden; eingebette Systeme; kleine und mittlere Unternehmen; Softwareentwicklung | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Publikationsart: | Dissertation | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Sprache: | Deutsch | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Seiten: | 182 Seiten | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Abbildungen: | 60 Abbildungen | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Gewicht: | 238 g | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Format: | 21 x 14,8 cm | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Bindung: | Paperback | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Preis: | 48,80 € | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Erscheinungsdatum: | November 2019 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Kaufen: | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Download: | Verfügbare Online-Dokumente zu diesem Titel: Sie benötigen den Adobe Reader, um diese Dateien ansehen zu können. Hier erhalten Sie eine kleine Hilfe und Informationen, zum Download der PDF-Dateien. Bitte beachten Sie, dass die Online-Dokumente nicht ausdruckbar und nicht editierbar sind.
Benutzereinstellungen für registrierte Online-Kunden Sie können hier Ihre Adressdaten ändern sowie bereits georderte Dokumente erneut aufrufen.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Weiterempfehlung: | Sie möchten diesen Titel weiterempfehlen? | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Rezensionsexemplar: | Hier können Sie ein Rezensionsexemplar bestellen. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Verlinken: | Sie möchten diese Seite verlinken? Hier klicken. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Zusammenfassung: | 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. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
