Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-33312
Titel: Modeling and verifying the FlexRay physical layer protocol with reachability checking of timed automata
VerfasserIn: Gerke, Michael
Sprache: Englisch
Erscheinungsjahr: 2020
Kontrollierte Schlagwörter: FlexRay
Zeitbehafteter Automat
Model Checking
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Dissertation
Abstract: In this thesis, I report on the verification of the resilience of the FlexRay automotive bus protocol's physical layer protocol against glitches during message transmission and drifting clocks. This entailed modeling a significant part of this industrially used communictation protocol and the underlying hardware as well as the possible error scenarios in fine detail. Verifying such a complex model with model-checking led me to the development of data-structures and algorithms able to handle the associated complexity using only reasonable resources. This thesis presents such data-structures and algorithms for reachability checking of timed automata. It also present modeling principles enabling the construction of timed automata models that can be efficiently checked, as well as the models arrived at. Finally, it reports on the verified resilience of FlexRay's physical layer protocol against specific patterns of glitches under varying assumptions about the underlying hardware, like clock drift.
In dieser Dissertation berichte ich über den Nachweis der Resilienz des Bitübertragungsprotokolls für die physikalische Schicht des FlexRay-Fahrzeugbusprotokolls gegenüber Übertragungsfehlern und Uhrenverschiebung. Dafür wurde es notwendig, einen signifikanten Teil dieses industriell genutzten Kommunikationsprotokolls mit seiner Hardwareumgebung und die möglichen Fehlerszenarien detailliert zu modellieren. Ein so komplexes Modell mittels Modellprüfung zu überprüfen führte mich zur Entwicklung von Datenstrukturen und Algorithmen, die die damit verbundene Komplexität mit vernünftigen Ressourcenanforderungen bewältigen können. Diese Dissertation stellt solche Datenstrukturen und Algorithmen zur Erreichbarkeitsprüfung gezeiteter Automaten vor. Sie stellt auch Modellierungsprinzipien vor, die es ermöglichen, Modelle in Form gezeiteter Automaten zu konstruieren, die effizient überprüft werden können, sowie die erstellten Modelle. Schließlich berichtet sie über die überprüfte Resilienz des FlexRay-Bitübertragungsprotokolls gegenüber spezifischen Übertragungsfehlermustern unter verschiedenen Annahmen über die Hardwareumgebung, wie etwa die Uhrenverschiebung.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-333120
hdl:20.500.11880/30860
http://dx.doi.org/10.22028/D291-33312
Erstgutachter: Finkbeiner, Bernd
Tag der mündlichen Prüfung: 21-Dez-2020
Datum des Eintrags: 11-Mär-2021
Drittmittel / Förderung: DFG: SFB/TRR 14 "AVACS - Automatische Verifikation und Analyse komplexer Systeme"
Fördernummer: TRR 14
Fakultät: MI - Fakultät für Mathematik und Informatik
Fachrichtung: MI - Informatik
Professur: MI - Prof. Bernd Finkbeiner, PhD
Sammlung:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Dateien zu diesem Datensatz:
Datei Beschreibung GrößeFormat 
GerkePhDThesis.pdf1,08 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.