C.2.1 Network Architecture and Design
Refine
Year of publication
- 2010 (1)
Document Type
- Report (1)
Language
- German (1)
Has Fulltext
- yes (1)
Keywords
- CAN bus (1)
- CAN-Bus (1)
- Kommunikationssystem (1)
- Leistungsbewertung (1)
- Medienzugriff (1)
- Model Checking (1)
- UPPAAL (1)
- Zeitautomaten (1)
- medium access (1)
- model checking (1)
Institute
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.