TY - RPRT A1 - Kresic, Dario A1 - Hielscher, Kai-Steffen A1 - German, Reinhard T1 - Spezifikation und Implementation des CAN-Arbitrierungsverfahrens in UPPAAL T1 - Specification and Implementation of CAN Arbitration in UPPAAL 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. T3 - Technical reports / Department Informatik - CS-2010-05 KW - Model Checking KW - Kommunikationssystem KW - Leistungsbewertung KW - CAN-Bus KW - Medienzugriff KW - UPPAAL KW - Zeitautomaten KW - CAN bus KW - medium access KW - model checking KW - timed automata Y1 - 2010 UR - https://opus4.kobv.de/opus4-fau/frontdoor/index/index/docId/1620 UR - https://nbn-resolving.org/urn:nbn:de:bvb:29-opus-23535 ER -