Bibliographic Metadata
Bibliographic Metadata
- TitleTiming Verifikation von AUTOSAR Softwarearchitekturen : / vorgelegt von M. Sc. Steffen Beringer
- Translated titleTiming verification of AUTOSAR software architectures
- Author
- Participants
- Published
- Description1 Online-Ressource (xiv, 170 Seiten) : Diagramme
- Institutional NoteUniversität Paderborn, Dissertation, 2022
- AnnotationTag der Verteidigung: 18.11.2022
- Defended on2022-11-18
- LanguageGerman ; English
- Document TypesDissertation (PhD)
- URN
- DOI
Links
- Social MediaShare
- Reference
- IIIF
Files
Classification
Zusammenfassung
Der Einsatz formaler Verifikation für Softwarearchitekturmodelle im Automobil ermöglicht es die Korrektheit und Robustheit von Steuergerätesoftware signifikant zu erhöhen. Dies gilt insbesondere für die Verifikation von Echtzeitanforderungen mittels Timing Verifikation. Existierende Methoden benötigen jedoch für die Durchführung der Timing Verifikation Steuergerätecode, der häufig erst spät im Prozess verfügbar ist oder berücksichtigen den in der Automobilindustrie verbreiteten AUTOSAR-Standard nicht. Des Weiteren ignorieren existierende Ansätze die Komplexität und Fehleranfälligkeit der Herleitung von formalen Echtzeitanforderungen für AUTOSAR aus Anforderungsdokumenten. Dies führt insgesamt dazu, dass existierende Ansätze erst spät im Entwicklungsprozess angewendet werden können und eine geringe praktische Relevanz aufweisen.In dieser Arbeit schlagen wir einen neuen Ansatz zur Timing Verifikation von AUTOSAR Softwarearchitekturen vor. Es wird zunächst eine Formalisierung für AUTOSAR Softwarearchitekturen, sowie für AUTOSAR Timing Anforderungen bereitgestellt. Daraufhin stellen wir einen Prozess vor, in dem AUTOSAR Timing Anforderungen zunächst auf Konsistenz geprüft werden und anschließend formal verifiziert werden. Im Gegensatz zu anderen Ansätzen wird kein Quellcode benötigt, sondern ausschließlich das AUTOSAR Architekturmodell verwendet.
Abstract
The use of formal verification for automotive software architecture models significantly increases the correctness and robustness of ECU software. This is especially true for the verification of real-time requirements using timing verification. Existing methods require ECU source-code to perform timing verification, which is often not available until late in the process, or do not take into account the AUTOSAR standard that is widely used in the automotive industry. Furthermore, existing approaches ignore the complexity and error-proneness of deriving formal real-time requirements for AUTOSAR from requirements documents. Overall, this means that the existing approaches can only be applied late in the development process and have little practical relevance.In this thesis, a new approach for timing verification of AUTOSAR software architectures is proposed. First, a formalization for AUTOSAR software architectures as well as for AUTOSAR timing requirements is provided. A process is then presented in which AUTOSAR timing requirements are first checked for consistency and then formally verified. In contrast to other approaches, no source code is required, but only the AUTOSAR software architecture model is used.
Content
Stats
- The PDF-Document has been downloaded 53 times.
License/Rightsstatement
