Spezifikation und Implementation des CAN-Arbitrierungsverfahrens in UPPAAL

Specification and Implementation of CAN Arbitration in UPPAAL

  • 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 automatiIn 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

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Dario Kresic, Kai-Steffen Hielscher, Reinhard German
URN:urn:nbn:de:bvb:29-opus-23535
Series (Volume number):Technical reports / Department Informatik, ISSN 2191-5008 (CS-2010-05)
Document Type:Report
Language:German
Date of Publication (online):2011/02/18
Release Date:2011/02/18
Tag:CAN-Bus; Medienzugriff; UPPAAL; Zeitautomaten
CAN bus; medium access; model checking; timed automata
SWD-Keyword:Kommunikationssystem; Leistungsbewertung; Model Checking
Institutes:Technische Fakultät -ohne weitere Spezifikation-
CCS-Classification:C.2.1 Network Architecture and Design
Dewey Decimal Classification:004 Datenverarbeitung; Informatik

$Rev: 12793 $