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.…
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 |