TY  - RPRT
T1  - Spezifikation und Implementation des CAN-Arbitrierungsverfahrens in UPPAAL
A1  - Kresic,Dario
A1  - Hielscher,Kai-Steffen
A1  - German,Reinhard
Y1  - 2011/02/18
N2  - In dieser Arbeit stellen wir eine durch Zeitautomaten modellierte Spezifikation des Mediumzugriffs im CAN-Protokoll vor sowie ihre Implementierung in UPPAAL. Zeitliche Anforderungen wurden dabei durch entsprechende Uhren-Nebenbedingungen erfasst. Dieses Zeitautomaten-Modell wurde anschließend automatisch verifiziert (Model Checking), wobei mehrere  Anforderungen identifiziert wurden, die das CAN Protokoll erfüllen muß (wie Deadlock-Freiheit des Modells, Übertragungsrecht für die höchstpriore Nachricht, exklusives Übertragungsrecht für beliebigen CAN-Adapter nach der gewonnenen Arbitrage etc.). All diese Eigenschaften wurden in einer Variante der temporalen Logik CTL spezifiziert; die automatische Verifikation selbst wurde dabei mit UPPAAL durchgeführt, einem Model Checker für zeitautomaten-basierte Modelle.
KW  - Model Checking
KW  - Kommunikationssystem
KW  - Leistungsbewertung
CY  - Erlangen
PB  - Universitätsbibliothek der Universität Erlangen-Nürnberg
AD  - Universitätsstraße. 4, 91054 Erlangen
L2  - http://www.opus.ub.uni-erlangen.de/opus/volltexte/2011/2353
ER  -