Hinweis zum Urheberrecht
Report (Bericht) zugänglich unter
URN: urn:nbn:de:bvb:29-opus-23535
URL: http://www.opus.ub.uni-erlangen.de/opus/volltexte/2011/2353/
Spezifikation und Implementation des CAN-Arbitrierungsverfahrens in UPPAAL
Specification and Implementation of CAN Arbitration in UPPAAL
Kresic, Dario ;
Hielscher, Kai-Steffen ;
German, Reinhard
| SWD-Schlagwörter: |
| Model Checking , Kommunikationssystem , Leistungsbewertung |
| Freie Schlagwörter (Deutsch): |
| CAN-Bus, Medienzugriff, UPPAAL, Zeitautomaten |
| Freie Schlagwörter (Englisch): |
| CAN bus, medium access, model checking, timed automata |
| CCS - Klassifikation: |
| C.2.1 |
| Fakultät: |
| Technische Fakultät |
| DDC-Sachgruppe: |
| Informatik |
| Dokumentart: |
| Report (Bericht) |
| Schriftenreihe: |
| Technical reports / Department Informatik, ISSN 2191-5008 |
| Bandnummer: |
| CS-2010,5 |
| Sprache: |
| Deutsch |
| Erstellungsjahr: |
| 2010 |
| Publikationsdatum: |
| 18.02.2011 |
| Kurzfassung in Deutsch: |
| 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. |
Sie benötigen weitere Informationen?
Fragen Sie uns!