Spezifikation und Implementation des CAN-Arbitrierungsverfahrens in UPPAAL

Specification and Implementation of CAN Arbitration in UPPAAL

Please always quote using this URN: urn:nbn:de:bvb:29-opus-23535
  • 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; dieIn 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.show moreshow less

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar Statistics
Metadaten
Author:Dario Kresic, Kai-Steffen Hielscher, Reinhard German
Persistent identifiers - URN:urn:nbn:de:bvb:29-opus-23535
Series (Volume number):Technical reports / Department Informatik (CS-2010-05)
Document Type:Report
Language:German
Year of publication:2010
Publishing Institution:Friedrich-Alexander-Universität Erlangen-Nürnberg (FAU)
Release Date:2011/02/18
Tag:CAN-Bus; Medienzugriff; UPPAAL; Zeitautomaten
CAN bus; medium access; model checking; timed automata
SWD-Keyword:Model Checking; Kommunikationssystem; Leistungsbewertung
Institutes:Technische Fakultät / Technische Fakultät -ohne weitere Spezifikation-
CCS-Classification:C. Computer Systems Organization / C.2 COMPUTER-COMMUNICATION NETWORKS / C.2.1 Network Architecture and Design
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
open_access (DINI-Set):open_access
Einverstanden ✔
Diese Webseite verwendet technisch erforderliche Session-Cookies. Durch die weitere Nutzung der Webseite stimmen Sie diesem zu. Unsere Datenschutzerklärung finden Sie hier.